論文の概要: TheoremGraph: Bridging Formal and Informal Mathematics
- arxiv url: http://arxiv.org/abs/2606.25363v1
- Date: Wed, 24 Jun 2026 03:47:05 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-06-25 17:05:30.210037
- Title: TheoremGraph: Bridging Formal and Informal Mathematics
- Title（参考訳）: TheoremGraph:ブリッジング形式とインフォーマル数学
- Abstract要約: TheoremGraphは、非公式数学と形式数学の両方にまたがる統一されたステートメントレベル依存グラフである。
非公式な側面では、数学 arXiv から 11.7M の定理のような環境を解析し、18.3M の候補指向の依存関係を復元する。
正式な面では、LeanGraphをリリースしています。Lean 4のエラボレータレベルの抽出器で、388,105の宣言ノードと11.3Mの型付きエッジを生成します。
- 参考スコア（独自算出の注目度）: 1.353002745363665
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Mathematical knowledge is organized around statements and their dependencies, but this structure is exposed unevenly: informal papers cite mostly at the document level, while formal libraries record fine-grained dependencies over a much smaller body of mathematics. We introduce TheoremGraph, a unified statement-level dependency graph spanning both informal and formal mathematics. On the informal side, we parse 11.7M theorem-like environments from mathematics arXiv and recover 18.3M candidate directed dependencies, each labeled by the extractor that proposed it so downstream users can trade coverage for precision. On the formal side, we release LeanGraph, a Lean 4 elaborator-level extractor producing 388,105 declaration nodes and 11.3M typed edges across 25 Lean projects. We bridge the two graphs by embedding generated natural-language slogans into a shared semantic space, linking related statements across papers and across the informal/formal divide; an LLM judge affirms 47,952 such matches above a 0.8 cosine floor, with the judge-acceptance rate rising from 48% across the floor to 87% in the >=0.9 tier. On formal concept retrieval, our name-and-signature representation with graph expansion comes within 0.5pp of LeanSearch v2's reranked Recall@10 (0.775 vs. 0.780) without an LM reranker. We release the dataset, extractors, HTTP API, and MCP interface as infrastructure for mathematical search, attribution, and retrieval-augmented reasoning, available at theoremsearch.com and huggingface.co/datasets/uw-math-ai/theorem-matching.
- Abstract（参考訳）: 数学的知識は文とその依存関係を中心に組織されているが、この構造は不均一に露呈している: 非公式な論文は主に文書のレベルで引用されるが、形式的な図書館はより小さな数学の体系に対するきめ細かい依存関係を記録している。
フォーマルな数学とフォーマルな数学の両方にまたがる統一的なステートメントレベル依存グラフであるTheoremGraphを紹介する。
非公式な面では、数学のarXivから1.7Mの定理のような環境を解析し、18.3Mの候補指向の依存関係を復元する。
フォーマルな面では、25のLeanプロジェクトで388,105の宣言ノードと11.3Mの型付きエッジを生成するLean 4エラボレータレベルの抽出器であるLeanGraphをリリースしています。
この2つのグラフは,生成した自然言語のスローガンを共有意味空間に埋め込んで,論文と形式的/形式的な隔たりをつなぐことでブリッジする。LCMの裁判官は,0.8コサインフロアの上の47,952個のマッチを確認し,判定受容率は床の48%から0.9層で87%に上昇する。
正式な概念検索では、グラフ拡張を伴う名前と署名の表現は、LMリランカなしでLeanSearch v2のreranked Recall@10 (0.775 vs. 0.780)の0.5pp以内です。
このデータセット、抽出器、HTTP API、MSPインターフェースを数学的検索、帰属、検索強化推論の基盤としてリリースし、the theoremsearch.com と huggingface.co/datasets/uw-math-ai/theorem-matching で利用可能である。
関連論文リスト
- GTA: Graph Theory Agent and Benchmark for Algorithmic Graph Reasoning with LLMs [50.68372832207766]
Graph Theory Bench (GT Bench) は、44のタスク構造設定において24の古典的なグラフ問題をカバーするベンチマークである。
GT Benchは、精度が入力表現と強く結びついていることを示している。
本稿では,選好学習された表現セレクタと計画と分解の足場を組み合わせたグラフ理論エージェント(GTA)を提案する。
論文 参考訳（メタデータ） (2026-09-10T22:50:10Z) - VeriGraph: Towards Verifiable Data-Analytic Agents [71.17693022916896]
LLMをベースとしたエージェントは、データ集約分析タスクにおいて強力な能力を示してきたが、その出力は滅多に検証されていない。
We propose VeriGraph, a traceable neuro-symbolic reasoning framework that agent can construct an explicit heterogeneous evidence directed acyclic graph。
以上の結果から,明示的なエビデンスグラフ構築がデータ分析エージェントの検証に期待できる道のりであることが示唆された。
論文 参考訳（メタデータ） (2026-06-15T11:50:56Z) - Goedel-Architect: Streamlining Formal Theorem Proving with Blueprint Generation and Refinement [69.77146194380488]
私たちはGoedel-Architectを紹介します。これは、青写真の生成と洗練に焦点を当てたLean 4で証明された公式な定理のためのフレームワークです。
Goedel-ArchitectがMiniF2Fテストで99.2%パス@1、PutnamBenchで75.6%パス@1を達成した。
これは、同等のオープンソースパイプラインよりも500倍低い価格で、オープンソースパイプラインの最先端のパフォーマンスを示している。
論文 参考訳（メタデータ） (2026-06-04T17:54:44Z) - COMPOSE: Composing Future Theorems from Citations and Formal Structure [2.0503162970534947]
そこでは、アンカー紙に対する理論的な未来的主張を生成することを目的として、基礎となる未来の数学的生成を紹介する。
科学的な引用コンテキストと形式的定理構造の両方に言語モデルを条件づけた,二重グラフフレームワークComposeを提案する。
実験の結果,Composeは検索において,将来的な論文に対して高いベースラインを達成していることがわかった。
論文 参考訳（メタデータ） (2026-05-28T17:58:42Z) - LiveMathematicianBench: A Live Benchmark for Mathematician-Level Reasoning with Proof Sketches [61.30693283718321]
研究レベルの数学的推論のための動的多重選択ベンチマークであるLiveMathematicianBenchを提案する。
新たに発表された定理で評価を基礎づけることで、記憶されたパターンを超えた現実的なテストベッドを提供する。
このパイプラインは、高レベルな証明戦略を使用して、妥当だが無効な解選択を構築する。
論文 参考訳（メタデータ） (2026-04-02T08:22:17Z) - LeanCat: A Benchmark Suite for Formal Category Theory in Lean (Part I: 1-Categories) [7.871706113805829]
LeanCatは、カテゴリ理論の形式化のためのリーンベンチマークである。
パート I: 1-カテゴリには、完全に形式化されたステートメントレベルのタスクが100個含まれています。
Part II: LeanBridgeはLeanExploreを使ってMathlibを検索し、単一モデルベースラインに対する一貫した利得を観察します。
論文 参考訳（メタデータ） (2025-12-31T11:33:29Z) - DRIFT: Decompose, Retrieve, Illustrate, then Formalize Theorems [14.568293842955065]
DRIFTは、非公式な数学的ステートメントをより小さく、より扱いやすい'サブコンポーネント'に分解するフレームワークである。
これは、モデルが形式化タスクにおいてより効果的に前提を使用するのを助けるために、イラストラティブな定理を回収する。
我々は,様々なベンチマーク(ProofNet,ConNF,MiniF2F-test)でDRIFTを評価し,前提条件の検索を継続的に改善することを発見した。
論文 参考訳（メタデータ） (2025-10-12T21:42:04Z) - Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
この研究は、記号的突然変異を通じて形式的な定理を構成するデータ合成のフレームワークであるAlchemyを提案する。
マドリブにおける各候補定理について、書き直しや適用に使用できるすべてのイベーシブルな定理を同定する。
その結果、マドリブの定理の数は110kから6Mへと桁違いに増加する。
論文 参考訳（メタデータ） (2024-10-21T08:04:21Z) - Herald: A Natural Language Annotated Lean 4 Dataset [15.42247133378869]
本稿では,Mathlib4コーパス(形式言語Lean 4における数学の統一ライブラリ)を自然言語に翻訳するための新しいフレームワークを提案する。
私たちはこのパイプラインの結果をHeraldとしてMathlib4で発表します(階層とレトリバルベースのトランスレーショナルリーン)。
また,Heraldを微調整したHerald Translatorを提案する。
論文 参考訳（メタデータ） (2024-10-09T10:11:24Z) - LEAN-GitHub: Compiling GitHub LEAN repositories for a versatile LEAN prover [56.34998574538897]
我々は、GitHub上のLean 4リポジトリから抽出された大規模なフォーマルデータからなるデータセットであるLEAN-GitHubを提案する。
我々のモデルは1回のパスで48.8%、64回のパスで54.5%、Lean 4 miniF2Fテストで54.5%に達し、最先端のメソッドを52%上回った。
論文 参考訳（メタデータ） (2024-07-24T12:28:03Z) - Evaluating Class Membership Relations in Knowledge Graphs using Large Language Models [0.0]
知識グラフのバックボーンは、与えられたクラスにエンティティを割り当てるクラスメンバーシップ関係である。
本稿では,与えられたエンティティとクラスの記述を処理することによって,これらの関係の質を評価する新しい手法を提案する。
本手法はWikidataとCaLiGraphの2つの公開知識グラフと7つの大言語モデルを用いて評価する。
論文 参考訳（メタデータ） (2024-04-25T19:44:46Z) - TheoremQA: A Theorem-driven Question Answering dataset [100.39878559382694]
GPT-4のこれらの問題を解決する能力は非並列であり、Program-of-Thoughts Promptingの精度は51%である。
TheoremQAは、350の定理をカバーする800の高品質な質問を含むドメインの専門家によってキュレートされる。
論文 参考訳（メタデータ） (2023-05-21T17:51:35Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。