49 lines
1.7 KiB
Markdown
49 lines
1.7 KiB
Markdown
---
|
||
title: "蓝图驱动 ATP（Blueprint-Driven ATP）"
|
||
created: 2026-07-03
|
||
updated: 2026-07-03
|
||
type: concept
|
||
tags: ["theorem-proving", "planning", "decomposition", "lean"]
|
||
sources: ["arxiv:2606.03303"]
|
||
---
|
||
|
||
# 蓝图驱动 ATP
|
||
|
||
> 不是一次性合成完整证明，而是通过蓝图草图逐步分解和迭代——仿效人类数学家的证明工作流。
|
||
|
||
## 核心定义
|
||
|
||
**蓝图驱动 ATP** 是 [[leap-agentic-atp|LEAP]] 在直接形式化失败后的回退策略：生成**非正式蓝图**（说明如何将目标归约为子目标），再翻译为 **Lean 证明草图**，将子目标注册入 [[and-or-dag-memoization|AND-OR DAG]] 后递归处理。
|
||
|
||
## 工作流
|
||
|
||
```
|
||
目标（OR 节点）
|
||
↓ 直接证明失败
|
||
蓝图生成 → 非正式蓝图（规划空间）
|
||
↓
|
||
翻译为 Lean 证明草图（AND 节点）
|
||
↓ Lean 编译器验证草图
|
||
→ 通过：子目标 → 新 OR 节点 → 递归处理
|
||
→ 拒绝：LLM Reviewer 评估 → 重试/回溯/放弃
|
||
```
|
||
|
||
## 与 Lean Blueprint 工具的关系
|
||
|
||
受 Lean Blueprint 工具的启发——该工具允许数学家编写人类可读的证明路线图，链接到 Lean 代码并可视化为 DAG。已在 Fermat's Last Theorem 形式化路线图等大型项目中验证。
|
||
|
||
## 与直接形式化的对比
|
||
|
||
| 维度 | 直接形式化 | 蓝图驱动 |
|
||
|------|----------|---------|
|
||
| 策略 | 一次性生成完整证明 | 分解为子目标逐步攻克 |
|
||
| 容错 | 整体正确才通过 | 子目标可独立重试 |
|
||
| 复用 | 无 | 引理跨分支复用 |
|
||
| 适用 | 简单/中等难度 | 高难度、多步骤证明 |
|
||
|
||
## 参考
|
||
|
||
- [[leap-agentic-atp|LEAP]]
|
||
- [[and-or-dag-memoization|AND-OR DAG 记忆化]]
|
||
- [[interleaved-informal-formal-planning|非正式-形式化交错规划]]
|