---
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]]