論文の概要: MathAdv: What Theorem Provers Know, Reason, Formalize, and Generalize
- arxiv url: http://arxiv.org/abs/2608.25449v2
- Date: Fri, 28 Aug 2026 17:03:13 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-08-31 15:11:36.080859
- Title: MathAdv: What Theorem Provers Know, Reason, Formalize, and Generalize
- Title（参考訳）: MathAdv: Theorem Proversが知っていること、推論、形式化、一般化
- Authors: Jiaxin Yuan, Connor Martinez Lockhart, Xiaoyu Liu, Jiaqi Wang, Chenghao Deng, Xiayimei Han, Vlassis Mastrantonis, Dmitrii Gudin, Shaopeng Zhu, Abdirisak Mohamed, Bilal Aytekin, Jiewen Lang, Zezheng Song, Furong Huang,
- Abstract要約: MathAdvは、学部および大学院レベルの数学で13のドメインにまたがる診断ベンチマークである。
本稿では, 定理証明精度が不明瞭であるモデル機能と故障モードを, コンポーネント単位で評価することで明らかにする方法について述べる。
- 参考スコア（独自算出の注目度）: 38.37332307303914
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Formal theorem proving enables machine-verifiable evaluation of mathematical reasoning, yet existing benchmarks often emphasize aggregate proof accuracy, concentrate on a narrow range of mathematics, and provide limited evidence of robustness to equivalent reformulations. We introduce MathAdv, a diagnostic benchmark spanning 13 domains across undergraduate- and graduate-level mathematics. Alongside Lean 4 theorem proving, MathAdv provides up to three auxiliary tasks: multiple-choice questions that probe mathematical knowledge, fill-in-the-blank problems that isolate informal reasoning, and expert-crafted transformations that test robustness to problem presentation. Our evaluation of contemporary theorem provers yields four findings: formalization remains a major bottleneck; performance varies substantially across mathematical domains; natural-language guidance helps general-purpose LLMs but can hinder proof-specialized models; and mathematically equivalent reformulations expose substantial robustness limitations. Together, these results show how component-wise evaluation can reveal model capabilities and failure modes that aggregate theorem-proving accuracy obscures. The dataset and evaluation scripts are available at https://github.com/margotyjx/MathAdv.git.
- Abstract（参考訳）: 形式的定理証明は、数学的推論の機械的検証を可能にするが、既存のベンチマークは、しばしば集合的証明の正確さを強調し、数学の狭い範囲に集中し、等価な修正に対する堅牢性の限られた証拠を提供する。
我々は、13のドメインにまたがる診断ベンチマークであるMathAdvを紹介した。
数学的な知識を探索する複数選択の質問、非公式な推論を分離するブランク問題の補足、問題提示に対する堅牢性をテストする専門家による変換である。
形式化は数学の領域によって大きく異なる; 自然言語指導は汎用LLMを補助するが、証明専用モデルを妨げる; 数学的に等価な改定は、かなりの頑健さの限界を示す。
これらの結果から, 定理証明精度が不明瞭であるモデル機能と故障モードが, 構成的評価によってどのように明らかになるかが分かる。
データセットと評価スクリプトはhttps://github.com/margotyjx/MathAdv.gitで公開されている。
関連論文リスト
- MathCoPilot: An Interactive System for Human-AI Symbiotic Paradigm of Mathematical Research [62.221184989046826]
MathCoPilotは、数学研究のための新しいAI共生パラダイムを具現化したループシステムである。
MathCoPilotは3つのコア機能を統合する: 証明をナビゲート可能なステップに分解するインタラクティブな証明青写真、適応的な知識ベース検索とリーン統合された反復検証を備えた自動証明スキルオーケストレーション、トピック駆動の紙検索と自動形式化を検証可能なリーン知識ベースに統合する。
論文 参考訳（メタデータ） (2026-07-16T05:22:40Z) - From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier [109.93387172162984]
AI4Mathシステムの次の飛躍は、事前に定義された問題解決者から研究エージェントへの決定的なシフトを必要とする。
この分野の体系的なレビューを行い、データセット、自動形式化、証明合成について紹介する。
論文 参考訳（メタデータ） (2026-07-08T17:46:36Z) - MA-ProofBench: A Two-Tiered Evaluation of LLMs for Theorem Proving in Mathematical Analysis [28.906916840252077]
MA-ProofBenchは数学解析に特化した最初の公式な定理証明ベンチマークである。
ベンチマークには6つのコアトピックと27のサブカテゴリをカバーする200の形式化された定理が含まれており、測定と積分理論、複素解析、関数解析が含まれる。
我々は、MA-ProofBench上での最近の汎用推論モデルと形式定理プロバーについて評価する。
論文 参考訳（メタデータ） (2026-06-11T18:00:04Z) - CAM-Bench: A Benchmark for Computational and Applied Mathematics in Lean [10.684401671916158]
CAM-Benchは、計算および応用数学における1000のリーン証明目標のLean 4定理証明ベンチマークである。
これらの問題は教科書の演習に適応しており、しばしばローカルに導入された定義、表記法、アルゴリズム、基礎的な結果に依存している。
リーンコンパイルとセマンティックレビューを通じて、結果のフォーマルな問題を検証し、フォーマルな正当性とセマンティックなアライメントの両方を元のエクササイズで確認します。
論文 参考訳（メタデータ） (2026-05-17T04:53:47Z) - LiveMathematicianBench: A Live Benchmark for Mathematician-Level Reasoning with Proof Sketches [61.30693283718321]
研究レベルの数学的推論のための動的多重選択ベンチマークであるLiveMathematicianBenchを提案する。
新たに発表された定理で評価を基礎づけることで、記憶されたパターンを超えた現実的なテストベッドを提供する。
このパイプラインは、高レベルな証明戦略を使用して、妥当だが無効な解選択を構築する。
論文 参考訳（メタデータ） (2026-04-02T08:22:17Z) - DeepTheorem: Advancing LLM Reasoning for Theorem Proving Through Natural Language and Reinforcement Learning [67.93945726549289]
DeepTheoremは、数学的推論を強化するために自然言語を活用する包括的な非公式な定理証明フレームワークである。
DeepTheoremには、121Kの高品質なIMOレベルの非公式な定理と証明からなる大規模なベンチマークデータセットが含まれている。
我々は、証明された定理の変種を利用して堅牢な数学的推論を動機付けることによって、非公式な定理証明に適した新しい強化学習戦略(RL-Zero)を考案する。
論文 参考訳（メタデータ） (2025-05-29T17:59:39Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。