重新思考监督粒度：基于 LLM 的定理证明中的分段学习

本文针对大语言模型在 Lean 4 中的自动定理证明任务，重新审视了监督粒度的构建问题。现有方法多采用步级策略预测或整篇证明生成，前者信号密集但割裂过程，后者保留全局结构但生成困难。作者提出“分段级监督”策略，提取局部连贯的证明片段用于训练策略模型，并在推理阶段复用该策略触发短程 rollout。实验表明，该方法在多个数据集上训练的模型在 miniF2F 基准测试中成功率显著优于步级和整篇基线，同时降低了推理成本，证明了合适的监督粒度能更好地对齐模型的推理学习与证明结构。