Direct Optimization of Generators for Search in Automated Theorem Proving.

arXiv:2609.25575v1 Announce Type: new Abstract: 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