发表机构
Stanford University（斯坦福大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本研究提出MathAgent，通过构建MathKG知识图谱增强LLM定理证明，发现特化优于增强，增强效果依赖模型能力，且不同增强模式互补，支持自适应选择策略。
AI 中文摘要
结构化数学知识是否有助于大型语言模型在Lean 4中证明定理？如果有帮助，对哪些模型有帮助，答案是否因问题而异？像Mathlib这样的形式化库编码了超过285,000条已验证的定理及其语法依赖关系，但数学家依赖的语义层（类比、泛化、跨领域桥梁）仍然是隐性的。我们引入了MathAgent，它将该层构建为知识图谱MathKG，并利用它增强LLM定理证明器。MathKG通过基于LLM的关系抽取（锚定于已验证的Mathlib声明）推断出的9,434条类型化语义边，连接了364条Mathlib定理和定义。我们在四种增强模式（无上下文、知识图谱上下文、Mathlib检索、两者结合）和五个模型（Qwen3-8B/32B、其Lean特化衍生模型Goedel-Prover-V2-8B/32B以及Claude Sonnet 4.6）上进行了受控消融实验，在miniF2F基准上测试，并对Sonnet在PutnamBench和MathOlympiadBench上额外测试。出现了三个发现。（i）特化主导增强：在每种模式下，Lean微调使求解率提高33-38个百分点，特化的8B模型比大4倍的通用模型高出29-35个百分点，而任何增强模式对求解率的提升不超过3个百分点。（ii）增强受能力条件限制：知识图谱上下文帮助小模型但损害大模型，特化模型在每个规模上相对于其通用基础模型获得更多相对增益。（iii）然而，增强模式解决了不同的问题：一个为每个问题选择最佳模式的预言机比未增强的证明器多解决6%至58%的问题，这种互补效应在更难的问题上更强（在PutnamBench上多32%）。这些结果促使采用根据模型能力和问题选择增强的自适应策略。代码、数据和工件可在以下URL获取。
英文摘要
Does structured mathematical knowledge help LLMs prove theorems in Lean 4? If so, for which models, and does the answer vary by problem? Formal libraries such as Mathlib encode 285,000+ verified theorems with syntactic dependencies, but the semantic layer mathematicians rely on for discovery (analogies, generalizations, cross-domain bridges) remains implicit. We introduce MathAgent, which builds this layer as a knowledge graph, MathKG, and uses it to augment LLM theorem provers. MathKG connects 364 Mathlib theorems and definitions by 9,434 typed semantic edges inferred via LLM-based relation extraction anchored to verified Mathlib declarations. We run a controlled ablation across four augmentation modes (no context, knowledge-graph context, Mathlib retrieval, both) and five models: Qwen3-8B/32B, their Lean-specialized derivatives Goedel-Prover-V2-8B/32B, and Claude Sonnet 4.6, on miniF2F, plus PutnamBench and MathOlympiadBench for Sonnet. Three findings emerge. (i) Specialization dominates augmentation: Lean fine-tuning adds 33-38 percentage points of solve rate in every mode, and a specialized 8B model beats a $4\times$ larger general one by 29-35 points, while no augmentation mode improves solve rate by more than 3 points. (ii) Augmentation is capability-conditioned: knowledge-graph context helps small models but hurts large ones, with the specialized model gaining more relative to its general base at every scale. (iii) Yet the augmentation modes solve different problems: an oracle selecting the best mode per problem solves 6% to 58% more than the unaugmented prover, a complementarity effect that strengthens on harder problems (32% more on PutnamBench). These results motivate adaptive strategies that select augmentation by model capability and problem. Code, data, and artifacts are available at https://github.com/sarehnabi/mathagent
Comments30 pages, 4 figures, 12 tables
