自荐式方法选择让形式化证明器在Putnam上命中率从84.2%升至95.0%
核心概要
该工作把形式化证明中的方法选择重新表述为适用性判断问题，提出“自荐”机制：在一次批量调用中让库中每个方法合约针对当前目标提出它要处理的目标片段、要执行的动作及所需条件，再对含糊或无依据的提案降级排序；在Putnam 2015–2025上hit@5达95.0%，最强重排基线为84.2%，IMO ProofBench上为91.7%对88.3%。
Figure 1: Self-advertised method selection. Given a theorem, a single model call asks every contract in the library how it would be used. A gate demotes proposals that are vague (Pigeonhole) or unsupported (AM-GM, since a i ≥ 0 a_{i}\geq 0 is not given), and the top-ranked contract (Cauchy–Schwarz) goes to the prover. Inset: similarity retrieval would pick AM-GM instead.
arXiv深度剖析
把方法选择与相似度检索区分开，并证明仅靠相似度表示的选择器可能给需要不同方法的多个目标分配相同表示，从而存在信息上限。 此前工作把检索单元设为引理、前提或既往证明，并以相似度排序；这里把检索单元改为带有前置条件、目标、动作与剩余义务的数学方法，并给出相似度选择器的信息界与两阶段选择的候选池上限。 以形式化命题与证明给出（命题2、推论1），并指出重排基线受第一阶段相似度候选池限制，短名单规模满足相应条件时低排名合约无法被任何重排骨干恢复。
提出自荐机制与82个方法合约：每个合约把方法的适用性描述与Mathlib锚点、已编译的脚手架或实例、以及预期剩余义务配对，在一次批量调用中为全部合约生成针对当前目标的提案。 不同于只输出分数或排序的LLM重排器，自荐让每个候选承诺可对照目标检查的目标、动作与所需条件，并用承诺门把含糊或无依据的主提名降级为支持角色。 82个合约由Putnam 2000–2014解答构建，全部执行侧Lean工件在Lean v4.27.0与Mathlib提交a3a10db下编译通过，每个合约提供任意参数下的脚手架与一个已编译实例；作者审阅了每个抽取方法与合并提议。
在Putnam 2015–2025与IMO ProofBench上，自荐在全部六个骨干–基准设置中取得最高recall@5，Putnam上hit@3、hit@5与MRR也在每个骨干下领先。 相对词法、稠密嵌入与嵌入加LLM重排基线，覆盖增益主要来自相似度排名在前五之外、甚至从未进入重排候选池的方法。 GPT-5.6 Luna下Putnam hit@5为95.0%、IMO ProofBench为91.7%，最强重排器分别为84.2%与88.3%；随骨干从DeepSeek V4.1 Flash到GPT-5.6 Luna再到GPT-5.6 Terra，Putnam hit@5从.900升至.950再升至.975，而最佳重排器停留在.842、.842、.858。
在固定编译预算的Ax-Prover式证明循环中加入排名第一的合约，Putnam已证问题比例从5.8%升至12.5%，IMO ProofBench从10.0%升至15.0%。 这是对所选合约是否对证明器有帮助的初步检验，增益集中在Putnam的分析与离散题以及IMO ProofBench的Basic题。 使用GPT-5.6 Luna、每题十次Lean编译预算；该比较整体加入所选合约，因此同时反映选择与合约内容，且多数问题在该预算内仍未解决。
启示与展望
该结果面向使用Lean与Mathlib的形式化证明流程：当证明器按顺序尝试短名单中的方法、或需要覆盖参考解法中的多个方法时，自荐提供的可检查提案与更高recall@5更有用。合约库由Putnam 2000–2014解答构建，评测在留出的Putnam 2015–2025与IMO ProofBench上进行，因此适用场景是竞赛数学方法的选择与复用；执行侧脚手架在Lean v4.27.0与Mathlib提交a3a10db下编译，命题1说明只要所需条件与剩余义务获得已检查证明，实例化脚手架即给出已检查证明。
短名单覆盖并不保证证明完成，下游比较整体加入合约而未隔离选择与执行指导的贡献，多数问题在十次编译预算内仍未解决。自荐给每个提案打绝对分数而非直接比较，不同合约的分数未必处于同一尺度，runoff只在领先提案间直接比较。命题3的界是条件性的最坏情况陈述，并不声称实测分数满足其前提；命题4指出多方法适用时期望hit@是次模目标，而实现按单合约分数排序，未运行贪心过程。标签由模型提出并经人工核验，hit@衡量与标注的一致性，是适用性的保守估计。