Rethinking Supervision Granularity: Segment-Level Learning for LLM-Based Theorem Proving

• URL: http://arxiv.org/abs/2605.11905v1
• Date: Tue, 12 May 2026 10:18:28 GMT
• Title: Rethinking Supervision Granularity: Segment-Level Learning for LLM-Based Theorem Proving
• Abstract summary: Automated theorem proving with large language models in Lean 4 is commonly approached through either step-level tactic prediction with tree search or whole-proof generation.<n>These two paradigms represent opposite granularities for constructing supervised training data.<n>We propose segment-level supervision, a training data construction strategy that extracts locally coherent proof segments for training policy models.
• Score: 8.420305724549603
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Automated theorem proving with large language models in Lean 4 is commonly approached through either step-level tactic prediction with tree search or whole-proof generation. These two paradigms represent opposite granularities for constructing supervised training data: the former provides dense local signals but may fragment coherent proof processes, while the latter preserves global structure but requires complex end-to-end generation. In this paper, we revisit supervision granularity as a training set construction problem over proof trajectories and propose segment-level supervision, a training data construction strategy that extracts locally coherent proof segments for training policy models. We further reuse the same strategy at inference time to trigger short rollouts for existing step-level models. When trained with segment-level supervision on STP, LeanWorkbook, and NuminaMath-LEAN, the resulting policy models achieve proof success rates of 64.84%, 60.90%, and 66.31% on miniF2F, respectively, consistently outperforming both step-level and whole-proof baselines. Goal-aware rollout further improves existing step-level provers while reducing inference costs. It increases the proof success rate of BFS-Prover-V2-7B from 68.77% to 70.74% and that of InternLM2.5-StepProver from 59.59% to 60.33%, showing that appropriate supervision granularity better aligns model learning with proof structure and search. Code and models are available at https://github.com/NJUDeepEngine/SEG-ATP.

Related papers

• SLAI T-Rex: Full-Parameter Post-training of the DeepSeek-V4 Family on Ascend SuperPOD [91.71050339479261]
  This report presents an end-to-end optimization practice on the Ascend NPU SuperPOD.<n>We develop a hierarchical optimization framework spanning model-level parallelism, computation-communication orchestration, and low-level kernel execution.<n>The resulting system achieves 34.22% Model FLOPs Utilization (MFU) with a 2.93x improvement over the open-source baseline recipe.
  arXiv  Detail & Related papers  (2026-07-22T13:49:17Z)
• GRPO-VPS: Enhancing Group Relative Policy Optimization with Verifiable Process Supervision for Effective Reasoning [48.32628338889922]
  Group Relative Policy Optimization suffers from indiscriminate credit assignment for intermediate steps.<n>We introduce a model-free and verifiable process supervision via probing the model's belief in the correct answer.<n>This approach enables more targeted and sample-efficient policy updates.
  arXiv  Detail & Related papers  (2026-04-22T15:08:58Z)
• Goedel-Code-Prover: Hierarchical Proof Search for Open State-of-the-Art Code Verification [34.98335927187393]
  Large language models (LLMs) can generate plausible code but offer limited guarantees of correctness.<n>We propose a hierarchical proof search framework for automated code verification in Lean4.<n>We train Goedel-Code-Prover-8B, a single unified policy for both decomposition and completion.
  arXiv  Detail & Related papers  (2026-03-18T18:42:04Z)
• Answer First, Reason Later: Aligning Search Relevance via Mode-Balanced Reinforcement Learning [7.006180736433431]
  Building a search relevance model that achieves both low latency and high performance is a long-standing challenge in the search industry.<n>We propose a novel textbfAnswer-First, Reason Later (AFRL) paradigm.<n>This paradigm requires the model to output the definitive relevance score in the very first token, followed by a structured logical explanation.
  arXiv  Detail & Related papers  (2026-02-10T17:28:12Z)
