SOURCE-LINKED INTELLIGENCE

Direct Optimization of Generators for Search in Automated Theorem Proving

arXiv · AI, language, vision and robotics · article · Sep 22, 2026 · UTC

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-

Read original source ↗ Open in workspace

recordType

paper

region

Global