Let the Library Speak: Self-Advertised Method Selection for Formal Proving
作者: Xiaopeng Yuan, Suijin Wang, Yanli Wang, Haibo Jin, Peng Kuang, Jerry Wang, Lijun Yu, Haohan Wang
分类: cs.AI
发布日期: 2026-10-07
备注: 17 pages. Preprint
💡 一句话要点
提出自我广告方法选择以解决形式证明中的适用性问题
🎯 匹配领域: 支柱五：交互与反应 (Interaction & Reaction)
关键词: 形式证明 方法选择 自我广告 适用性 自动定理证明 机器学习 数学方法
📋 核心要点
- 现有的形式证明工具在方法选择上仅依赖相关性，无法有效判断方法的适用性，导致选择不当。
- 本文提出自我广告机制，通过生成问题特定的提案来明确每个候选方法的目标和条件，从而提高方法选择的准确性。
- 实验结果显示，自我广告方法在多个基准测试中显著提升了方法选择的命中率，尤其在Putnam上表现突出。
📝 摘要（中文）
基于大型语言模型的形式证明工具能够检索相关的引理和先前的证明，但仅凭相关性无法判断某一数学方法是否适用于当前定理。方法具有前提条件、目标、预期操作和使用后留下的证明义务。本文将此问题表述为一个适用性感知的方法选择问题，并引入自我广告机制：在候选方法排名之前，模型为每个候选生成特定于问题的提案，说明其目标部分、将采取的操作及该操作所需的条件。我们将2000-2014年间的82种可重用方法组织为方法合同，配对适用性描述与Mathlib锚点、已检查的示例或框架及预期证明义务。通过单次批量调用，生成整个库的提案；模糊或不支持的提案被降级，从而产生一个带有可检查声明的排名短名单。实验结果表明，自我广告在Putnam 2015-2025上达到了95.0%的命中率，而最强的重排器为84.2%。
🔬 方法详解
问题定义：本文旨在解决形式证明中方法选择的适用性问题。现有方法仅依赖于相关性，无法有效区分不同方法的适用条件，导致选择不当和效率低下。
核心思路：论文提出自我广告机制，允许模型在候选方法排名前生成针对特定问题的提案，明确每个方法的目标、预期操作及其条件。这种设计旨在提高方法选择的准确性和有效性。
技术框架：整体架构包括方法合同的组织、提案生成模块和排名模块。首先，将82种方法整理为方法合同，配对适用性描述与Mathlib锚点。然后，通过批量调用生成提案，最后对提案进行排名，剔除模糊或不支持的提案。
关键创新：最重要的技术创新在于自我广告机制的引入，使得方法选择不仅依赖于相关性，还考虑了适用性。这与现有方法的本质区别在于，后者往往忽视了方法的具体应用条件。
关键设计：在模型设计中，关键参数包括提案生成的条件设置和候选方法的排名策略。损失函数的设计考虑了提案的准确性和可解释性，以确保最终生成的短名单具有较高的质量和实用性。
🖼️ 关键图片
📊 实验亮点
实验结果显示，自我广告方法在Putnam 2015-2025基准测试中达到了95.0%的命中率，相较于最强重排器的84.2%有显著提升。在IMO ProofBench上，自我广告方法的命中率为91.7%，也高于对比基线的88.3%。
🎯 应用场景
该研究的潜在应用领域包括自动定理证明、数学教育和形式化验证等。通过提高方法选择的准确性，能够有效提升形式证明工具的效率和可靠性，进而推动相关领域的发展和应用。
📄 摘要（原文）
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.