发表机构
University of Illinois at Urbana-Champaign; Tsinghua University; Imperial College London; Google（伊利诺伊大学厄巴纳-香槟分校; 清华大学; 帝国理工学院; 谷歌）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
针对形式化证明中方法选择忽视适用性的问题，提出自荐式方法选择，通过生成提案并降级模糊项，在Putnam和IMO基准上显著提升命中率。
AI 中文摘要
基于LLM的形式化证明器可以检索相关的引理和先前的证明，但相关性本身并不能说明某个数学方法是否可用于当前定理。一个方法具有前置条件、目标、预期动作以及使用后遗留的证明义务。因此，与定理看似同样相关的方法，在是否提供合理的下一步步骤方面可能存在显著差异。我们将此问题表述为适用性感知的方法选择问题，并引入自荐机制：在对候选方法进行排序之前，模型为每个候选方法生成一个针对特定问题的提案，说明其针对目标哪一部分、将采取什么动作以及该动作所需的条件。我们将Putnam 2000-2014中的82个可重用方法组织为方法契约，这些契约将适用性描述与Mathlib锚点、经过检查的示例或脚手架以及预期的证明义务配对。一次批量调用即可在整个库中引出提案；模糊或不支持的提案会被降级，从而产生一个带有关于每个候选方法使用的可检查声明的排序短名单。我们分析了基于相似性的表示何时无法区分具有不同适用性的方法、适用性估计中的错误如何影响短名单质量，以及经过检查的脚手架在其声明假设下能保证什么。与基于词汇、嵌入以及嵌入加LLM重排序的基线相比，自荐在Putnam 2015-2025上实现了95.0%的命中率@5，而最强重排序器为84.2%。在IMO ProofBench上，它实现了91.7%，而后者为88.3%。这些结果表明，在检索到的短名单中，注释方法的覆盖率有所提高，尤其是在Putnam上。
英文摘要
LLM-based formal provers can retrieve relevant lemmas and prior proofs, but relevance alone does not say whether a mathematical method can be used on the current theorem. A method has prerequisites, a target, an intended action, and obligations that its use leaves to prove. Methods that look equally related to a theorem may therefore differ substantially in whether they offer a plausible next step. We formulate this as an applicability-aware method-selection problem and introduce self-advertisement: before candidates are ranked, a model generates a problem-specific proposal for each one, stating what part of the goal it targets, what action it would take, and what conditions that action requires. We organize 82 reusable methods from Putnam 2000-2014 as Method Contracts, which pair applicability descriptions with Mathlib anchors, a checked example or scaffold, and expected proof obligations. A single batched call elicits proposals across the library; vague or unsupported proposals are demoted, yielding a ranked shortlist accompanied by inspectable claims about each candidate's use. We analyze when similarity-based representations cannot distinguish methods with different applicability, how errors in applicability estimates affect shortlist quality, and what a checked scaffold guarantees under its stated assumptions. Against lexical, embedding, and embedding-plus-LLM reranking baselines, self-advertisement achieves 95.0% hit@5 on Putnam 2015-2025, compared with 84.2% for the strongest reranker. On IMO ProofBench, it achieves 91.7% compared with 88.3%. These results indicate improved coverage of annotated methods in the retrieved shortlists, particularly on Putnam.
Comments17 pages. Preprint
