Direct Optimization of Generators for Search in Automated Theorem Proving

📄 arXiv: 2609.25575v1 📥 PDF

作者: Adam Ousherovitch, Ambuj Tewari

分类: cs.AI, stat.ML

发布日期: 2026-09-22

💡 一句话要点

提出计算对齐训练以优化自动定理证明中的生成器

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 自动定理证明 大型语言模型 计算对齐训练 树搜索 损失函数优化 搜索策略 证明成功率

📋 核心要点

  1. 现有方法在自动定理证明中，使用交叉熵作为损失函数在树搜索中表现不佳，导致生成器性能受限。
  2. 本文提出计算对齐训练（CAT）方法，通过政策引导搜索的抽象，推导出新的损失函数以优化生成器。
  3. 在Lean基准测试中，提出的方法在六种搜索策略下的证明成功率显著高于传统交叉熵，且在计算预算上表现出良好的扩展性。

📝 摘要（中文）

微调的大型语言模型（LLMs）在自动定理证明（ATP）中取得了显著进展，但通常作为树搜索中的指导策略而非单次生成使用。近期研究表明，交叉熵在平面搜索策略中表现不佳，提出了新的损失函数以纠正这一不匹配。将这种对齐扩展到树搜索中更具挑战性，因为证明发现依赖于通过未跟踪状态的探索和恢复。本文通过政策引导搜索的抽象，将计算对齐训练（CAT）扩展到此设置，推导出可处理的、支持跟踪的损失函数。我们还引入了一种与搜索无关的均匀分配（UA）损失，考虑预算而不指定具体搜索。两者在每个策略的交叉熵梯度上施加标量权重。在Lean基准上，这两种方法在六种搜索策略中均实现了比交叉熵更高的证明成功率，且单一共享的UA适配器表现出色。预算扫描显示，在256次扩展时，相较于16次扩展，CAT的增益更大，表明其在测试时间计算上具有良好的扩展性。

🔬 方法详解

问题定义：本文旨在解决自动定理证明中生成器性能不足的问题，现有方法在树搜索中使用交叉熵作为损失函数，导致生成效果不佳，特别是在未跟踪状态的探索中表现不理想。

核心思路：论文提出计算对齐训练（CAT）方法，通过引入新的损失函数，优化生成器在树搜索中的表现，特别是针对未跟踪状态的探索和恢复。

技术框架：整体架构包括政策引导搜索的抽象，推导出可处理的损失函数，并结合均匀分配（UA）损失，形成一个支持跟踪的损失计算流程。

关键创新：最重要的技术创新在于将计算对齐训练扩展到树搜索中，并引入与搜索无关的均匀分配损失，显著提高了生成器的性能。

关键设计：论文设计了新的损失函数，考虑了搜索预算的影响，并在每个策略的交叉熵梯度上施加标量权重，优化了生成器的训练过程。具体参数设置和损失函数的设计细节在实验中进行了验证。

🖼️ 关键图片

fig_0
fig_1

📊 实验亮点

实验结果表明，提出的CAT方法在Lean基准上实现了比交叉熵更高的证明成功率，尤其在16次扩展时的增益显著，显示出该方法在计算预算上的良好扩展性。

🎯 应用场景

该研究在自动定理证明领域具有广泛的应用潜力，能够提升生成器在复杂搜索任务中的表现，适用于数学证明、程序验证等领域，未来可能推动智能推理系统的发展。

📄 摘要（原文）

Fine-tuned Large Language Models (LLMs) significantly advance Automated Theorem Proving (ATP), but are often deployed as guiding policies within tree search rather than for single-attempt generation. Recent work shows cross entropy is suboptimal for an LLM used in flat search strategies such as aggregation or filtering and that work has developed new loss functions to correct this misalignment. Extending this alignment to tree search is more challenging: proof discovery depends on exploration and recovery through off-trace states that supervised demonstrations do not reveal. We extend Compute-Aligned Training (CAT) to this setting through an abstraction of policy-guided search, deriving tractable, trace-supported losses. Alongside these search-aware losses, we introduce a search-agnostic uniform-allocation (UA) loss that accounts for the budget without specifying the specific search. Both induce scalar weights on per-tactic cross-entropy gradients. We characterize how off-trace behavior affects the search-aware weights, including conditions for vanishing approximation error at large budgets. On a Lean benchmark, both approaches achieve higher observed proof-success rates than cross-entropy across six search strategies, with strong results from a single shared UA adapter. Budget sweeps show larger gains over cross-entropy at 16 than at 256 expansions, implying CAT scales with test time compute.