論文の概要: TaoBench: Do Automated Theorem Prover LLMs Generalize Beyond MathLib?

• arxiv url: http://arxiv.org/abs/2603.12744v1
• Date: Fri, 13 Mar 2026 07:39:47 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-03-16 17:38:11.973086
• Title: TaoBench: Do Automated Theorem Prover LLMs Generalize Beyond MathLib?
• Title（参考訳）: TaoBench: 自動理論のLLMはMathLibを超えて一般化するのか?
• Authors: Alexander K Taylor, Junyi Zhang, Ethan Ji, Vigyan Sahai, Haikang Deng, Yuanzhou Chen, Yifan Yuan, Di Wu, Jia-Chen Gu, Kai-Wei Chang, Nanyun Peng, Amit Sahai, Wei Wang,
• Abstract要約: 新たな定義枠組みに適用した場合の現在のATPシステムの堅牢性を評価する。 本稿では,terence Tao氏のAnalytic Iから派生した,学部レベルのベンチマークであるTaoBenchを紹介する。 公平な評価のために,各問題に対してコンパイル可能な自己完結型ローカル環境を自動的に抽出するエージェントパイプラインを構築した。
• 参考スコア（独自算出の注目度）: 104.38098884163541
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Automated theorem proving (ATP) benchmarks largely consist of problems formalized in MathLib, so current ATP training and evaluation are heavily biased toward MathLib's definitional framework. However, frontier mathematics is often exploratory and prototype-heavy, relying on bespoke constructions that deviate from standard libraries. In this work, we evaluate the robustness of current ATP systems when applied to a novel definitional framework, specifically examining the performance gap between standard library problems and bespoke mathematical constructions. We introduce TaoBench, an undergraduate-level benchmark derived from Terence Tao's Analysis I, which formalizes analysis by constructing core mathematical concepts from scratch, without relying on standard Mathlib definitions, as well as by mixing from-scratch and MathLib constructions. For fair evaluation, we build an agentic pipeline that automatically extracts a compilable, self-contained local environment for each problem. To isolate the effect of definitional frameworks, we additionally translate every problem into a mathematically equivalent Mathlib formulation, yielding paired TaoBench-Mathlib statements for direct comparison. While state-of-the-art ATP models perform capably within the MathLib framework, performance drops by an average of roughly 26% on the definitionally equivalent Tao formulation. This indicates that the main bottleneck is limited generalization across definitional frameworks rather than task difficulty. TaoBench thus highlights a gap between benchmark performance and applicability, and provides a concrete foundation for developing and testing provers better aligned with research mathematics.
• Abstract（参考訳）: ATP(Automated theorem Proving)ベンチマークは主にMathLibで形式化された問題で構成されているため、現在のATPトレーニングと評価はMathLibの定義フレームワークに大きく偏っている。 しかしながら、フロンティア数学はしばしば探索的かつプロトタイプ重大であり、標準図書館から逸脱する造形に依存している。 本研究では,新しい定義フレームワークに適用した現行ATPシステムのロバスト性を評価する。 本稿では,TeoBenchについて紹介する。TeoBenchはTerence TaoのAnalytic Iから派生した,標準のMathlib定義に依存することなく,基本数学的概念をスクラッチから構築することで解析を形式化し, from-scratch と MathLib の構造を混合した,学部レベルのベンチマークである。 公平な評価のために,各問題に対してコンパイル可能な自己完結型ローカル環境を自動的に抽出するエージェントパイプラインを構築した。 定義フレームワークの効果を分離するために、すべての問題を数学的に等価なMathlib式に変換し、直接比較のためにペア化されたTaoBench-Mathlib文を生成する。 最先端のATPモデルはMathLibフレームワークで実行可能であるが、定義上等価なTaoの定式化では平均で26%性能が低下する。 これは、主なボトルネックはタスクの難しさよりも定義フレームワーク間の一般化に限られていることを示している。 TaoBenchは、ベンチマークパフォーマンスと適用性の間のギャップを強調し、研究数学に適合したプローバーの開発とテストのための具体的な基盤を提供する。

関連論文リスト

• MathlibLemma: Folklore Lemma Generation and Benchmark for Formal Mathematics [51.65118519899584]
  数学的民俗補題の発見と形式化を自動化するLLMベースのマルチエージェントシステムであるMathlibLemmaを紹介する。 さらに、幅広い数学的領域にまたがる4,028の型チェックリーンステートメントスイートであるMathlibLemmaベンチマークを構築します。
  論文  参考訳（メタデータ） (2026-01-30T15:24:42Z)
• 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)
• DAG-Math: Graph-Guided Mathematical Reasoning in LLMs [54.231935013127206]
  大型言語モデル (LLM) は, CoT (Chain-of-Thought) による数学的問題に対して高い性能を示す 我々は、有向非巡回グラフ(DAG)上の一定の規則に基づくプロセスとしてCoTをモデル化することを提案する。 ここでは,モデルのCoT軌道がDAG構造にどの程度よく依存するかを定量化する計量である論理的近接性を導入する。
  論文  参考訳（メタデータ） (2025-10-19T21:05:17Z)
• DRIFT: Decompose, Retrieve, Illustrate, then Formalize Theorems [14.568293842955065]
  DRIFTは、非公式な数学的ステートメントをより小さく、より扱いやすい'サブコンポーネント'に分解するフレームワークである。 これは、モデルが形式化タスクにおいてより効果的に前提を使用するのを助けるために、イラストラティブな定理を回収する。 我々は,様々なベンチマーク(ProofNet,ConNF,MiniF2F-test)でDRIFTを評価し,前提条件の検索を継続的に改善することを発見した。
  論文  参考訳（メタデータ） (2025-10-12T21:42:04Z)
• Computational Reasoning of Large Language Models [51.629694188014064]
  textbfTuring Machine Benchは,Large Language Models(LLM)による推論プロセスの実行能力を評価するベンチマークである。 TMBenchには、自己完結型および知識に依存しない推論、最小主義的な多段階構造、制御可能な難易度、チューリングマシンに基づく理論的基礎の4つの重要な特徴が組み込まれている。
  論文  参考訳（メタデータ） (2025-04-29T13:52:47Z)
• 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)
• StructTest: Benchmarking LLMs' Reasoning through Compositional Structured Outputs [78.84060166851805]
  StructTestは、大規模な言語モデル(LLM)を合成命令に従って構造化出力を生成する能力に基づいて評価する、新しいベンチマークである。 評価はルールベースの評価器を用いて決定的に行われ、新しいタスクやデータセットに容易に拡張できる。 StructTestは、Deepseek-V3/R1やGPT-4oといったトップパフォーマンスモデルでも、依然として難しいままです。
  論文  参考訳（メタデータ） (2024-12-23T22:08:40Z)

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

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