Learning Lean Feedback for Efficient Proof-Candidate Evaluation on GPUs

Training language models for formal theorem proving requires large numbers of verifier calls. Slow checks and timeouts can 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 model that annotates proof attempts with predicted goal states and error messages. To evaluate them, we collect a 68,932-program benchmark using three public provers. A two-stage evaluator that screens candidates with a classifier and scores its positive predictions with the feedback model reaches 87.8\% accuracy on this benchmark. Speculative decoding triples feedback-generation throughput, enabling the combined evaluator to process 3.5 candidates per second on one H100 GPU. This is 4.2$\times$ the throughput of our CPU baseline, the 64-worker Lean pool that reuses loaded environments. Combining Lean verdicts with evaluator predictions yields hybrid rewards that shorten GRPO training steps by approximately 31\%. After one epoch, training with hybrid rewards achieves 62.2\% pass@1 on all 488 miniF2F problems, compared with 62.4\% for training with Lean-only rewards---preserving essentially the same final prover performance while substantially reducing training time.