論文の概要: Re$^2$Math: Benchmarking Theorem Retrieval in Research-Level Mathematics
- arxiv url: http://arxiv.org/abs/2605.09012v1
- Date: Sat, 09 May 2026 15:52:49 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-05-12 23:28:50.019575
- Title: Re$^2$Math: Benchmarking Theorem Retrieval in Research-Level Mathematics
- Title（参考訳）: Re$2$Math: 研究レベル数学におけるベンチマーク理論の検索
- Abstract要約: 証明が不十分なステップに達すると、有用なアシスタントが必要なツールがすでに存在するかどうかを判断する必要がある。
Re$2$Mathは、部分数学的証明からツールグラウンドで検索するためのベンチマークである。
- 参考スコア（独自算出の注目度）: 20.784132035246696
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Large language models are increasingly capable at closed-world mathematical reasoning, but research assistance also requires source-grounded use of the literature. When a proof reaches a non-trivial step, a useful assistant should determine whether the needed tool (e.g., a lemma) already exists, identify a suitable scholarly source, and verify that its assumptions align with the current proof context. To rigorously evaluate such capabilities, we introduce Re$^2$Math, a benchmark for tool-grounded retrieval from partial mathematical proofs. Each instance is built from a candidate instrumental citation in the proof of a main theorem, with hierarchical context and an optional leakage-controlled anchor hint. We also make the task source-grounded yet citation-agnostic in that any admissible theorem sufficient for the proof transition is accepted. Evaluation uses a release-frozen retrieval artifact, ensuring reproducibility, while the benchmark itself supports automatic, continual expansion with newly constructed instances. On the current benchmark test set, the best fixed-judge ToolAcc reaches 7.0%, despite substantially higher rates of source grounding, indicating that current systems often retrieve valid statements but fail to establish their applicability to the local proof step. By decoupling citation recall, grounding, and proof-gap sufficiency, Re$^2$Math transforms literature-grounded mathematical tool use into a controlled diagnostic task.
- Abstract（参考訳）: 大規模言語モデルは、クローズドワールドな数学的推論の能力がますます高まっているが、研究補助には、文献のソースとしての利用も必要である。
証明が非自明なステップに達すると、有用なアシスタントは、必要なツール(例えば、補題)が既に存在するかどうかを判断し、適切な学術的情報源を特定し、その仮定が現在の証明コンテキストと一致することを検証する必要がある。
このような機能を厳格に評価するために,部分数学的証明からツールグラウンド検索を行うRe$^2$Mathを導入する。
各インスタンスは、主定理の証明において候補の楽器的引用から構築され、階層的文脈と任意のリーク制御されたアンカーヒントを持つ。
また、証明遷移に十分な許容定理が受け入れられるという点で、タスクの原点がまだ引用に依存しないようにしている。
評価にはリリースフリーズされた検索アーティファクトを使用し、再現性を確保する一方で、ベンチマーク自体が新たに構築されたインスタンスによる自動的な継続的拡張をサポートする。
現在のベンチマークテストセットでは、最も優れた固定ジョブツールAccが7.0%に達している。
Re$^2$Mathは、引用のリコール、グラウンド、証明ギャップの充足を分離することにより、文学的な地下の数学的ツールの使用を制御された診断タスクに変換する。
関連論文リスト
- LiveMathematicianBench: A Live Benchmark for Mathematician-Level Reasoning with Proof Sketches [61.30693283718321]
研究レベルの数学的推論のための動的多重選択ベンチマークであるLiveMathematicianBenchを提案する。
新たに発表された定理で評価を基礎づけることで、記憶されたパターンを超えた現実的なテストベッドを提供する。
このパイプラインは、高レベルな証明戦略を使用して、妥当だが無効な解選択を構築する。
論文 参考訳（メタデータ） (2026-04-02T08:22:17Z) - Compile to Compress: Boosting Formal Theorem Provers by Compiler Outputs [48.390500145598544]
大型言語モデル (LLM) は形式定理の証明において大きな可能性を証明している。
我々は形式的検証において情報的構造を利用する: コンパイラが多様な証明の試みの広大な空間をマッピングする観察である。
我々は,この圧縮を利用して効率的な学習と証明探索を行う,学習と再定義のためのフレームワークを提案する。
論文 参考訳（メタデータ） (2026-03-13T01:33:20Z) - LemmaBench: A Live, Research-Level Benchmark to Evaluate LLM Capabilities in Mathematics [5.676144562388248]
本研究では,研究レベルの数学において,大規模言語モデルの能力をベンチマークするための新しいアプローチを提案する。
既存のベンチマークは、数学研究のプロキシとして静的で手作業によるコンテストや教科書スタイルの問題に大きく依存している。
代わりに、最新の数学研究結果に基づいてモデルを直接評価する最新のベンチマークを確立する。
論文 参考訳（メタデータ） (2026-02-27T16:52:52Z) - CiteAudit: You Cited It, But Did You Read It? A Benchmark for Verifying Scientific References in the LLM Era [51.63024682584688]
大規模言語モデル (LLM) は新たなリスクを導入している。
本稿では,科学文献における幻覚的引用のための総合的なベンチマークおよび検出フレームワークについて紹介する。
我々のフレームワークは、精度と解釈可能性の両方において、先行手法を著しく上回っている。
論文 参考訳（メタデータ） (2026-02-26T19:17:39Z) - MathDoc: Benchmarking Structured Extraction and Active Refusal on Noisy Mathematics Exam Papers [22.091709845799784]
我々は,高校数学試験論文から文書レベルの情報を抽出する最初のベンチマークであるMathDocを紹介する。
幹の精度, 視覚的類似性, 拒絶能力を考慮した多次元評価フレームワークを提案する。
Qwen3-VL や Gemini-2.5-Pro など SOTA MLLM の実験では、エンド・ツー・エンドのモデルでは強力な抽出性能が得られたが、常に入力を拒否することはできなかった。
論文 参考訳（メタデータ） (2026-01-15T06:17:47Z) - Are Language Models Efficient Reasoners? A Perspective from Logic Programming [109.47572890883248]
現代言語モデル(LM)は、強い推論能力を示すが、標準的な評価は、人間のような推論の重要な側面である効率性を見越しながら、正確性を強調する。
本稿では、論理プログラミングのレンズを用いて、LM推論効率を評価するためのフレームワークを提案する。
論文 参考訳（メタデータ） (2025-10-29T15:30:31Z) - Solving Inequality Proofs with Large Language Models [42.667163027148916]
不等式証明は様々な科学・数学分野において不可欠である。
これにより、大きな言語モデル(LLM)の需要が高まるフロンティアとなる。
我々は、Olympiadレベルの不平等を専門家が計算したデータセットであるIneqMathをリリースした。
論文 参考訳（メタデータ） (2025-06-09T16:43:38Z) - MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。
5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。
我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
論文 参考訳（メタデータ） (2024-02-14T05:57:58Z) - A New Approach Towards Autoformalization [7.275550401145199]
オートフォーマル化(Autoformalization)は、自然言語をプログラムで検証可能な形式言語に変換するタスクである。
研究論文は大量の背景と文脈を必要とする。
本稿では,研究レベルの数学の自己形式化に取り組み,タスクをより容易に,より親しみやすいサブタスクに分割する手法を提案する。
論文 参考訳（メタデータ） (2023-10-12T00:50:24Z) - LeanDojo: Theorem Proving with Retrieval-Augmented Language Models [72.54339382005732]
大規模言語モデル(LLM)は、Leanのような証明アシスタントを使って形式的な定理を証明することを約束している。
既存のメソッドは、プライベートコード、データ、計算要求のために、複製や構築が難しい。
本稿では、ツールキット、データ、モデルからなるオープンソースのリーンツールキットであるLeanDojoを紹介します。
本研究では,LLM ベースの証明器 ReProver を開発した。
論文 参考訳（メタデータ） (2023-06-27T17:05:32Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。