Method self-descriptions improve theorem proving accuracy with large language models
Let the Library Speak: Self-Advertised Method Selection for Formal Proving
Artificial Intelligence
Summary
Picking the right math method to prove a theorem is tricky because not all methods fit every problem. The authors propose that each method should explain what part of the problem it solves, what it does, and what it needs to work. This lets a computer better choose useful methods instead of just picking ones that look similar. Their approach significantly improves finding the right methods for math problems in tests like the Putnam competition and the International Math Olympiad.
What this means in practice
- •For formal methods engineers: Increase success rates in automated proof assistants by using methods that specify their applicability before selection.
- •For mathematics software developers: Develop smarter theorem-proving tools that rank methods based on their stated goals and assumptions to guide proof construction efficiently.
Authors
Xiaopeng Yuan, Suijin Wang, Yanli Wang, Haibo Jin, Peng Kuang, Jerry Wang, Lijun Yu, Haohan Wang
Abstract
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.