35 lines
1.3 KiB
Markdown
35 lines
1.3 KiB
Markdown
---
|
||
title: "预期引理规划（Anticipatory Lemma Planning）"
|
||
created: 2026-07-03
|
||
updated: 2026-07-03
|
||
type: concept
|
||
tags: ["theorem-proving", "planning", "dag", "lemma"]
|
||
sources: ["arxiv:2606.03303"]
|
||
---
|
||
|
||
# 预期引理规划
|
||
|
||
> 在蓝图生成阶段提前提出辅助引理——当前不需要，但保留在 DAG 中随时可用。
|
||
|
||
## 核心定义
|
||
|
||
**预期引理规划** 是 [[leap-agentic-atp|LEAP]] 中 [[and-or-dag-memoization|AND-OR DAG]] 记忆化的一项高级能力：在生成蓝图时，Agent 可提出辅助引理声明，这些引理**不是当前证明草图的必要依赖**，但预期在后续证明步骤中可能有用。
|
||
|
||
## 在 DAG 中的表示
|
||
|
||
- 预期引理以**虚线边**连接——表示非必需依赖
|
||
- 在当前 AND 节点被解决前，这些引理不作为硬性依赖
|
||
- 当后续分支需要时，引理已经存在，无需重新推导
|
||
|
||
## 价值
|
||
|
||
1. **前瞻性**：类似人类数学家「我先引入几个可能有用的中间结果」
|
||
2. **避免重复**：当自然语言推理暗示某个中间结论有用时，提前注册为引理
|
||
3. **降低回溯成本**：不会因缺少引理而需要回溯到更早的节点
|
||
|
||
## 参考
|
||
|
||
- [[leap-agentic-atp|LEAP]]
|
||
- [[and-or-dag-memoization|AND-OR DAG 记忆化]]
|
||
- [[blueprint-driven-atp|蓝图驱动 ATP]]
|