論文の概要: 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の数学能力を評価するためのライブで研究レベルのベンチマーク
• 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$$%であることを示す。

関連論文リスト

• MathCoPilot: An Interactive System for Human-AI Symbiotic Paradigm of Mathematical Research [62.221184989046826]
  MathCoPilotは、数学研究のための新しいAI共生パラダイムを具現化したループシステムである。 MathCoPilotは3つのコア機能を統合する: 証明をナビゲート可能なステップに分解するインタラクティブな証明青写真、適応的な知識ベース検索とリーン統合された反復検証を備えた自動証明スキルオーケストレーション、トピック駆動の紙検索と自動形式化を検証可能なリーン知識ベースに統合する。
  論文  参考訳（メタデータ） (2026-07-16T05:22:40Z)
• SABER-Math: Automated Benchmark for Information Retrieval Evaluation in Mathematics [4.685475117723465]
  専門家のアノテーションを使わずに数理IRを評価するための,最初の完全自動ベンチマークであるSABER-Mathを紹介する。 SABER-Mathは283Kのハイスクールレベルの数学問題から始まり、3つのステップでタスクのランク付けに挑戦する。 我々は、語彙検索器、特殊数式検索システム、最近の埋め込みモデルを評価する。
  論文  参考訳（メタデータ） (2026-06-29T07:32:50Z)
• LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks [85.86474267842907]
  大規模言語モデル(LLM)は、強力な非公式な数学的推論を示すが、リーンのような形式言語で検証可能な証明を生成するのに苦労している。 本稿では,汎用基礎モデルによる自動形式定理証明の最先端性能を実現するためのエージェントフレームワークであるLEAPを提案する。
  論文  参考訳（メタデータ） (2026-06-02T08:16:42Z)
• Beyond Benchmarks: MathArena as an Evaluation Platform for Mathematics with LLMs [4.559742899048613]
  我々は、その範囲を大幅に広げることで、オリジナルのMathArenaベンチマークを構築します。 MathArenaは現在、証明ベースの競争、研究レベルのarXiv問題、Leanでの正式な証明生成など、より広範なタスクをカバーしています。 最強のモデルであるGPT-5.5は、2026年のアメリカ数学オリンピックで98%、研究レベルの質問で74%に達した。
  論文  参考訳（メタデータ） (2026-05-01T13:56:34Z)
• LiveMathematicianBench: A Live Benchmark for Mathematician-Level Reasoning with Proof Sketches [61.30693283718321]
  研究レベルの数学的推論のための動的多重選択ベンチマークであるLiveMathematicianBenchを提案する。 新たに発表された定理で評価を基礎づけることで、記憶されたパターンを超えた現実的なテストベッドを提供する。 このパイプラインは、高レベルな証明戦略を使用して、妥当だが無効な解選択を構築する。
  論文  参考訳（メタデータ） (2026-04-02T08:22:17Z)
• 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)

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

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