arXiv · cs.AI· Xiaopeng Yuan, Suijin Wang, Yanli Wang, Haibo Jin, Peng Kuang, Jerry Wang, Lijun Yu, Haohan Wang·· 1 天前
LLM形式化证明器提出Self-advertisement方法选择方法
Let the Library Speak: Self-Advertised Method Selection for Formal Proving
arXiv:2610.09401v1阅读论文 PDF ↗
仅依据论文摘要整理；未读取全文，实验条件、证明与基准细节请核对原文。
作者：Xiaopeng Yuan, Suijin Wang, Yanli Wang, Haibo Jin, Peng Kuang, Jerry Wang, Lijun Yu, Haohan Wang
首次提交：2026-10-07 12:03
研究任务与主要进展
作者提出Self-advertisement，用于让LLM形式化证明器在排序候选数学方法前生成问题特定提案，说明方法的目标、动作及使用条件。该方法整理了82个来自Putnam 2000–2014的可复用方法，并在Putnam 2015–2025上报告95.0%的hit@5，在IMO ProofBench上报告91.7%，分别高于论文比较的最强基线84.2%和88.3%。
阶段、条件与复现 · 深读核对
- 新能力对应什么具体任务与最小输入输出？
- 代码、模型、数据、许可与可用入口是否明确？
- 效果、总成本、失效条件与实际工作流如何验证？
这些是阅读核对问题；材料未说明的条件保留未知。请结合上方论文版本、资料范围与原文核验。
来源：arXiv · cs.AI · arxiv.org