論文の概要: LiveMathematicianBench: A Live Benchmark for Mathematician-Level Reasoning with Proof Sketches
- arxiv url: http://arxiv.org/abs/2604.01754v1
- Date: Thu, 02 Apr 2026 08:22:17 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-04-03 14:21:10.609431
- Title: LiveMathematicianBench: A Live Benchmark for Mathematician-Level Reasoning with Proof Sketches
- Title（参考訳）: LiveMathematicianBench: Proof Sketchesを使った数学レベル推論のためのライブベンチマーク
- Abstract要約: 研究レベルの数学的推論のための動的多重選択ベンチマークであるLiveMathematicianBenchを提案する。
新たに発表された定理で評価を基礎づけることで、記憶されたパターンを超えた現実的なテストベッドを提供する。
このパイプラインは、高レベルな証明戦略を使用して、妥当だが無効な解選択を構築する。
- 参考スコア（独自算出の注目度）: 61.30693283718321
- License: http://creativecommons.org/licenses/by-nc-nd/4.0/
- Abstract: Mathematical reasoning is a hallmark of human intelligence, and whether large language models (LLMs) can meaningfully perform it remains a central question in artificial intelligence and cognitive science. As LLMs are increasingly integrated into scientific workflows, rigorous evaluation of their mathematical capabilities becomes a practical necessity. Existing benchmarks are limited by synthetic settings and data contamination. We present LiveMathematicianBench, a dynamic multiple-choice benchmark for research-level mathematical reasoning built from recent arXiv papers published after model training cutoffs. By grounding evaluation in newly published theorems, it provides a realistic testbed beyond memorized patterns. The benchmark introduces a thirteen-category logical taxonomy of theorem types (e.g., implication, equivalence, existence, uniqueness), enabling fine-grained evaluation across reasoning forms. It employs a proof-sketch-guided distractor pipeline that uses high-level proof strategies to construct plausible but invalid answer choices reflecting misleading proof directions, increasing sensitivity to genuine understanding over surface-level matching. We also introduce a substitution-resistant mechanism to distinguish answer recognition from substantive reasoning. Evaluation shows the benchmark is far from saturated: Gemini-3.1-pro-preview, the best model, achieves only 43.5%. Under substitution-resistant evaluation, accuracy drops sharply: GPT-5.4 scores highest at 30.6%, while Gemini-3.1-pro-preview falls to 17.6%, below the 20% random baseline. A dual-mode protocol reveals that proof-sketch access yields consistent accuracy gains, suggesting models can leverage high-level proof strategies for reasoning. Overall, LiveMathematicianBench offers a scalable, contamination-resistant testbed for studying research-level mathematical reasoning in LLMs.
- Abstract（参考訳）: 数学的推論は人間の知能の目印であり、大きな言語モデル(LLM)が有意義に実行できるかは、人工知能と認知科学の中心的な問題である。
LLMが科学的なワークフローに統合されるにつれて、その数学的能力の厳密な評価が現実的に必要となる。
既存のベンチマークは、合成設定とデータ汚染によって制限されている。
我々は,最近のarXiv論文から構築された研究レベルの数学的推論のための動的多重選択ベンチマークであるLiveMathematicianBenchを紹介する。
新たに発表された定理で評価を基礎づけることで、記憶されたパターンを超えた現実的なテストベッドを提供する。
このベンチマークでは、定理型(例えば、含意、等価性、存在、特異性)の13カテゴリの論理分類を導入し、推論形式全体にわたってきめ細かい評価を可能にした。
このパイプラインは、高レベルな証明戦略を用いて、誤解を招く証明方向を反映した、妥当だが無効な回答選択を構築し、表面レベルのマッチングに対する真の理解に対する感度を高める。
また,回答認識と実体的推論を区別する置換耐性機構も導入した。
Gemini-3.1-pro-previewは最高のモデルであり、43.5%しか達成していない。
GPT-5.4は30.6%、Gemini-3.1-pro-previewは20%のランダムベースライン以下17.6%である。
デュアルモードプロトコルは、証明スケッチアクセスが一貫した精度向上をもたらすことを明らかにし、モデルが推論のために高いレベルの証明戦略を活用できることを示唆する。
全体として、LiveMathematicianBenchはLLMの研究レベルの数学的推論を研究するために、スケーラブルで汚染に強いテストベッドを提供する。
関連論文リスト
- MathAdv: What Theorem Provers Know, Reason, Formalize, and Generalize [38.37332307303914]
MathAdvは、学部および大学院レベルの数学で13のドメインにまたがる診断ベンチマークである。
本稿では, 定理証明精度が不明瞭であるモデル機能と故障モードを, コンポーネント単位で評価することで明らかにする方法について述べる。
論文 参考訳（メタデータ） (2026-08-26T07:12:54Z) - MathCoPilot: An Interactive System for Human-AI Symbiotic Paradigm of Mathematical Research [62.221184989046826]
MathCoPilotは、数学研究のための新しいAI共生パラダイムを具現化したループシステムである。
MathCoPilotは3つのコア機能を統合する: 証明をナビゲート可能なステップに分解するインタラクティブな証明青写真、適応的な知識ベース検索とリーン統合された反復検証を備えた自動証明スキルオーケストレーション、トピック駆動の紙検索と自動形式化を検証可能なリーン知識ベースに統合する。
論文 参考訳（メタデータ） (2026-07-16T05:22:40Z) - 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) - LemmaBench: A Live, Research-Level Benchmark to Evaluate LLM Capabilities in Mathematics [5.676144562388248]
本研究では,研究レベルの数学において,大規模言語モデルの能力をベンチマークするための新しいアプローチを提案する。
既存のベンチマークは、数学研究のプロキシとして静的で手作業によるコンテストや教科書スタイルの問題に大きく依存している。
代わりに、最新の数学研究結果に基づいてモデルを直接評価する最新のベンチマークを確立する。
論文 参考訳（メタデータ） (2026-02-27T16:52:52Z) - ARCHE: A Novel Task to Evaluate LLMs on Latent Reasoning Chain Extraction [70.53044880892196]
本稿では、複雑な推論引数を標準推論パラダイムの組み合わせに分解し、Reasoning Logic Tree (RLT) という形で分解しなければならない、ARCHE(Latent Reasoning Chain extract)という新しいタスクを紹介する。
この作業を容易にするために,我々は,1,900以上の参照と38,000の視点を含む70のNature Communicationsの記事から得られた新しいベンチマークであるARCHE Benchをリリースする。
ARCHE Bench上での10のLLMの評価では、モデルがREAとECのトレードオフを示しており、完全な標準推論チェーンを抽出することはできません。
論文 参考訳（メタデータ） (2025-11-16T07:37:09Z) - Are Language Models Efficient Reasoners? A Perspective from Logic Programming [109.47572890883248]
現代言語モデル(LM)は、強い推論能力を示すが、標準的な評価は、人間のような推論の重要な側面である効率性を見越しながら、正確性を強調する。
本稿では、論理プログラミングのレンズを用いて、LM推論効率を評価するためのフレームワークを提案する。
論文 参考訳（メタデータ） (2025-10-29T15:30:31Z) - Do LLMs Overthink Basic Math Reasoning? Benchmarking the Accuracy-Efficiency Tradeoff in Language Models [6.312798900093575]
大規模言語モデル (LLM) は複雑な数学的ベンチマークでは優れた性能を得るが、基本的な数学的推論では失敗することがある。
本稿では,正確さと過度に考えることの基本的なトレードオフに焦点を当てる。
本研究は,総合モデル評価のための高精度とトークン効率を組み合わせた調和平均計量であるOverthinking Scoreを紹介する。
論文 参考訳（メタデータ） (2025-07-05T12:31:17Z) - Solving Inequality Proofs with Large Language Models [42.667163027148916]
不等式証明は様々な科学・数学分野において不可欠である。
これにより、大きな言語モデル(LLM)の需要が高まるフロンティアとなる。
我々は、Olympiadレベルの不平等を専門家が計算したデータセットであるIneqMathをリリースした。
論文 参考訳（メタデータ） (2025-06-09T16:43:38Z) - Formal Theorem Proving by Rewarding LLMs to Decompose Proofs Hierarchically [29.908878832382523]
本稿では,自動検証/評価を可能にする形式言語による証明記述能力の向上に焦点をあてる。
我々は、定理に直接関係する補題がテスト時の定理証明者に与えられないより自然な設定で作業する。
我々は、モデルが定理を補題に分解し、補題を証明し、補題を用いて定理を証明することを奨励するRLベースの訓練アルゴリズムを設計する。
論文 参考訳（メタデータ） (2024-11-04T05:57:40Z) - Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。
Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
論文 参考訳（メタデータ） (2024-07-14T01:43:07Z) - MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。
5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。
我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
論文 参考訳（メタデータ） (2024-02-14T05:57:58Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。