TheoremGraph：桥接形式化与非形式化数学

Hugging Face Daily Papers 论文
formal-mathematics dependency-graph lean arxiv semantic-embedding retrieval math-ai

摘要

TheoremGraph 是一个统一的语句级依赖图，涵盖非形式化数学（arXiv 论文）和形式化数学（Lean 项目），利用语义嵌入来弥合两者之间的差距。作者提供了数据集、提取器和 API，以支持数学搜索和检索。

数学知识围绕陈述及其依赖关系进行组织，但这种结构暴露不均：非形式化论文主要是在文档层面进行引用，而形式化库则在规模小得多的数学体系中记录细粒度的依赖关系。我们提出了 TheoremGraph，这是一个统一的语句级依赖图，涵盖非形式化与形式化数学。在非形式化方面，我们从数学 arXiv 解析了 1170 万个类定理环境，并恢复了 1830 万个候选有向依赖关系，每个关系都由提出该关系的提取器标记，以便下游用户可以在覆盖率和精确度之间进行权衡。在形式化方面，我们发布了 LeanGraph，这是一个 Lean 4 的 elaborator 级提取器，在 25 个 Lean 项目中生成了 388,105 个声明节点和 1130 万条类型化边。我们通过将生成的自然语言标语嵌入到共享的语义空间中来桥接这两个图，从而连接论文之间以及非形式化/形式化鸿沟两边的相关陈述；一个 LLM 评判器确认了 47,952 个这样的匹配，这些匹配的余弦相似度高于 0.8 的阈值，评判器的接受率从该阈值处的 48% 上升到 >=0.9 层级的 87%。在形式化概念检索方面，我们采用名称加签名表示并结合图扩展的方法，在无需 LM 重排序器的情况下，与 LeanSearch v2 的重排序后的 Recall@10 相差不到 0.5 个百分点（0.775 对比 0.780）。我们发布了数据集、提取器、HTTP API 和 MCP 接口，作为数学搜索、归因和检索增强推理的基础设施，这些可在 theoremsearch.com 和 huggingface.co/datasets/uw-math-ai/theorem-matching 获取。
查看原文
查看缓存全文

缓存时间: 2026/06/30 07:34

论文页面 - TheoremGraph：连接形式化与非形式化数学

摘要

一个统一的数学依赖图，通过语义嵌入以及从arXiv论文和Lean项目中自动提取，将非形式化数学与形式化数学连接起来。

数学知识围绕命题及其依赖关系组织，但这种结构的呈现并不均衡：非形式化论文通常只在文档级别进行引用，而形式化库则记录了更小规模数学内容上的细粒度依赖关系。我们引入了TheoremGraph，这是一个跨越非形式化与形式化数学的统一命题级依赖图。在非形式化一侧，我们解析了来自数学arXiv的1170万个类定理环境，并恢复了1830万个候选有向依赖关系，每个依赖都标注了提出它的提取器，以便下游用户可以在覆盖率和精确度之间进行权衡。在形式化一侧，我们发布了LeanGraph，这是一个Lean 4精化器级别的提取器，在25个Lean项目中生成了388,105个声明节点和1130万条带类型边。我们通过将生成的自然语言标语嵌入到共享的语义空间中，将两个图桥接起来，从而连接了论文间以及非形式化/形式化分界两侧的相关命题；一个LLM评判器确认了47,952个这样的匹配，余弦阈值设置为0.8以上，其中评判器接受率从整个阈值下的48%上升到≥0.9层级时的87%。在形式化概念检索任务上，我们的名称与签名表示结合图扩展，在没有LM重排序器的情况下，其召回率@10（0.775 vs. 0.780）与LeanSearch v2的重排序版本相差不到0.5个百分点。我们发布了数据集、提取器、HTTP API和MCP接口，作为数学搜索、归因和检索增强推理的基础设施，可在theoremsearch.com和huggingface.co/datasets/uw-math-ai/theorem-matching获取。

查看arXiv页面 查看PDF 项目页面 添加到收藏

将这篇论文放到你的智能体中：

hf papers read 2606.25363

没有最新的CLI？curl -LsSf https://hf.co/cli/install.sh | bash

引用此论文的模型（0）

没有模型链接到此论文

请在模型README.md中引用arxiv.org/abs/2606.25363以从本页面链接它。

引用此论文的数据集（1）

uw-math-ai/math-graph 查看器• 更新于1天前 • 16.1M • 75 • 2 (https://huggingface.co/datasets/uw-math-ai/math-graph)

引用此论文的Space（0）

没有Space链接到此论文

请在Space README.md中引用arxiv.org/abs/2606.25363以从本页面链接它。

包含此论文的收藏（0）

没有收藏包含此论文

请将此论文添加到一个收藏中以从本页面链接它。

相似文章

MathAtlas：野外自动形式化基准测试

arXiv cs.AI

MathAtlas 是一个针对研究生级别数学的自动形式化的大规模基准测试，包含从103本教科书中提取的约5.2万个定理和定义，并附带一个包含约17.8万条关系的数学依赖图。实验表明，最先进的模型正确率最高仅为9.8%，凸显了其难度。

形式化猜想：数学中可验证发现的开放且持续演进的基准

arXiv cs.AI

本文介绍了形式化猜想（Formal Conjectures），这是一个持续演进的基准，包含2615个在 Lean 4 中形式化的数学陈述，其中包括用于证明发现的开放研究猜想和用于自动形式化的已解决问题，旨在零污染地评估自动推理系统。