Process-Verified Reinforcement Learning for Theorem Proving via Lean

• URL: http://arxiv.org/abs/2606.20068v1
• Date: Thu, 18 Jun 2026 10:40:55 GMT
• Title: Process-Verified Reinforcement Learning for Theorem Proving via Lean
• Abstract summary: We show that the Lean proof assistant itself can serve as a symbolic process oracle.<n>Experiments with LeanLean and DeepSeek-V1.5 show that tactic-level supervision outperforms outcome-only baselines in most settings.
• Score: 47.294932573003756
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: While reinforcement learning from verifiable rewards (RLVR) typically has relied on a single binary verification signal, symbolic proof assistants in formal reasoning offer rich, fine-grained structured feedback. This gap between structured processes and unstructured rewards highlights the importance of feedback that is both dense and sound. In this work, we demonstrate that the Lean proof assistant itself can serve as a symbolic process oracle, supplying both outcome-level and fine-grained tactic-level verified feedback during training. Proof attempts are parsed into tactic sequences, and Lean's elaboration marks both locally sound steps and the earliest failing step, yielding dense, verifier-grounded credit signals rooted in type theory. We incorporate these structured rewards into a GRPO-style reinforcement learning objective with first-error propagation and first-token credit methods that balances outcome- and process-level advantages. Experiments with STP-Lean and DeepSeek-Prover-V1.5 show that tactic-level supervision outperforms outcome-only baselines in most settings, delivering improvements on benchmarks such as MiniF2F and ProofNet. Beyond empirical gains, our study highlights a broader perspective: symbolic proof assistants are not only verifiers at evaluation time, but can also act as process-level reward oracles during training. This opens a path toward reinforcement learning frameworks that combine the scalability of language models with the reliability of symbolic verification for formal reasoning.

Related papers

• DHRCL:Training Code LLMs with Dense Hierarchical Rewards and Curriculum Learning [15.421698703970167]
  We propose DHRCL, a reinforcement learning framework with Dense Hierarchical Rewards and Curriculum Learning.<n>DHRCL decomposes feedback into syntax validation, execution success, unit-test pass rate, and AST-based structural similarity.<n>We evaluate DHRCL across Qwen3-4B, Qwen3-8B, and Qwen3-14B backbones, showing that its advantage remains consistent as model capacity increases.
  arXiv  Detail & Related papers  (2026-07-29T04:16:33Z)
• Verifiable Process Rewards for Agentic Reasoning [21.195739597726142]
  Reinforcement learning from verifiable rewards (RLVR) has improved the reasoning abilities of large language models (LLMs)<n>Most existing approaches rely on sparse outcome-level feedback.<n>We propose Verifiable Process Rewards (VPR), a framework that converts such oracles into dense turn-level supervision for reinforcement learning.
  arXiv  Detail & Related papers  (2026-05-11T10:30:53Z)
• Discovering Process-Outcome Credit in Multi-Step LLM Reasoning [3.584086358722852]
  Reinforcement Learning (RL) serves as a potent paradigm for enhancing reasoning capabilities in Large Language Models (LLMs)<n>We propose a novel framework designed to provide continuous reward signals.<n>Our model exhibits superior out-of-distribution robustness, demonstrating promising zero-shot transfer capabilities to unseen and challenging reasoning tasks.
  arXiv  Detail & Related papers  (2026-02-01T05:44:09Z)
• Refinement Provenance Inference: Detecting LLM-Refined Training Prompts from Model Behavior [58.751981587234916]
  This paper formalizes the Refinement Provenance Inference (RPI) audit task as Refinement Provenance Inference (RPI)<n>We propose RePro, a logit-based framework that fuses teacher-forced likelihood features with logit-ranking signals.<n>During training, RePro learns a transferable representation via shadow fine-tuning, and uses a lightweight linear head to infer provenance on unseen victims without training-data access.
  arXiv  Detail & Related papers  (2026-01-05T10:16:41Z)
• Look As You Think: Unifying Reasoning and Visual Evidence Attribution for Verifiable Document RAG via Reinforcement Learning [55.232400251303794]
  Look As You Think (LAT) is a reinforcement learning framework that trains models to produce verifiable reasoning paths with consistent attribution.<n>LAT consistently improves the vanilla model in both single- and multi-image settings, yielding average gains of 8.23% in soft exact match (EM) and 47.0% in IoU@0.5.
  arXiv  Detail & Related papers  (2025-11-15T02:50:23Z)
• Veri-R1: Toward Precise and Faithful Claim Verification via Online Reinforcement Learning [53.05161493434908]
  Claim verification with large language models (LLMs) has recently attracted growing attention, due to their strong reasoning capabilities and transparent verification processes.<n>We introduce Veri-R1, an online reinforcement learning framework that enables an LLM to interact with a search engine and to receive reward signals that explicitly shape its planning, retrieval, and reasoning behaviors.<n> Empirical results show that Veri-R1 improves joint accuracy by up to 30% and doubles the evidence score, often surpassing its larger-scale model counterparts.
  arXiv  Detail & Related papers  (2025-10-02T11:49:48Z)
• Learning a Dense Reasoning Reward Model from Expert Demonstration via Inverse Reinforcement Learning [50.20267980386502]
  We learn a dense, token-level reward model for process supervision directly from expert demonstrations.<n>The learned reasoning reward serves two complementary roles: (i) it provides step-level feedback to optimise a reasoning policy during training; and (ii) it functions at inference as a critic to rerank sampled traces under fixed compute budgets.
  arXiv  Detail & Related papers  (2025-10-02T09:55:26Z)
• AURORA: Augmented Understanding via Structured Reasoning and Reinforcement Learning for Reference Audio-Visual Segmentation [113.75682363364004]
  AURORA is a framework designed to enhance genuine reasoning and language comprehension in reference audio-visual segmentation.<n>AURORA achieves state-of-the-art performance on Ref-AVS benchmarks and generalizes effectively to unreferenced segmentation.
  arXiv  Detail & Related papers  (2025-08-04T07:47:38Z)
• Reinfier and Reintrainer: Verification and Interpretation-Driven Safe Deep Reinforcement Learning Frameworks [36.730973051834376]
  We propose a verification-driven interpretation-in-the-loop framework Reintrainer to develop trustworthy DRL models.<n>In each iteration, this framework measures the gap between the on-training model and predefined properties using formal verification.<n>Reinfier features breakpoints searching and verification-driven interpretation, associated with a concise constraint-encoding language DRLP.
  arXiv  Detail & Related papers  (2024-10-19T15:03:26Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.