定理证明训练数据不再靠堆量：从已验证证明里挖出500道边界难题，两个证明器都涨分
核心概要
形式定理证明的强化学习受限于高质量难题稀缺：现有Lean题目要么已被证明器解出，要么信息量太低。ProofFrontier从已有Lean已验证的定理–证明对出发，保持原定理陈述不变，只遮住证明结构中的关键局部节点，让证明器重新发现中间推理，再用基础证明器的通过率筛出“原则上可解、但不易解”的边界难题。用GRPO在500道合成任务上训练后，DeepSeek-Prover-V2-7B与Goedel-Prover-V2-8B在miniF2F、ProofNet和PutnamBench上均较各自基础模型提升。
深度剖析
训练形式定理证明器所需的高难度题目，可以从已有证明里“遮”出来，而不必新造定理陈述。 此前的Lean题库要么已被当前证明器解出、学习压力很小，要么远超其能力、只产生失败轨迹，因此缺少既保证可解又足够难的完整任务。 在miniF2F上，DeepSeek-Prover-V2-7B经ProofFrontier训练后由70.49升至75.41，Goedel-Prover-V2-8B由77.87升至81.15，两者采样预算均为32，结果由Lean验证。
做法是把一条已验证的Lean证明解析成局部证明图，找出结构上关键的节点，再按可见程度生成一族提示。 被遮住的证明体从不作为填空目标，遮罩只控制向证明器暴露多少证明结构信息，定理陈述始终不变。 节点按桥接、使用和变化三项启发式打分，可见字段被渲染成简短提示；难度不由遮罩等级预设，而由基础证明器在Lean验证下的通过率实测标定。
筛选环节只保留基础证明器通过率落在每16次尝试中多于3次、少于5次的任务。 这一区间对应“已不平凡、但验证器反馈仍有信息量”的难度带，训练数据因此集中在证明器的能力边界附近。 主实验使用500道筛选后的边界难题；在miniF2F上，100道任务把基础分从70.49提到72.71，250道到74.38，500道到75.41。
启示与展望
演示范围限于Lean中的形式定理证明，训练任务取自开源数据集Goedel-LM/SFT_dataset_v2中的已验证定理–证明对，评测覆盖miniF2F、ProofNet和PutnamBench，主实验训练500道筛选任务，评测时不提供任何ProofFrontier提示或参考证明。
证明结构遮罩基于源码级启发式，结构上重要的节点未必对应某个证明器真正困难的推理步骤；能力感知筛选依赖具体模型，换基础证明器、解码预算或验证器设置都可能需要重新标定；辅助的证明相似度奖励可能把模型引向参考证明轨迹，从而低估其他有效证明。