失败的证明不再被丢弃：7B模型把Isabelle证明成功率推到73.8%
HybridProver把整段证明生成与逐步策略生成接在同一条流水线上：整段模型先给出候选证明，未通过Isabelle检查的候选被抽成保留高层结构的证明骨架，再由策略模型与Sledgehammer逐个子目标补全。在Isabelle版miniF2F的244道测试题上，该流程取得73.8%的成功率，高于此前Isabelle系统的最好成绩61.9%。两个7B规模模型经监督微调与以Isabelle验证为奖励的强化学习训练，说明轻量模型也能生成Isabelle/HOL证明。