1.8 KiB
1.8 KiB
title, created, updated, type, tags, sources
| title | created | updated | type | tags | sources | |||||
|---|---|---|---|---|---|---|---|---|---|---|
| AND-OR DAG 分层记忆化 | 2026-07-03 | 2026-07-03 | concept |
|
|
AND-OR DAG 分层记忆化
不只是记录证明进度，还结构化分层记忆——单调精化、引理复用、预期规划。
核心定义
AND-OR DAG 分层记忆化 是 leap-agentic-atp 证明树的组织方式：
- OR 节点：开放目标或引理声明——可用任意有效策略解决
- AND 节点：候选分解——其成功取决于所有子目标都被证明
三个关键属性
1. 单调精化（Monotone Refinement）
一旦目标被分解为子目标，后续搜索可聚焦于扩展和解决这些后代，无需重构已有依赖结构。单个证明尝试可被修改、扩展或放弃，而 DAG 保留整体证明计划的稳定依赖结构。
2. 引理记忆化（Lemma Memoization）
中间引理声明存储为共享证明节点，在不同分支中出现相同子问题时复用。这减少了冗余推导，让独立证明路径收敛于公共依赖。
3. 预期引理规划（Anticipatory Lemma Planning）
蓝图生成阶段可提出当前不立即需要但未来可能有用的辅助引理。这些预期引理作为非必需依赖（虚线边）保留在图记忆中，不影响当前 AND 节点的解决。
与证明透明度的关系
DAG 暴露了：哪些目标仍开放、哪些引理已解决、哪些节点阻塞下游进展。这为 verification-guided-proof-search 提供可解释的蓝图式工作空间，也支持人-AI 协作。