结构化知识何时有助于神经定理证明？

结构化数学知识是否有助于LLM证明Lean 4 中的定理？如果是，对于哪些型号，答案是否因问题而异？ Mathlib 等正式库编码了 285,000 多个具有句法依赖性的经过验证的定理，但数学家用来发现的语义层（类比、概括、跨域桥梁）仍然是隐式的。我们引入MathAgent，它将这一层构建为知识图MathKG，并用它来增强LLM定理证明器。 MathKG 通过基于 LLM 的关系提取推断出的 9,434 个类型化语义边缘连接了 364 个 Mathlib 定理和定义，这些关系提取锚定到经过验证的 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%）。这些结果激发了根据模型能力和问题选择增强的自适应策略。代码、数据和工件可在 https://github.com/sarehnabi/mathagent 获取