論文の概要: MathAtlas: A Benchmark for Autoformalization in the Wild

• arxiv url: http://arxiv.org/abs/2605.14061v1
• Date: Wed, 13 May 2026 19:35:46 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-05-15 21:45:34.479944
• Title: MathAtlas: A Benchmark for Autoformalization in the Wild
• Title（参考訳）: MathAtlas: 野生でのオートフォーマル化のためのベンチマーク
• Authors: Nilay Patel, Noah Arias, Davit Babayan, Victoria Cochran, Timothy Libman, Hafsah Mahmood, Liam McCarty, Soli Munoz, Laurel Willey, Jeffrey Flanigan,
• Abstract要約: 野生の大学院レベルの数学における最初の大規模自己形式化ベンチマークであるMathAtlasを紹介する。 MathAtlasには、52kの定理、定義、演習、例が含まれ、103の大学院数学の教科書から抽出された。
• 参考スコア（独自算出の注目度）: 7.981378950583468
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Current autoformalization benchmarks are largely focused on olympiad or undergraduate mathematics, while graduate and research-level mathematics remains underexplored. In this paper, we introduce MathAtlas, the first large-scale autoformalization benchmark of in the wild graduate-level mathematics, containing ~52k theorems, definitions, exercises, examples, and proofs extracted from 103 graduate mathematics textbooks. MathAtlas is enriched with a mathematical dependency graph containing ~178k relations, and is the first autoformalization benchmark to include such relations, facilitating evaluation and development of dependency-aware autoformalization systems. Our extensive experiments show that MathAtlas is high quality but extremely challenging: strong baselines achieve at most 9.8% correctness on theorem statements and 16.7% on definitions. Furthermore, we find performance of state-of-the-art models degrades substantially with dependency depth: on MA-Hard, a subset of 700 entities with the deepest dependency trees, the best model achieves only 2.6% correctness for autoformalization on this challenging dataset. We release MathAtlas to the community as a benchmark set for large-scale autoformalization of graduate-level mathematics in the wild.
• Abstract（参考訳）: 現在の自己形式化ベンチマークは主にオリンピックや学部数学に焦点が当てられているが、大学院や研究レベルの数学は未調査のままである。 本稿では,約52kの定理,定義,エクササイズ,例,および103の大学院数学教科書から抽出した証明を含む,野生の大学院数学における最初の大規模自己形式化ベンチマークであるMathAtlasを紹介する。 MathAtlas は ~178k の関係を含む数学的依存グラフに富み、そのような関係を含む最初のオートフォーマル化ベンチマークであり、依存性を意識したオートフォーマル化システムの評価と開発を容易にする。 我々の広範な実験により、MathAtlasは高品質であるが極めて難しいことが示される:強いベースラインは、定理文の少なくとも9.8%の正しさと定義の16.7%である。 MA-Hardでは、最も深い依存木を持つ700個のエンティティのサブセットであり、最も優れたモデルは、この挑戦的なデータセット上で自動形式化の2.6%の正確性しか達成できない。 我々は,大学院数学の大規模オートフォーマル化のためのベンチマークセットとして,MathAtlasをコミュニティにリリースした。

関連論文リスト

• Matlas: A Semantic Search Engine for Mathematics [2.8548596155460024]
  Matlasは数学的ステートメントのセマンティック検索エンジンである。 マトラスは1826年から2025年にかけて435万件の査読論文から870万件の文書を抽出した大規模コーパス上に構築されている。 このコーパスの上に,自然言語クエリを用いた数学的結果の効率的な検索を可能にする意味検索システムを構築する。
  論文  参考訳（メタデータ） (2026-04-19T15:17:28Z)
• HorizonMath: Measuring AI Progress Toward Mathematical Discovery with Automatic Verification [54.06301039725887]
  計算および応用数学において8つの領域にまたがる100以上の未解決問題のベンチマークであるHorizonMathを紹介する。 我々のベンチマークは、発見が困難であり、意味のある数学的洞察を必要とする問題のクラスをターゲットにしているが、検証は計算的に効率的で簡単なものである。
  論文  参考訳（メタデータ） (2026-03-16T17:59:53Z)
• TaoBench: Do Automated Theorem Prover LLMs Generalize Beyond MathLib? [104.38098884163541]
  新たな定義枠組みに適用した場合の現在のATPシステムの堅牢性を評価する。 本稿では,terence Tao氏のAnalytic Iから派生した,学部レベルのベンチマークであるTaoBenchを紹介する。 公平な評価のために,各問題に対してコンパイル可能な自己完結型ローカル環境を自動的に抽出するエージェントパイプラインを構築した。
  論文  参考訳（メタデータ） (2026-03-13T07:39:47Z)
• AutoMathKG: The automated mathematical knowledge graph based on LLM and vector database [1.799933345199395]
  数学知識グラフ(KG)は、数学の分野における知識を構造化された方法で提示する。 本稿では,自動更新が可能な高品質・広包・多次元数学KGであるAutoMathKGを提案する。
  論文  参考訳（メタデータ） (2025-05-19T17:41:29Z)
• Challenging the Boundaries of Reasoning: An Olympiad-Level Math Benchmark for Large Language Models [86.45058529521258]
  OlymMATHは、LLMの複雑な推論能力を厳格にテストするために設計された、Olympiadレベルの新しい数学ベンチマークである。 OlymMATHは200の厳密にキュレートされた問題があり、それぞれが手動で検証され、英語と中国語の並行バージョンで利用可能である。
  論文  参考訳（メタデータ） (2025-03-27T11:20:17Z)
• Formal Mathematical Reasoning: A New Frontier in AI [60.26950681543385]
  我々は公式な数学的推論を提唱し、AI4Mathを次のレベルに進めるには不可欠であると主張している。 既存の進捗を要約し、オープンな課題について議論し、将来の成功を測るための重要なマイルストーンを想定します。
  論文  参考訳（メタデータ） (2024-12-20T17:19:24Z)
• MathBench: Evaluating the Theory and Application Proficiency of LLMs with a Hierarchical Mathematics Benchmark [82.64129627675123]
  MathBenchは、大規模言語モデルの数学的能力を厳格に評価する新しいベンチマークである。 MathBenchは幅広い数学の分野にまたがっており、理論的な理解と実践的な問題解決のスキルの両方を詳細に評価している。
  論文  参考訳（メタデータ） (2024-05-20T17:52:29Z)
• A New Approach Towards Autoformalization [7.275550401145199]
  オートフォーマル化(Autoformalization)は、自然言語をプログラムで検証可能な形式言語に変換するタスクである。 研究論文は大量の背景と文脈を必要とする。 本稿では,研究レベルの数学の自己形式化に取り組み,タスクをより容易に,より親しみやすいサブタスクに分割する手法を提案する。
  論文  参考訳（メタデータ） (2023-10-12T00:50:24Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。