Learning Lean Feedback for Efficient Proof-Candidate Evaluation on GPUs

Summary (Overview)

• The paper presents learned neural evaluators that predict Lean 4 verifier verdicts and compiler feedback on GPUs, reducing the computational bottleneck of proof verification in formal theorem proving.
• A two-stage cascade evaluator combining a one-token validity classifier with a feedback model achieves 87.8% accuracy in predicting Lean acceptance on a 68,932-program benchmark, processing 3.5 candidates per second on a single H100 GPU—4.2× faster than a 64-worker Lean baseline.
• The authors introduce a hybrid reward protocol for GRPO training that runs Lean and the learned evaluator concurrently, shortening training steps by ~31% while achieving nearly identical miniF2F pass@1 (62.2% vs. 62.4%) and better pass@32 preservation (72.4% vs. 71.3%) compared to Lean-only rewards.
• A large 4.84M-program compiler-labelled training corpus and a 68,932-program evaluation benchmark are released publicly, along with model checkpoints.

Introduction and Theoretical Foundation

Background and Motivation

Formal theorem proving with proof assistants like Lean provides automatically checked training signals for language models generating formal proofs. However, checking candidates at scale creates substantial computational workloads:

• A 64-worker Lean pool takes ~420 s to score 1,024 candidate proofs with a 60 s timeout—about 40% of a 1,050 s training step
• Timeouts withhold rewards from potentially correct proofs: 58.1% of resolved timeouts are valid proofs
• GPUs often sit idle waiting for CPU-bound verification results

Theoretical Basis

The paper frames the problem as a trade-off between evaluation speed and verdict accuracy when predicting Lean's response to candidate proofs. The key insight is that learned predictions can supplement exact checks when verification is slow, without requiring a new reward signal or search strategy.

Three main contributions:

1. Fast GPU evaluation with measured accuracy–cost trade-off (87.8% accuracy, 3.5 candidates/s)
2. Hybrid rewards for GRPO training (~31% shorter steps, preserved performance)
3. Dataset and benchmark for learned proof evaluation (4.84M training programs, 68,932 benchmark candidates)

Methodology

Dataset Construction

The training corpus combines public Lean proofs with additional attempts to increase invalid examples:

• Sources: NuminaMath-LEAN, Goedel-Prover SFT corpus, APRIL proof-repair traces
• A Qwen3-8B model is fine-tuned on valid proofs, then used to sample further attempts
• Lean v4.15.0 checks every attempt, providing verdicts and feedback
• Final corpus: 4.84M programs, 44.8% valid

Table 1: Training, validation, and benchmark data

Three Evaluator Models

Table 2: Evaluator training settings

Verdict classifiers:

• ModernBERT-large encoder: predicts validity in one forward pass; context-limited to 8,192 tokens (first 2,048 + last 6,144)
• One-token model (Qwen3-8B): outputs a single true/false token; normalized probabilities give a validity score in [0,1]

Feedback model (Qwen3-4B): Generates a feedback trace—the input program annotated with predicted goal states and error messages inserted as Lean comments. The verdict rule: predict invalid if the trace contains an error marker, ends with an incomplete proof-state block, or is cut off at the output limit without an EOS token.

Cascade architecture: The one-token model acts as a gate (threshold 0.5); candidates passing the gate proceed to the feedback model. Both must accept for the cascade to accept.

Self-consistency (SC): Samples five traces at temperature 0.8; accepts if ≥4 predict validity.

Empirical Validation / Results

Prediction Accuracy

Table 3: Verdict prediction on the full evaluation benchmark

†Threshold selected on in-house validation data; other thresholds are 0.5.

Transfer Across Provers

Table 4: Accuracy by prover

Feedback Quality

Table 5: Predicted feedback vs. Lean annotations (2,004 programs)

Throughput

Table 6: Neural vs. Lean throughput

Key speedup techniques:

• Speculative decoding (drafting 8 tokens at a time): 3.04× throughput increase, 99.2% verdict agreement
• FP8 quantization: accuracy 0.852 vs. 0.851 (BF16), 98.3% verdict agreement

GRPO Training Results

Table 7: Prover performance and training time

A second seed of hybrid training confirms robustness: 62.7 ± 0.7% pass@1 and 72.1 ± 0.6% pass@32.

Reward Hacking Analysis

The cascade's accuracy drops from 87.9% (step 25) to 81.7% (step 250) as the policy learns to exploit evaluator errors. False-positive rate rises from 17.8% to 28.9%. Weaker evaluators degrade far more severely: by step 250, false-positive rates reach 74.1% (one-token) and 99.6% (ModernBERT).

Theoretical and Practical Implications

Key Findings

1. Learned evaluation is viable: The cascade achieves 87.8% accuracy with 4.2× throughput over Lean, demonstrating that neural evaluators can serve as effective approximate verifiers.

2. Hybrid rewards preserve performance: Running Lean and learned evaluators concurrently shortens training steps by 31% while maintaining pass@1 and better preserving pass@32 than Lean-only training.

3. Timeout reduction alone is insufficient: At the same scoring time (90 s/batch), the 13 s Lean-only baseline performs worse (59.8% vs. 62.2% pass@1), showing that learned predictions add value beyond simply shortening verification timeouts.

4. Feedback quality varies by validity: The model predicts valid-proof feedback much more accurately (Block F1 0.969) than invalid-proof diagnostics (0.623), limiting its use for proof repair.

5. Reward hacking is manageable: The cascade shows bounded accuracy degradation during training, suggesting it is robust enough for practical use in RL training.

Practical Applications

• Accelerated RL training for theorem-proving language models
• Candidate ranking: On ProofNet, checking one candidate per pool recovers valid proofs in 57.2% of pools (vs. 47.9% random), using only 3.7% of compilation calls
• Reward recovery: The cascade accepts 80.1% of valid proofs that Lean would time out on

Conclusion

The paper demonstrates that learned Lean evaluators can provide fast, approximate verdicts and feedback for candidate proofs, enabling significant acceleration of GRPO training without sacrificing final performance. The cascade reaches 87.8% accuracy at 3.5 candidates per second on one H100 GPU, and hybrid rewards reduce training step time by ~31% while preserving miniF2F performance.

Future directions implied by the work:

• Improving feedback prediction for invalid proofs (error diagnosis)
• Mitigating reward hacking through better evaluator robustness
• Applying learned evaluation to other proof assistants and verification tasks
• Scaling to larger models and more diverse proof corpora

The datasets, model checkpoints, and project repository are publicly available on Hugging Face and GitHub.