重新思考监督粒度：面向LLM定理证明的段级学习

在Lean 4中用大语言模型做自动定理证明，通常要么采用结合树搜索的步级战术预测，要么采用整证明生成。这两种范式代表了构建监督训练数据的两个相反粒度：前者提供稠密的局部信号，但可能割裂连贯的证明过程；后者保留全局结构，却需要复杂的端到端生成。本文将监督粒度重新视为证明轨迹上的训练集构建问题，提出段级监督这一训练数据构建策略，抽取局部连贯的证明片段来训练策略模型。我们进一步在推理时复用同一策略，为现有步级模型触发短的rollout。在STP、LeanWorkbook和NuminaMath-LEAN上用段级监督训练后，所得策略模型在miniF2F上分别取得64.84%、60.90%和66.31%的证明成功率，持续优于步级和整证明两类基线。目标感知rollout在降低推理成本的同时进一步提升现有步级证明器。它将BFS-Prover-V2-7B的证明成功率从68.77%提升到70.74%，将InternLM2.5-StepProver从59.59%提升到60.33%，表明合适的监督粒度能更好地使模型学习与证明结构及搜索相对齐。代码和模型已发布于 https://github.com/NJUDeepEngine/SEG-ATP。