• ProRAG: Process-Supervised Reinforcement Learning for Retrieval-Augmented Generation [54.071574153853994]
  ProRAG is a process-supervised reinforcement learning framework designed to integrate learned step-level supervision into the online optimization loop.<n>Our framework consists of four stages: (1) Supervised Policy Warmup to initialize the model with a structured reasoning format; (2) construction of an MCTS-based Process Reward Model (PRM) to quantify intermediate reasoning quality; (3) PRM-Guided Reasoning Refinement to align the policy with fine-grained process preferences; and (4) Process-Supervised Reinforcement Learning with a dual-granularity advantage mechanism.
  arXiv  Detail & Related papers  (2026-01-29T16:04:59Z)
• DiRL: An Efficient Post-Training Framework for Diffusion Language Models [54.405206032785706]
  Diffusion Language Models (dLLMs) have emerged as promising alternatives to Auto-Regressive (AR) models.<n>Existing methods suffer from computational inefficiency and objective mismatches between training and inference.<n>We introduce DiRL, an efficient post-training framework that tightly integrates FlexAttention-accelerated blockwise training with LMDeploy-optimized inference.
  arXiv  Detail & Related papers  (2025-12-23T08:33:19Z)
• SPARK: Stepwise Process-Aware Rewards for Reference-Free Reinforcement Learning [39.1720897614261]
  Process reward models (PRMs) that provide dense, step-level feedback have shown promise for reinforcement learning.<n>We propose SPARK: a three-stage framework where in the first stage a generator model produces diverse solutions and a verifier model evaluates them.<n>We show that aggregating multiple independent verifications at the step level produces training data for process reward models that surpass ground-truth outcome supervision.
  arXiv  Detail & Related papers  (2025-12-02T21:30:47Z)
• Revolutionizing Reinforcement Learning Framework for Diffusion Large Language Models [49.911784762244814]
  TraceRL is a trajectory-aware reinforcement learning framework for diffusion language models (DLMs)<n>We derive a series of state-of-the-art diffusion language models, namely TraDo.<n>TraDo-8B-Instruct achieves relative accuracy improvements of 6.1% over Qwen2.5-7B-Instruct and 51.3% over Llama3.1-8B-Instruct on mathematical reasoning benchmarks.
  arXiv  Detail & Related papers  (2025-09-08T17:58:06Z)
• CLGRPO: Reasoning Ability Enhancement for Small VLMs [4.551310348498266]
  Small Vision Language Models (SVLMs) generally refer to models with parameter sizes less than or equal to 2B.<n>This paper proposes a post-training optimization paradigm called the Incremental Training Strategy to enhance the reasoning ability of SVLMs.<n> Experimental results demonstrate that our method significantly improves the reasoning ability of 1B SVLM.
  arXiv  Detail & Related papers  (2025-06-22T14:32:15Z)
• TemplateRL: Structured Template-Guided Reinforcement Learning for LLM Reasoning [56.250782426571526]
  Reinforcement learning (RL) has emerged as an effective paradigm for enhancing model reasoning.<n>We propose a structured template-guided RL framework that augments policy optimization with explicit template guidance.<n>Our approach first constructs a problem-solving template library via MCTS on a small seed set, then seamlessly integrates this high-level structured guidance into RL training.
  arXiv  Detail & Related papers  (2025-05-21T16:06:10Z)
• ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis [50.020850767257095]
  We propose ProofAug, a procedure that equips LLMs with automation methods at various granularities.<n>Our method is validated on the miniF2F benchmark using the open-source deep-math-7b-base model and the Isabelle proof assistant.<n>We also implement a Lean 4 version of ProofAug that can improve the pass@1 performance of Kimina-Prover-seek-Distill-1.5B from 44.3% to 50.4%.
  arXiv  Detail & Related papers  (2025-01-30T12:37:06Z)
• Efficient Stagewise Pretraining via Progressive Subnetworks [53.00045381931778]
  The prevailing view suggests that stagewise dropping strategies, such as layer dropping, are ineffective when compared to stacking-based approaches. This paper challenges this notion by demonstrating that, with proper design, dropping strategies can be competitive, if not better, than stacking methods. We propose an instantiation of this framework - Random Part Training (RAPTR) - that selects and trains only a random subnetwork at each step, progressively increasing the size in stages.
  arXiv  Detail & Related papers  (2024-02-08T18:49:09Z)

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.