失败的证明不再被丢弃：7B模型把Isabelle证明成功率推到73.8%
核心概要
HybridProver把整段证明生成与逐步策略生成接在同一条流水线上：整段模型先给出候选证明，未通过Isabelle检查的候选被抽成保留高层结构的证明骨架，再由策略模型与Sledgehammer逐个子目标补全。在Isabelle版miniF2F的244道测试题上，该流程取得73.8%的成功率，高于此前Isabelle系统的最好成绩61.9%。两个7B规模模型经监督微调与以Isabelle验证为奖励的强化学习训练，说明轻量模型也能生成Isabelle/HOL证明。
深度剖析
整段证明生成与逐步策略生成被放进同一条流水线，失败的整段候选不再直接丢弃，而是转成可复用的中间结构继续修补。 此前两类方法基本各自独立使用：整段合成擅长高层规划却在细节上易错，策略生成擅长局部步骤却缺少全局结构。 在Isabelle版miniF2F的244道测试题上，整段合成模型单独为45.9%，策略生成模型单独为39.3%，两者简单取并集为49.6%，接入骨架细化后升到71.3%，完整流程为73.8%。
流水线以证明骨架作为中间表示，把高层规划与低层推理分开，再在骨架内逐个子目标补全。 骨架由整段模型自己生成的候选证明机械地构造，而不是像DSP那样由另一个模型从非形式化证明提示生成。 骨架构造时逐个检查子目标，把其余子目标的证明替换为sorry，保留正确的局部步骤、只把失败处留作待补；这些骨架先经Isabelle检查剔除结构无效者，多数骨架能通过，在不填具体策略时骨架的成功率可达90%。
两个7B规模模型在优化后的Isabelle数据上做监督微调，再用Isabelle验证信号做强化学习。 训练数据取自Isabelle标准库与Archive of Formal Proofs，并按Isar与apply-style两种证明风格分开，分别对应整段合成与策略生成两个阶段。 整段模型在Isar数据上训练、策略模型在apply-style数据上训练，均用LoRA微调；强化学习采用GRPO，以通过验证得1.0、语法有效但验证失败得0.2、无效输出得0.0、含sorry等模式扣0.2的奖励，训练数据为优化数据集的1%随机子集。
启示与展望
演示范围是Isabelle/HOL上的miniF2F测试集，评测使用128个候选证明的采样规模，训练数据全部来自AFP与STD，miniF2F只用于评测。作者提出的下一步是把更先进的证明搜索接入策略生成阶段，并在定义好的AFP评测集上考察更广的Isabelle/HOL领域，同时开发更易用的集成系统。
作者指出当前消融没有固定其他因素，因此改进归因于整个后训练流程而非监督微调或强化学习中的某一阶段。骨架细化阶段的搜索策略较简单，子目标增多时细化与评测效率下降、计算开销上升；流程依赖Isabelle作为验证预言机，在大量候选证明时带来延迟与扩展性瓶颈；模型在既有证明语料上训练，可能偏向熟悉的证明模式，对新颖或差异较大的证明结构泛化有限；实证结论限于miniF2F。