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

📄 arXiv: 2605.11905v1 📥 PDF

作者: Shuo Xu, Jiakun Zhang, Junyu Lai, Chun Cao, Jingwei Xu

分类: cs.AI

发布日期: 2026-05-12

备注: 22 pages, 4 figures, 6 tables

🔗 代码/项目: GITHUB

💡 一句话要点

提出段级监督以解决大语言模型定理证明中的训练数据构建问题

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 定理证明 大语言模型 段级监督 自动化推理 机器学习

📋 核心要点

  1. 现有的步骤级和整体证明生成方法在训练数据构建上存在明显不足，导致模型学习与证明结构不匹配。
  2. 论文提出段级监督，通过提取局部连贯的证明段来构建训练数据，从而提高模型的学习效率和效果。
  3. 实验结果显示，段级监督训练的模型在多个基准测试中均表现优异，成功率显著高于传统方法。

📝 摘要（中文）

在Lean 4中，使用大语言模型进行自动定理证明通常通过步骤级策略预测或整体证明生成来实现。这两种方法在构建监督训练数据时存在对立的粒度：前者提供密集的局部信号，但可能会破坏连贯的证明过程；后者则保留全局结构，但需要复杂的端到端生成。本文重新审视监督粒度，提出段级监督作为一种训练数据构建策略，从证明轨迹中提取局部连贯的证明段用于训练策略模型。实验结果表明，使用段级监督训练的模型在miniF2F上的证明成功率分别为64.84%、60.90%和66.31%，显著优于步骤级和整体证明基线。

🔬 方法详解

问题定义：本文旨在解决现有大语言模型在定理证明中训练数据构建的粒度问题。现有方法在步骤级和整体生成之间存在权衡，导致模型学习效果不佳。

核心思路：提出段级监督作为一种新的训练数据构建策略，旨在提取局部连贯的证明段，以更好地对齐模型学习与证明结构。

技术框架：整体架构包括数据提取、模型训练和推理三个主要阶段。在数据提取阶段，从证明轨迹中提取局部段落；在模型训练阶段，使用提取的段落进行策略模型训练；在推理阶段，利用相同策略触发短期回滚。

关键创新：最重要的创新在于段级监督的引入，这一策略有效解决了现有方法的局限性，使得模型能够在保持全局结构的同时，利用局部信息进行学习。

关键设计：在模型训练中，采用特定的损失函数来优化段级监督的效果，同时在网络结构上进行了调整，以适应局部段落的输入特性。

🖼️ 关键图片

fig_0
fig_1
fig_2

📊 实验亮点

实验结果显示，使用段级监督训练的模型在miniF2F上取得了64.84%的成功率，LeanWorkbook和NuminaMath-LEAN分别为60.90%和66.31%。此外，目标感知回滚进一步提升了现有步骤级证明器的性能，成功率分别从68.77%提升至70.74%，从59.59%提升至60.33%。

🎯 应用场景

该研究的潜在应用领域包括自动定理证明、形式化验证和智能合约等。通过提高定理证明的效率和准确性，能够在软件验证、数学证明等领域产生实际价值，推动相关技术的发展与应用。

📄 摘要（原文）

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.