用数学知识图谱增强大模型，提升自动定理证明能力
Scaling Natural-Language Graph-Based Test Time Compute for Automated Theorem Proving
- 用可靠数学文本构建知识图谱，辅助大模型推理
- 在多个数据集上提升2%-11%，最高达21%准确率增益
- 无需微调即可显著提升，适合数学推理研究者
大型语言模型在需要多步逻辑推理的自然语言处理任务中表现出色，如自动定理证明。然而，定理证明仍面临关键数学概念识别、关系理解及自然语言中正确形式化证明等挑战。本文提出KG-prover框架，利用从权威数学文本中挖掘的知识图谱，增强通用大模型以构建和形式化数学证明。我们研究了基于知识图谱的测试时计算扩展效果，结果显示在多个数据集上性能显著优于基线。通用大模型结合KG-prover后，在miniF2F-test上最多提升21%，在ProofNet、miniF2F-test和MUSTARD数据集上均实现2%-11%的一致提升。此外，KG-prover与o4-mini结合可在miniF2F-test上达到50%通过率。该工作为不依赖微调的自然语言证明推理提供了可行路径。
原文摘要 · Abstract (English)
Large language models have demonstrated remarkable capabilities in natural language processing tasks requiring multi-step logical reasoning capabilities, such as automated theorem proving. However, challenges persist within theorem proving, such as the identification of key mathematical concepts, understanding their interrelationships, and formalizing proofs correctly within natural language. We present KG-prover, a novel framework that leverages knowledge graphs mined from reputable mathematical texts to augment general-purpose LLMs to construct and formalize mathematical proofs. We also study the effects of scaling graph-based, test-time compute using KG-Prover, demonstrating significant performance improvements over baselines across multiple datasets. General-purpose LLMs improve up to 21\% on miniF2F-test when combined with KG-Prover, with consistent improvements ranging from 2-11\% on the ProofNet, miniF2F-test, and MUSTARD datasets. Furthermore, KG-Prover with o4-mini achieves 50\% on pass miniF2F-test. This work provides a promising approach for augmenting natural language proof reasoning with knowledge graphs without the need for additional finetuning.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。