論文の概要: LemmaBench: A Live, Research-Level Benchmark to Evaluate LLM Capabilities in Mathematics
- arxiv url: http://arxiv.org/abs/2602.24173v1
- Date: Fri, 27 Feb 2026 16:52:52 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-03-02 19:48:24.524548
- Title: LemmaBench: A Live, Research-Level Benchmark to Evaluate LLM Capabilities in Mathematics
- Title（参考訳）: LemmaBench: LLMの数学能力を評価するためのライブで研究レベルのベンチマーク
- Authors: Antoine Peyronnet, Fabian Gloeckle, Amaury Hayat,
- Abstract要約: 本研究では,研究レベルの数学において,大規模言語モデルの能力をベンチマークするための新しいアプローチを提案する。
既存のベンチマークは、数学研究のプロキシとして静的で手作業によるコンテストや教科書スタイルの問題に大きく依存している。
代わりに、最新の数学研究結果に基づいてモデルを直接評価する最新のベンチマークを確立する。
- 参考スコア（独自算出の注目度）: 5.676144562388248
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: We present a new approach for benchmarking Large Language Model (LLM) capabilities on research-level mathematics. Existing benchmarks largely rely on static, hand-curated sets of contest or textbook-style problems as proxies for mathematical research. Instead, we establish an updatable benchmark evaluating models directly on the latest research results in mathematics. This consists of an automatic pipeline that extracts lemmas from arXiv and rewrites them into self-contained statements by making all assumptions and required definitions explicit. It results in a benchmark that can be updated regularly with new problems taken directly from human mathematical research, while previous instances can be used for training without compromising future evaluations. We benchmark current state-of-the-art LLMs, which obtain around 10-15$\%$ accuracy in theorem proving (pass@1) depending on the model, showing that there is currently a large margin of progression for LLMs to reach human-level proving capabilities in a research context.
- Abstract（参考訳）: 本稿では,研究レベルの数学において,LLM(Large Language Model)の能力をベンチマークするための新しいアプローチを提案する。
既存のベンチマークは、数学研究のプロキシとして静的で手作業によるコンテストや教科書スタイルの問題に大きく依存している。
代わりに、最新の数学研究結果に基づいてモデルを直接評価する最新のベンチマークを確立する。
これは、arXivからレムマを抽出し、すべての仮定と必要な定義を明確にすることで、それらを自己完結したステートメントに書き換える自動パイプラインで構成されている。
その結果、人間の数学的研究から直接取られた新しい問題に対して定期的に更新できるベンチマークが得られ、以前のインスタンスは将来の評価を損なうことなくトレーニングに使用できる。
現状のLCMをベンチマークし,そのモデルによる定理証明(pass@1)の精度が約10～15$$%であることを示す。
関連論文リスト
- EternalMath: A Living Benchmark of Frontier Mathematics that Evolves with Human Discovery [23.517907682810932]
我々は、フロンティア数学的推論を評価するための完全自動化された定理基底パイプラインを提案する。
このパイプラインは、最近のピアレビューされた数学的文献を実行可能で検証可能な推論タスクに変換する。
このパイプラインを適用すると、現代の研究論文から派生した進化的評価スイートである textbfEternalMath が生成される。
論文 参考訳（メタデータ） (2026-01-04T06:40:25Z) - MathArena: Evaluating LLMs on Uncontaminated Math Competitions [4.655668424508813]
MathArenaは、大きな言語モデル(LLM)を評価するための新しいベンチマークである。
繰り返し行われる数学コンペは、高品質で困難な問題のストリームを提供する。
MathArenaは、証明書込み機能の最初のベンチマークでもある。
論文 参考訳（メタデータ） (2025-05-29T09:28:06Z) - RealMath: A Continuous Benchmark for Evaluating Language Models on Research-Level Mathematics [30.778394290919582]
大規模言語モデル(LLM)における数学的推論を評価するための既存のベンチマークは、主に競合問題、公式な証明、人工的な問題に依存している。
論文や数理フォーラムから直接派生した新しいベンチマークであるRealMathを導入し,実数理タスクにおけるLLMの能力を評価する。
論文 参考訳（メタデータ） (2025-05-18T23:32:46Z) - Model Utility Law: Evaluating LLMs beyond Performance through Mechanism Interpretable Metric [99.56567010306807]
大規模言語モデル(LLM)は、学術、産業、そして日々のアプリケーションに欠かせないものになっている。
大規模言語モデル (LLM) 時代における評価の課題の1つは一般化問題である。
従来の性能スコアを補完するメカニズムの解釈可能性向上指標であるモデル利用指数(MUI)を提案する。
論文 参考訳（メタデータ） (2025-04-10T04:09:47Z) - Sample, Don't Search: Rethinking Test-Time Alignment for Language Models [55.2480439325792]
新しいテストタイムアライメントアプローチであるQAlignを紹介します。
テスト時間計算をスケールする際、QAlignは各プロンプトの最適配向分布からのサンプリングに収束する。
マルコフ連鎖モンテカルロのテキスト生成における最近の進歩を取り入れることで、基礎となるモデルを変更したり、ロジットアクセスを必要とせずに、より良い整合出力を可能にする。
論文 参考訳（メタデータ） (2025-04-04T00:41:40Z) - 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) - LeanAgent: Lifelong Learning for Formal Theorem Proving [85.39415834798385]
フォーマルな定理証明のための新しい生涯学習フレームワークであるLeanAgentを紹介する。
LeanAgentは継続的に一般化し、拡張可能な数学的知識を改善します。
これは23のリーンリポジトリにわたる155の定理の正式な証明を生成する。
論文 参考訳（メタデータ） (2024-10-08T17:11:24Z) - MathHay: An Automated Benchmark for Long-Context Mathematical Reasoning in LLMs [61.74749961334557]
MathHayは、LLMの長文数学的推論能力を評価するために設計された自動ベンチマークである。
我々は,8つのトップパフォーマンスモデルの長文数学的推論能力を評価するために,MathHayの広範な実験を行った。
論文 参考訳（メタデータ） (2024-10-07T02:30:07Z) - Benchmarking Uncertainty Quantification Methods for Large Language Models with LM-Polygraph [83.90988015005934]
不確実性定量化は機械学習アプリケーションにおいて重要な要素である。
最新のUQベースラインの集合を実装した新しいベンチマークを導入する。
我々は、11タスクにわたるUQと正規化技術に関する大規模な実証的研究を行い、最も効果的なアプローチを特定した。
論文 参考訳（メタデータ） (2024-06-21T20:06:31Z) - Mathador-LM: A Dynamic Benchmark for Mathematical Reasoning on Large Language Models [34.814875040792344]
大規模言語モデル(LLM)の数学的推論を評価するための新しいベンチマークであるMathador-LMを紹介する。
Mathador-LMはMathadorゲームにインスパイアされており、そのゲームの目的は、与えられた基本数の集合の基本的な算術演算を用いてターゲット数に到達することである。
先行するLLMに対して,目標の難易度に従って,ベンチマークインスタンスを動的に生成しながら,安定した平均性能が得られることを示す。
論文 参考訳（メタデータ） (2024-06-18T13:02:12Z) - GSM-Plus: A Comprehensive Benchmark for Evaluating the Robustness of LLMs as Mathematical Problem Solvers [68.77382332826167]
大規模言語モデル (LLM) は、様々な数学的推論ベンチマークで顕著な性能を達成している。
1つの必須かつ頻繁な証拠は、数学の質問がわずかに変更されたとき、LLMは誤って振る舞うことができることである。
このことは, LLMの数学推論能力の頑健性を評価するために, 幅広い質問のバリエーションを試すことによるものである。
論文 参考訳（メタデータ） (2024-02-29T15:26:14Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。