Direct Optimization of Generators for Search in Automated Theorem Proving

Compute-Aligned Training (CAT) extends policy-guided search alignment to automated theorem proving by deriving tractable, trace-supported losses that account for off-trace states. The method introduces a search-agnostic uniform-allocation loss to manage computational budgets, applying scalar weights to per-tactic cross-entropy to optimize LLMs for tree search rather than single-attempt generation.