Direct Optimization of Generators for Search：把 Lean 定理证明模型的训练目标直接对齐到有限预算搜索成功率

该工作指出，LLM theorem prover 通常在 tree search 中部署，但训练仍使用逐 token cross-entropy，目标与有限预算下的搜索成功并不一致。作者将 Compute-Aligned Training 扩展到 policy-guided search，推导出基于 trace 的 search-aware losses，并提出无需指定具体搜索策略的 uniform-allocation loss。Lean 4 / LeanDojo 实验显示，两类目标在 458 个 held-out theorem、6 种 search strategy 上均优于普通 cross-entropy；而且相对收益在更紧的 expansion budget 下更明显。