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