論文の概要: ReuF2F: Benchmarking Coding Agents on Formalized Undergraduate Research Problems
- arxiv url: http://arxiv.org/abs/2610.27046v1
- Date: Mon, 19 Oct 2026 17:52:28 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-10-21 21:58:47.440209
- Title: ReuF2F: Benchmarking Coding Agents on Formalized Undergraduate Research Problems
- Title（参考訳）: ReuF2F:形式化学部研究問題におけるベンチマークコーディングエージェント
- Abstract要約: 我々はReuF2Fを紹介します。ReuF2Fは、REU(Research Experiences for Undergraduates)から引き出された244の形式化されたオープンな問題のリーン4ベンチマークです。
標準のコーディングエージェント評価設定を採用し、各問題とその論理的否定を、Dockerコンテナ内のリーンプロジェクトに配置します。
評価の結果,最も優れたモデルでも40%しか解決できず,形式化されたオープンリサーチ問題の改善の余地が残されていることがわかった。
- 参考スコア（独自算出の注目度）: 45.6989701160515
- License: http://creativecommons.org/licenses/by-nc-sa/4.0/
- Abstract: As AI systems begin to resolve open research problems, reliable verification becomes increasingly important. Formal mathematics provides a trusted framework for mathematical reasoning, enabling agents to produce machine-checkable proofs while conducting mathematical exploration. Existing formal mathematics benchmarks often focus on known results or a small set of prominent open problems, which can become difficult to evaluate reliably once solutions are discovered and widely disseminated. Existing evaluation protocols are also not always aligned with how modern coding agents operate. We therefore introduce ReuF2F, a Lean 4 benchmark of 244 formalized open problems drawn from Research Experiences for Undergraduates (REU), spanning entry-level open research problems across a broad range of mathematical subfields. We expect these less prominent open problems, which tend to attract less attention and may remain unsolved for longer, to be better suited for held-out evaluation of end-to-end open problem resolution in Lean. We adopt a standard coding-agent evaluation setting, placing each problem and its logical negation into a Lean project in a Docker container. We also build Leanimum-agent on mini-SWE-agent to provide a unified harness for fair comparisons across models. Our evaluation finds that even the best-performing model resolves only ~40% of the problems, leaving substantial room for improvement on formalized open research problems.
- Abstract（参考訳）: AIシステムがオープンな研究課題を解決し始めると、信頼性の高い検証がますます重要になる。
形式数学は数学的推論のための信頼できる枠組みを提供し、エージェントは数学的探索を行いながら機械検査可能な証明を作成できる。
既存の公式な数学のベンチマークは、既知の結果やいくつかの顕著なオープンな問題に焦点をあてることが多く、解が発見され、広く普及すると、確実に評価することが困難になる。
既存の評価プロトコルは、現代のコーディングエージェントの動作方法と必ずしも一致していない。
そこで我々は、REU(Research Experiences for Undergraduates)から引き出された244のオープン問題に関するLean 4ベンチマークであるReuF2Fを紹介した。
リーンのエンドツーエンドのオープンな問題解決の持続的評価に、これらの顕著なオープンな問題は、注意を惹きつけず、長く未解決のままである傾向にある、と私たちは期待しています。
標準のコーディングエージェント評価設定を採用し、各問題とその論理的否定を、Dockerコンテナ内のリーンプロジェクトに配置します。
また、ミニSWEエージェント上にLeanimum-agentを構築し、モデル間の公正な比較のための統一されたハーネスを提供しています。
評価の結果,最高の性能モデルでも40%程度しか解決できず,形式化されたオープンリサーチ問題の改善の余地が残されていることがわかった。
関連論文リスト
- Iteris: Agentic Research Loops for Computational Mathematics [7.052820770689716]
本稿では,計算数学におけるオープンな問題に対するエージェント研究システムであるイテリスを紹介する。
我々は最近のSimons Workshopコレクションからイテリスを2つのオープンな問題に適用した。
イテリスは数値的な証拠、建設、証明の草案を作成し、専門家のレビューと修正を経て、検証結果に繋がった。
論文 参考訳（メタデータ） (2026-06-01T16:54:31Z) - RMA: an Agentic System for Research-Level Mathematical Problems [30.952480229786236]
研究数学エージェント(Research Math Agents、RMA)は、研究レベルの数学的問題に対する自動推論のためのエージェントフレームワークである。
RMAは、研究レベルの証明を、問題解析、文献検索と理解、公正比較、知識銀行構築、証明検証のための特殊なモジュールに分解する。
論文 参考訳（メタデータ） (2026-05-20T04:54:22Z) - Formal Conjectures: An Open and Evolving Benchmark for Verified Discovery in Mathematics [9.38309744591661]
フォーマル・コンジェクチャ(Formal Conjectures)は、Lean 4.0で形式化された2615の数学的問題文の進化ベンチマークである。
このデータセットは、数学的な証明発見のためのゼロ汚染ベンチマークを提供する1029のオープンリサーチ予想を特徴としている。
我々は,これらの形式化の正しさを保証するためのアプローチを,アクティブなコミュニティからのコントリビューションを生かしたオープンソースプロジェクトとして紹介する。
論文 参考訳（メタデータ） (2026-05-13T08:33:15Z) - Riemann-Bench: A Benchmark for Moonshot Mathematics [0.12430801435092285]
近年のAIシステムは国際数学オリンピックでゴールド・メディカルレベルのパフォーマンスを達成した。
我々は、研究レベルの数学におけるAIシステムを評価するために設計された25のエキスパートキュレートされた問題のプライベートベンチマークであるベンチを紹介する。
論文 参考訳（メタデータ） (2026-04-08T08:16:37Z) - BeyondSWE: Can Current Code Agent Survive Beyond Single-Repo Bug Fixing? [61.247730037229815]
BeyondSWEは2つの軸 – 解像度スコープと知識スコープ – に沿って既存の評価を拡張する包括的なベンチマークです。
外部知識の役割を解明するために,ディープ検索とコーディング能力を統合するフレームワークであるSearchSWEを開発した。
この作業は、現実的で挑戦的な評価ベンチマークと、より有能なコードエージェントに向けた研究を進めるための柔軟なフレームワークの両方を提供する。
論文 参考訳（メタデータ） (2026-03-03T17:52:01Z) - Barbarians at the Gate: How AI is Upending Systems Research [58.95406995634148]
システム研究は、新しいパフォーマンス指向アルゴリズムの設計と評価に長年注力してきたが、AI駆動のソリューション発見には特に適している、と私たちは主張する。
このアプローチをAI駆動システム研究(ADRS)と呼び、ソリューションを反復的に生成し、評価し、洗練する。
我々の研究結果は、AI時代のシステム研究の実践に急激な適応の必要性と破壊的な可能性を浮き彫りにしている。
論文 参考訳（メタデータ） (2025-10-07T17:49:24Z) - IMProofBench: Benchmarking AI on Research-Level Mathematical Proof Generation [4.991157581428135]
IMProofBenchは、専門家数学者によって開発された39のピアレビューされた問題からなるプライベートベンチマークである。
それぞれの問題は詳細な証明を必要とし、最終的な答えを持つサブプロブレムと組み合わせられる。
以前のベンチマークとは異なり、評価設定は現実的な研究環境をシミュレートする。
論文 参考訳（メタデータ） (2025-09-30T10:50:37Z) - 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) - ErrorRadar: Benchmarking Complex Mathematical Reasoning of Multimodal Large Language Models Via Error Detection [60.297079601066784]
エラー検出におけるMLLMの能力を評価するために設計された最初のベンチマークであるErrorRadarを紹介する。
ErrorRadarはエラーステップ識別とエラー分類という2つのサブタスクを評価している。
2500の高品質なマルチモーダルK-12数学問題で構成され、実世界の学生相互作用から収集される。
GPT-4oの優れた性能は、まだ人間の評価に約10%遅れているため、大きな課題が残っている。
論文 参考訳（メタデータ） (2024-10-06T14:59:09Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。