# Learning Lean Feedback for Efficient Proof-Candidate Evaluation on GPUs

> Learned neural evaluators predict Lean 4 proof verdicts with 87.8% accuracy at 4.2x throughput, cutting GRPO training time by 31% without performance loss.

- **Source:** [arXiv](https://arxiv.org/abs/2610.21881)
- **Published:** 2026-10-17
- **Permalink:** https://picx.dev/p/GI32Pl
- **Whiteboard:** https://picx.dev/p/GI32Pl/image

## Summary

# 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**

| Data | Programs | Valid fraction |
|------|----------|----------------|
| Training corpus | 4.84M | 44.8% |
| In-house validation (miniF2F and ProofNet) | 27,210 | 38.9% |
| miniF2F benchmark candidates | 41,638 | 61.7% |
| ProofNet benchmark candidates | 27,294 | 9.0% |
| Combined benchmark (deduplicated) | 68,932 | 40.8% |

### Three Evaluator Models

**Table 2: Evaluator training settings**

| | Encoder | One-token | Feedback |
|---|---|---|---|
| **Backbone** | ModernBERT-large (395M) | Qwen3-8B | Qwen3-4B |
| **Pretraining task** | Predict masked tokens (30% masking) | Predict next token | Predict next token |
| **Supervised target** | Binary validity label | One true/false token | Source annotated with feedback |
| **Context (tokens)** | 8,192 | 32,768 | 32,768 |
| **Learning rate** | $2 \times 10^{-5}$ | $10^{-5}$ | $10^{-5}$ |
| **Batch size** | 64 | 8 | 8 |
| **Update steps** | 75,251 | 16,250 | 55,470 |

**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**

| Evaluator | Accuracy | Macro F1 | MCC | AUROC |
|-----------|----------|----------|-----|-------|
| Cascade, SC feedback stage @4/5 | **0.888** | **0.887** | **0.783** | — |
| Cascade, calibrated gate (0.82)† | 0.887 | 0.885 | 0.778 | — |
| Cascade: one-token → feedback | 0.878 | 0.877 | 0.772 | — |
| Cascade, FP8 feedback stage | 0.877 | 0.876 | 0.770 | — |
| Feedback 4B, 5-sample SC @4/5 | 0.874 | 0.873 | 0.762 | 0.919 |
| Feedback 4B | 0.851 | 0.851 | 0.733 | — |
| One-token 8B, calibrated (0.86)† | 0.831 | 0.831 | 0.683 | 0.905 |
| One-token 8B | 0.752 | 0.752 | 0.592 | 0.905 |
| ModernBERT-large | 0.586 | 0.563 | 0.372 | 0.862 |

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

### Transfer Across Provers

**Table 4: Accuracy by prover**

| Prover | Valid fraction | Feedback | One-token | Cascade |
|--------|---------------|----------|-----------|---------|
| Goedel-Prover-V2-8B | 0.530 | 0.867 | 0.819 | **0.893** |
| DeepSeek-Prover-V2-7B | 0.408 | 0.843 | 0.765 | **0.878** |
| Pythagoras-Prover-4B | 0.328 | 0.848 | 0.688 | **0.865** |

### Feedback Quality

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

| Metric | Overall | Valid | Invalid |
|--------|---------|-------|---------|
| Block F1, exact | 0.796 | 0.969 | 0.623 |
| Anchored block F1 | 0.795 | 0.969 | 0.621 |
| Token F1 | 0.852 | 0.983 | 0.721 |
| Error-presence agreement | 0.840 | 0.974 | 0.707 |

### Throughput

**Table 6: Neural vs. Lean throughput**

| Evaluator | Candidates/s | Seconds/candidate |
|-----------|-------------|-------------------|
| ModernBERT | 264 | 0.0038 |
| One-token 8B | 4.9 | 0.204 |
| Feedback 4B, no speculation | 0.73 | 1.37 |
| Feedback 4B + speculation | 3.27 | 0.306 |
| Cascade | 3.48 | 0.287 |
| Cascade, FP8 feedback stage | **3.59** | **0.279** |
| Lean REPL pool, 64 workers | 0.835 | 1.20 |

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**

| Checkpoint / reward source | Pass@1 (%) | Pass@32 (%) | Step time (s) |
|---------------------------|-----------|-------------|---------------|
| Initial checkpoint (shared) | 53.8 ± 0.6 | 72.8 ± 0.3 | — |
| GRPO, Lean-only, 60 s timeout | 62.4 ± 0.6 | 71.3 ± 0.8 | 1,050 |
| GRPO, hybrid rewards | 62.2 ± 0.8 | 72.4 ± 0.4 | 720 |
| GRPO, Lean-only, 13 s timeout | 59.8 ± 0.6 | 69.7 ± 1.1 | 720 |

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.

---

_Markdown view of https://picx.dev/p/GI32Pl, served by PicX — AI-generated visual whiteboard summaries of research papers._