Research map / Large language models / Reasoning and chain of thought

Process-Verified Reinforcement Learning for Theorem Proving via Lean

ICLR 2026 · Large language models › Reasoning and chain of thought · approach: RL with verifiable rewards for reasoning · 0 citations (OpenAlex)

Read the paperCheck your idea against 108,967 papers

AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.

Uses the Lean 4 proof assistant as a symbolic process oracle, assigning first-error-propagated tactic-level rewards plus outcome rewards to the first token of each tactic inside a GRPO-style objective, improving STP-Lean and DeepSeek-Prover-V1.5 on MiniF2F and ProofNet.

Problem

Outcome-only RLVR for theorem proving gives only a sparse binary signal, while Lean's elaboration provides fine-grained tactic-level feedback that is unused during RL training.

Approach

Treat Lean's per-tactic error log as a process reward: tactics before the first error get a mild penalty d1, tactics from the first error onward get a stronger penalty d2 (first-error propagation), and the resulting tactic advantage is added to the normalized outcome advantage only at each tactic's first token, with no PRM or value model.

Key results

• STP-Lean + Outcome+Tactic RL reaches 59.2% pass@64 on MiniF2F-Test vs 56.7% for the STP-Lean baseline and 57.9% for outcome-only GRPO.
• On ProofNet-Test, STP-Lean + Ours achieves 18.6% pass@32 vs 17.4% for outcome-only GRPO, and 19.0% pass@64 (equal to GRPO).
• Removing first-error propagation drops MiniF2F pass@64 from 59.2% to 58.2% and ProofNet pass@32 from 18.6% to 17.4%.

Surprising findings

• Collapsing the two penalties into a single value (d1=d2) gives the best MiniF2F pass@32 (57.7%) but lower ProofNet results, so the gain is not uniform across benchmarks.
• Assigning tactic advantage to all tokens, or to entropy-selected tokens, did not improve over outcome-only training.

Limitations

• Tactic penalties d1 and d2 are fixed hand-set values and reported as sensitive across models and datasets.
• Evaluated only with pure non-CoT Lean proofs; unclear how to design such rewards for long-form reasoning.
• Gains are small and often within standard deviations; some settings show drops (e.g., tactic-only, ProofNet pass@64).

Experimental setup

Datasets: STP dataset MiniF2F ProofNet

Benchmarks: MiniF2F-Test ProofNet-Test

Metrics: pass@32 pass@64

Baselines: STP-Lean DeepSeek-Prover-V1.5-SFT DeepSeek-Prover-V1.5-RL Goedel-Prover-SFT Lean-STaR InternLM2-Math-Plus-7B InternLM2.5-StepProver RMaxTS GRPO outcome-only

Builds on: GRPO DAPO PPO potential-based reward shaping

Closest papers by meaning

• DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search (ICLR 2025 · similarity 0.92)
• Distilling LLM Feedback for Lean Theorem Proving (NeurIPS 2026 · similarity 0.90)
• Reviving DSP for Advanced Theorem Proving in the Era of Reasoning Models (NeurIPS 2025 · similarity 0.88)
• From Verifiable Dot to Reward Chain: Harnessing Verifiable Reference-based Rewards for Reinforcement Learning of Open-ended Generation (ICLR 2026 · similarity 0.87)
• Rewarding Progress: Scaling Automated Process Verifiers for LLM Reasoning (ICLR 2025 · similarity 0.87)
• Subgoal-based Demonstration Learning for Formal Theorem Proving (ICML 2024 · similarity 0.87)