利用大语言模型智能体与知识图谱实现数学证明自动生成

大语言模型在需要多步逻辑推理的自然语言处理任务（如自动定理证明）中展现出卓越能力。然而定理证明领域仍存在关键挑战：数学概念的识别、概念间关系的理解以及自然语言证明的形式化。

我们提出KG-prover创新框架，通过从权威数学文本挖掘的知识图谱来增强通用大语言模型，构建并形式化数学证明。研究还探讨了基于图谱的测试时计算扩展效果，在多个数据集上相比基线模型取得显著性能提升。

当结合KG-prover时，通用大语言模型在miniF2F-test上的性能提升达21%，在ProofNet、miniF2F-test和MUSTARD数据集上持续获得2-11%的改进且无需额外扩展。此外，搭载o4-mini的KG-prover在miniF2F-test上实现超过50%的准确率。这项工作为无需额外微调即可通过知识图谱增强自然语言证明推理提供了可行方案。

本文已被ICML AI4Math Workshop 2025和NAACL SRW 2025接收