用大模型和向量库自动构建可更新的数学知识图谱。
AutoMathKG: The automated mathematical knowledge graph based on LLM and vector database
- 将数学定义、定理、问题构建成有向图，通过大模型增强知识。
- 在五个基线中表现更优，支持高效数学推理与知识补全。
- 适合数学研究者、教育AI开发者快速获取结构化知识。
数学知识图谱（KG）以结构化方式呈现数学领域知识。基于自然语言构建数学KG是重要但具挑战性的任务。现有工作存在两大局限：一是受语料完整性限制，常丢弃或人工补充不完整知识；二是难以全自动整合多源知识。本文提出AutoMathKG，一个高质量、高覆盖、多维度且可自动更新的数学知识图谱。AutoMathKG将数学视为由定义、定理、问题实体及其引用关系构成的大型有向图。整合ProofWiki、教科书、arXiv论文和TheoremQA数据，利用大语言模型（LLM）通过上下文学习实现数据增强。为实现相似实体检索，设计两种嵌入策略，构建MathVD向量数据库（基于SBERT）。提出两种自动更新机制：知识补全机制通过定制数学大模型（Math LLM）交互生成缺失证明或解答；知识融合机制利用MathVD检索相似实体，再由LLM判断是否合并或新建实体。大量实验表明，AutoMathKG系统性能先进，应用广泛：在MathVD上达到优于五种基线的可达性查询效果，且在数学推理任务中表现出强鲁棒性。
原文摘要 · Abstract (English)
A mathematical knowledge graph (KG) presents knowledge within the field of mathematics in a structured manner. Constructing a math KG using natural language is an essential but challenging task. There are two major limitations of existing works: first, they are constrained by corpus completeness, often discarding or manually supplementing incomplete knowledge; second, they typically fail to fully automate the integration of diverse knowledge sources. This paper proposes AutoMathKG, a high-quality, wide-coverage, and multi-dimensional math KG capable of automatic updates. AutoMathKG regards mathematics as a vast directed graph composed of Definition, Theorem, and Problem entities, with their reference relationships as edges. It integrates knowledge from ProofWiki, textbooks, arXiv papers, and TheoremQA, enhancing entities and relationships with large language models (LLMs) via in-context learning for data augmentation. To search for similar entities, MathVD, a vector database, is built through two designed embedding strategies using SBERT. To automatically update, two mechanisms are proposed. For knowledge completion mechanism, Math LLM is developed to interact with AutoMathKG, providing missing proofs or solutions. For knowledge fusion mechanism, MathVD is used to retrieve similar entities, and LLM is used to determine whether to merge with a candidate or add as a new entity. A wide range of experiments demonstrate the advanced performance and broad applicability of the AutoMathKG system, including superior reachability query results in MathVD compared to five baselines and robust mathematical reasoning capability in Math LLM.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。