让数学方法自行说明适用条件：形式化证明的方法选择

基于 LLM 的形式证明者可以检索相关引理和先验证明，但仅相关性并不能说明数学方法是否可以用于当前定理。一种方法有先决条件、目标、预期的行动以及其使用需要证明的义务。因此，看起来与定理同样相关的方法可能在是否提供合理的下一步方面存在很大差异。我们将其表述为一个适用性意识方法选择问题，并引入自我广告：在对候选者进行排名之前，模型会为每个候选者生成一个针对特定问题的建议，说明其目标目标的哪一部分、将采取什么行动以及该行动需要什么条件。我们将 Putnam 2000-2014 中的 82 个可重用方法组织为方法契约，它将适用性描述与 Mathlib 锚点、经过检查的示例或脚手架以及预期的证明义务配对。一次批量调用即可引发整个图书馆的提案；模糊或不受支持的提案会被降级，产生一个排名入围的名单，并附上关于每个候选项用途的可检查的声明。我们分析基于相似性的表示何时无法区分具有不同适用性的方法，适用性估计中的错误如何影响候选名单的质量，以及经过检查的脚手架在其规定的假设下保证什么。相对于词汇、嵌入和嵌入加 LLM 重新排名基线，自我广告在 Putnam 2015-2025 上实现了 95.0% hit@5，而最强重新排名者的命中率为 84.2%。在 IMO ProofBench 上，它达到了 91.7%，而在 IMO ProofBench 上则为 88.3%。这些结果表明检索到的候选列表中带注释方法的覆盖率有所提高，特别是在 Putnam 上。