Direct Optimization of Generators for Search in Automated Theorem Proving

Adam Ousherovitch, Ambuj Tewari

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-…