1.5 KiB
1.5 KiB
title, created, updated, type, tags, sources
| title | created | updated | type | tags | sources | |||||
|---|---|---|---|---|---|---|---|---|---|---|
| 非正式-形式化交错规划（Interleaved Informal-Formal Planning） | 2026-07-03 | 2026-07-03 | concept |
|
|
非正式-形式化交错规划
LLM 擅长非正式推理和策略生成，Lean 擅长严格验证——交错规划让二者各司其职。
核心定义
非正式-形式化交错规划 是 leap-agentic-atp 的设计原则：在每个证明步骤中，先以自然语言做策略规划，再翻译为形式化 Lean 代码。这利用了 LLM 和 Lean 的互补优势。
两条路径中的体现
直接证明路径
- LLM 生成非正式论证（自然语言）→ 翻译为 Lean 候选证明
- Lean 编译器验证 → 失败则 LLM 修正非正式论证 → 重新翻译
分解路径（blueprint-driven-atp）
- LLM 生成非正式蓝图（说明如何归约为子目标）
- 翻译为 Lean 证明草图 → 记录依赖关系
- 每个子目标递归进入非正式 → 形式化循环
为什么需要交错
- 形式化代码直接生成极脆弱：一步错误整个证明报废
- 非正式草图提供规划空间——在形式化之前先理顺策略
- 可解释性：每个形式化尝试都有对应的非正式理由，方便审查