Learning Lean Feedback for Efficient Proof-Candidate Evaluation on GPUs

Lazar Milikic, Etienne Bamas, Emmanuel Abbe +1

Training language models for formal theorem proving requires large numbers of verifier calls. Slow checks and timeouts often leave GPUs waiting and withhold rewards from potentiall…