自动定理证明中搜索生成器的直接优化

中文摘要 AI 辅助

微调的大型语言模型（LLMs）显著推进了自动定理证明（ATP），但通常被部署为树搜索中的引导策略，而非用于单次尝试生成。近期工作表明，对于在平坦搜索策略（如聚合或过滤）中使用的LLM，交叉熵是次优的，并且该工作已开发新的损失函数来纠正这种错位。将这种对齐扩展到树搜索更具挑战性：证明发现依赖于通过监督演示未揭示的偏离轨迹状态进行探索和恢复。我们通过策略引导搜索的抽象将计算对齐训练（CAT）扩展到该设置，推导出可处理的、支持轨迹的损失。除这些搜索感知损失外，我们引入了一种搜索无关的均匀分配（UA）损失，该损失在不指定具体搜索的情况下考虑预算。两者都在每个策略的交叉熵梯度上引入标量权重。我们刻画了偏离轨迹行为如何影响搜索感知权重，包括在大预算下近似误差消失的条件。在Lean基准上，两种方法在六种搜索策略中均实现了比交叉熵更高的观察证明成功率，且单个共享UA适配器取得了强劲结果。预算扫描显示，在16次扩展时比交叉熵的增益大于256次扩展时，表明CAT随测试时计算规模扩展。

英文摘要

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.

发表机构

• University of Michigan（密歇根大学）

机构由 AI 辅助整理，请以论文原文为准。