論文の概要: ProofCouncil: An LLM Agent for Solving Open Mathematical Problems
- arxiv url: http://arxiv.org/abs/2607.09474v1
- Date: Fri, 10 Jul 2026 14:46:01 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-07-13 14:47:12.862942
- Title: ProofCouncil: An LLM Agent for Solving Open Mathematical Problems
- Title（参考訳）: ProofCouncil:オープンな数学的問題を解くためのLLMエージェント
- Abstract要約: 本稿では,著者批判アーキテクチャを用いてオープンな問題に対処する数学的エージェントProofCouncilを紹介する。
ProofCouncilは、エージェントが自律的に解決しなければならない10の現実の数学的問題からなるチャレンジであるFirstProofの第2バッチの提出として機能した。
人的フィードバックを受けた21のソリューションのうち、5は完全正当と判断され、さらに2つは有望な最終検証と判断され、さらに8つは有用な部分的な進歩を含んでいた。
- 参考スコア（独自算出の注目度）: 2.90620992303615
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Large language models (LLMs) have shown increasing promise in solving open problems in mathematics. However, their performance can be further improved through agentic workflows tailored to real-world mathematical practice. To this end, we introduce ProofCouncil, a mathematical agent that is designed to tackle open problems using an author-critic architecture. ProofCouncil served as a submission to the second batch of FirstProof, a challenge consisting of 10 real-world mathematical problems that agents must solve autonomously. Its submissions for 6 of the 10 problems were judged by the referees to be correct up to at most minor revisions, showing the best performance among participating teams. We also evaluate ProofCouncil on 30 open problems collected from mathematical researchers. Among the 21 solutions that received human feedback, 5 were judged completely correct, 2 more were judged promising pending final verification, and a further 8 contained useful partial progress. In this short paper, we describe the development of ProofCouncil and the agent-building library used to create it, which we release as open source to the community.
- Abstract（参考訳）: 大規模言語モデル (LLMs) は、数学におけるオープンな問題を解くことへの期待が高まっている。
しかし、それらの性能は現実世界の数学的実践に適したエージェントワークフローによってさらに改善することができる。
そこで本研究では,著者批判アーキテクチャを用いてオープンな問題に対処する数学的エージェントProofCouncilを紹介する。
ProofCouncilは、エージェントが自律的に解決しなければならない10の現実の数学的問題からなるチャレンジであるFirstProofの第2バッチの提出として機能した。
10つの問題のうち6つの問題への応募は、審判によって、ほとんどのマイナーリビジョンで修正されると判断され、参加チームの中で最高のパフォーマンスを示した。
また,ProofCouncilは数学研究者が収集した30のオープンな問題に対して評価を行う。
人的フィードバックを受けた21のソリューションのうち、5は完全正当と判断され、さらに2つは有望な最終検証と判断され、さらに8つは有用な部分的な進歩を含んでいた。
本稿では,ProofCouncilとエージェント構築ライブラリの開発について述べる。
関連論文リスト
- MathCoPilot: An Interactive System for Human-AI Symbiotic Paradigm of Mathematical Research [62.221184989046826]
MathCoPilotは、数学研究のための新しいAI共生パラダイムを具現化したループシステムである。
MathCoPilotは3つのコア機能を統合する: 証明をナビゲート可能なステップに分解するインタラクティブな証明青写真、適応的な知識ベース検索とリーン統合された反復検証を備えた自動証明スキルオーケストレーション、トピック駆動の紙検索と自動形式化を検証可能なリーン知識ベースに統合する。
論文 参考訳（メタデータ） (2026-07-16T05:22:40Z) - CrowdMath: A Dataset of Crowdsourced Mathematical Research Discussions [7.449578020792231]
我々は、MIT PRIMES--Art of Problem Solving (AoPS)プログラムから164のエキスパートアノテートプログレスチェーンのデータセットであるCrowdMathを紹介する。
各チェーンは、オープンプロブレムステートメントから完成した証明まで、多人数のフォーラムディスカッションをトレースする。
モデルは次のポスト予測において83～88%の精度を達成し、数学的議論の局所的な流れに従うことができることを示唆している。
論文 参考訳（メタデータ） (2026-06-02T20:38:39Z) - LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks [85.86474267842907]
大規模言語モデル(LLM)は、強力な非公式な数学的推論を示すが、リーンのような形式言語で検証可能な証明を生成するのに苦労している。
本稿では,汎用基礎モデルによる自動形式定理証明の最先端性能を実現するためのエージェントフレームワークであるLEAPを提案する。
論文 参考訳（メタデータ） (2026-06-02T08:16:42Z) - Riemann-Bench: A Benchmark for Moonshot Mathematics [0.12430801435092285]
近年のAIシステムは国際数学オリンピックでゴールド・メディカルレベルのパフォーマンスを達成した。
我々は、研究レベルの数学におけるAIシステムを評価するために設計された25のエキスパートキュレートされた問題のプライベートベンチマークであるベンチを紹介する。
論文 参考訳（メタデータ） (2026-04-08T08:16:37Z) - Can MLLMs Read Students' Minds? Unpacking Multimodal Error Analysis in Handwritten Math [55.83696908107408]
スクラッチマス(ScratchMath)は,手書き数学のスクラッチワークにおける誤りの説明と分類のための新しいベンチマークである。
本データセットは,中国初等・中等生の1,720個の数学サンプルからなる。
我々は,ScratchMath上での16のMLLMを系統的に評価し,人的専門家に対する顕著な性能差を明らかにした。
論文 参考訳（メタデータ） (2026-03-26T02:57:20Z) - HorizonMath: Measuring AI Progress Toward Mathematical Discovery with Automatic Verification [54.06301039725887]
計算および応用数学において8つの領域にまたがる100以上の未解決問題のベンチマークであるHorizonMathを紹介する。
我々のベンチマークは、発見が困難であり、意味のある数学的洞察を必要とする問題のクラスをターゲットにしているが、検証は計算的に効率的で簡単なものである。
論文 参考訳（メタデータ） (2026-03-16T17:59:53Z) - Can a Lightweight Automated AI Pipeline Solve Research-Level Mathematical Problems? [1.8139694172697178]
大規模言語モデル(LLM)は、最近、厳密な数学的証明を生成することに成功している。
次世代モデル(例えば、Gemini 3 Pro, GPT-5.2 Pro)が洗練された研究グレードの問題を解決することを実証する。
論文 参考訳（メタデータ） (2026-02-14T09:36:24Z) - CombiGraph-Vis: A Curated Multimodal Olympiad Benchmark for Discrete Mathematical Reasoning [3.609560822507327]
State-of-the-art (SOTA) LLMは、証明ベースのOlympiad問題から、IMO 2025問題のほとんどを解決するまで、進歩してきた。
本稿では,90 Gemini 2.5 Pro生成ソリューションのコーパスを用いて,詳細なエラーアノテーションを用いた1-4スケールで評価を行った。
分析の結果、モデルが不正確な解を確実にフラグ付けできるが、部分クレジットの割り当て方法にキャリブレーションのギャップがあることがわかった。
論文 参考訳（メタデータ） (2025-10-31T01:31:58Z) - RefGrader: Automated Grading of Mathematical Competition Proofs using Agentic Workflows [8.700422995850152]
State-of-the-art (SOTA) LLMは、証明ベースのOlympiad問題から、IMO 2025問題のほとんどを解決するまで、進歩してきた。
本稿では,90 Gemini 2.5 Pro生成ソリューションのコーパスを用いて,詳細なエラーアノテーションを用いた1-4スケールで評価を行った。
分析の結果、モデルが不正確な解を確実にフラグ付けできるが、部分クレジットの割り当て方法にキャリブレーションのギャップがあることがわかった。
論文 参考訳（メタデータ） (2025-10-10T05:47:40Z) - TheoremQA: A Theorem-driven Question Answering dataset [100.39878559382694]
GPT-4のこれらの問題を解決する能力は非並列であり、Program-of-Thoughts Promptingの精度は51%である。
TheoremQAは、350の定理をカバーする800の高品質な質問を含むドメインの専門家によってキュレートされる。
論文 参考訳（メタデータ） (2023-05-21T17:51:35Z) - Learning by Fixing: Solving Math Word Problems with Weak Supervision [70.62896781438694]
数学用語問題(mwps)の従来のニューラルネットワークソルバは、完全な監視によって学習され、多様なソリューションを生み出すことができない。
MWPを学習するためのテキスト弱教師付きパラダイムを提案する。
この手法は最終回答のアノテーションのみを必要とし、単一の問題に対して様々な解決策を生成できる。
論文 参考訳（メタデータ） (2020-12-19T03:10:21Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。