Neural evaluators speed up proof checking on GPUs by four times
Learning Lean Feedback for Efficient Proof-Candidate Evaluation on GPUs
Machine Learning
Summary
Checking whether computer-generated math proofs are correct can be very slow, making some proof-finding computers wait a lot. The authors trained neural networks to quickly predict if a proof will be accepted and to provide helpful feedback, running efficiently on graphics processors. Their combined approach is much faster than traditional methods and helps train proof-writing AI systems faster without losing accuracy. This can make automated theorem proving more practical and efficient.
What this means in practice
- •For software verification teams: Accelerate formal proof verification inside software development pipelines by using fast neural feedback models on GPUs to reduce waiting times.
- •For ai system builders: Speed up training of AI systems that generate formal proofs by combining neural evaluators with traditional verifiers to improve feedback throughput.
Authors
Lazar Milikic, Etienne Bamas, Emmanuel Abbe, Viktor Kunčak
Abstract
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 potentially correct proofs. We train neural evaluators to predict Lean 4 verdicts and compiler feedback on GPUs using 4.84M labelled programs. We compare two validity classifiers with a feedback model that annotates proof attempts with predicted goal states and error messages. A two-stage evaluator that screens candidates with a classifier and scores its positive predictions with the feedback model reaches 87.8% accuracy in predicting whether Lean accepts a candidate proof, evaluated on a 68,932-program benchmark collected from public provers. The combined evaluator processes 3.5 candidates per second on one H100, 4.2x the throughput of our 64-worker Lean baseline with environment reuse. Finally, we combine our evaluator with Lean verdicts to obtain a hybrid reward system that shortens GRPO training steps by approximately 31%. After one GRPO epoch with hybrid rewards, the prover achieves nearly the same miniF2F pass@1 as with Lean-only rewards (62.2% versus 62.4%) and a pass@32 of 72.4% versus 71.3%.