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

微调后的大语言模型（LLM）显著推进了自动定理证明（ATP），但它们通常被部署为树搜索中的引导策略，而非单次生成。近期工作表明，交叉熵对用于聚合、过滤等平面搜索策略的 LLM 而言是次优的，并提出了新的损失函数来纠正这种错位。把这种对齐扩展到树搜索更具挑战性：证明发现依赖于经过轨迹外状态的探索与恢复，而监督演示无法揭示这些状态。我们通过对策略引导搜索的抽象，把计算对齐训练（Compute-Aligned Training, CAT）扩展到该设定，推导出可处理、有轨迹支撑的损失。除这些搜索感知损失外，我们还引入一个搜索无关的均匀分配（UA）损失，它计入预算但不指定具体搜索。两者都对逐策略（per-tactic）交叉熵梯度诱导标量权重。我们刻画了轨迹外行为如何影响搜索感知权重，包括在大预算下近似误差消失的条件。在 Lean 基准上，两种方法在六种搜索策略下都取得高于交叉熵的观测证明成功率，其中单一共享 UA 适配器即获得强劲结果。预算扫描显示，16 次扩展时相对交叉熵的增益大于 256 次扩展时，意味着 CAT 随测试时算力而扩展。