論文の概要: QED: An Open-Source Multi-Agent System for Generating Mathematical Proofs on Open Problems
- arxiv url: http://arxiv.org/abs/2604.24021v2
- Date: Wed, 29 Apr 2026 19:53:30 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-05-01 14:06:12.640049
- Title: QED: An Open-Source Multi-Agent System for Generating Mathematical Proofs on Open Problems
- Title（参考訳）: QED: オープン問題に関する数学的証明を生成するためのオープンソースのマルチエージェントシステム
- Authors: Chenyang An, Qihao Ye, Minghao Pan, Jiayaun Zhang,
- Abstract要約: ベンチマークの成功と研究レベルの証明のギャップは,主にシステム設計の1つである,と我々は主張する。
アーキテクチャ上の各決定が特定の障害モードに直接対処する,オープンソースのマルチエージェント証明システムであるQEDを提案する。
- 参考スコア（独自算出の注目度）: 2.994333558834796
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: We explore a central question in AI for mathematics: can AI systems produce original, nontrivial proofs for open research problems? Despite strong benchmark performance, producing genuinely novel proofs remains an outstanding challenge for LLMs. Through systematic experiments with frontier LLMs on research-level proof tasks, we identify seven failure modes that prevent reliable proof generation, including context contamination, citation hallucination, hand-waving on key steps and misallocation of proof effort, unstable proof plans, unfocused verification, problem modification and single-model bottleneck. We argue that the gap between benchmark success and research-level proving is primarily one of system design, due to those failure modes. We present QED, an open-source multi-agent proof system in which each architectural decision directly addresses a specific failure mode. Evaluated on five open problems in applied analysis and PDEs contributed by domain experts, QED produces correct proofs for three problems, each verified by the contributing experts as original and nontrivial. QED is released as open-source software at https://github.com/proofQED/QED.
- Abstract（参考訳）: AIシステムは、オープンな研究問題に対して、独創的で非自明な証明を生成できるだろうか?
ベンチマーク性能は高いが、真に新しい証明を生成することは、LLMにとって大きな課題である。
研究レベルの証明タスクに関するフロンティアのLLMを用いた系統的な実験により、コンテキスト汚染、引用幻覚、キーステップによる手作業、証明作業の誤り、不安定な証明計画、未集中検証、問題修正、単一モデルボトルネックなど、信頼性の高い証明生成を防止する7つの障害モードを同定する。
ベンチマークの成功と研究レベルの証明のギャップは、主にシステム設計の1つであり、これらの障害モードのためである、と我々は主張する。
アーキテクチャ上の各決定が特定の障害モードに直接対処する,オープンソースのマルチエージェント証明システムであるQEDを提案する。
応用分析とドメインの専門家によるPDEの5つのオープンな問題に基づいて評価され、QEDは3つの問題に対して正しい証明を生成する。
QEDはhttps://github.com/proofQED/QEDでオープンソースソフトウェアとしてリリースされた。
関連論文リスト
- Automated Self-Testing as a Quality Gate: Evidence-Driven Release Management for LLM Applications [51.56484100374058]
我々は,エビデンスに基づくリリース決定を伴う品質ゲートを導入する自動自己テストフレームワークを提案する。
内部展開型多エージェント対話型AIシステムの縦型ケーススタディにより,本フレームワークの評価を行った。
論文 参考訳（メタデータ） (2026-03-13T20:44:15Z) - Proof-RM: A Scalable and Generalizable Reward Model for Math Proof [67.53066972145183]
大規模言語モデル(LLM)は,*検証リワード*(RLVR)を用いた強化学習を通じて,強力な数学推論能力を示した。
多くの先進的な数学的問題は証明ベースであり、単純な解マッチングによって証明の真性を決定するための保証された方法はない。
自動検証を実現するには、完全な証明プロセスを確実に評価できるリワードモデル(RM)が必要である。
論文 参考訳（メタデータ） (2026-02-02T17:42:53Z) - GeoBench: Rethinking Multimodal Geometric Problem-Solving via Hierarchical Evaluation [48.04396968707237]
幾何学的問題解決における4つの推論レベルを特徴とする階層型ベンチマークであるGeoBenchを提案する。
属性抽出から論理的誤り訂正まで,様々な機能を体系的に評価する。
これらの結果はGeoBenchを総合的なベンチマークとして確立し、幾何学的問題解決システムを開発するための実用的なガイドラインを提供する。
論文 参考訳（メタデータ） (2025-12-30T09:56:37Z) - Learning the Boundary of Solvability: Aligning LLMs to Detect Unsolvable Problems [51.62477754641947]
本研究では,実現可能な問題を解き,固有の矛盾を検知し,能力を超えたタスクを慎重に拒否するUnsolvableQAとUnsolvableRLを提案する。
具体的には、双トラック手法を用いて導出される、ペアで解決可能かつ解決不可能なインスタンスのデータセットであるUnsolvableQAを構築する。
このデータセット上に構築されたUnsolvableRLは,精度,未解決性,難易度を考慮した3つの報酬成分を備えた強化学習フレームワークである。
論文 参考訳（メタデータ） (2025-12-01T13:32:59Z) - AInstein: Assessing the Feasibility of AI-Generated Approaches to Research Problems [28.38783951577184]
AInsteinは、AI研究問題に対する有効なソリューションを、大規模言語モデルが生成できるかどうかをテストするためのフレームワークである。
受け入れ層により層状化された1,214 ICLR紙上でのAInsteinの評価を行った。
論文 参考訳（メタデータ） (2025-10-06T22:50:41Z) - Demystifying deep search: a holistic evaluation with hint-free multi-hop questions and factorised metrics [89.1999907891494]
We present WebDetective, a benchmark of hint-free multi-hop questions with a control Wikipedia sandbox。
25の最先端モデルに対する我々の評価は、すべてのアーキテクチャにまたがる体系的な弱点を明らかにしている。
私たちはエージェントワークフローであるEvidenceLoopを開発し、ベンチマークが特定する課題を明示的にターゲットしています。
論文 参考訳（メタデータ） (2025-10-01T07:59:03Z) - Lean Meets Theoretical Computer Science: Scalable Synthesis of Theorem Proving Challenges in Formal-Informal Pairs [41.29431283264807]
本稿では、厳密な証明問題のスケーラブルな情報源として理論計算機科学(TCS)を活用することを提案する。
本稿では,2つのTCS領域に対して,チューリング機械停止動作の証明を含むベイジービーバー問題(Busy Beaver problem)と,論理と算術の推論を組み合わせた混合ブール算術問題(Mixed Boolean Arithmetic problem)を提案する。
我々のフレームワークは,並列形式 (Lean4) と非公式 (Markdown) 仕様で問題を自動生成し,検証問題を生成するスケーラブルなパイプラインを作成する。
論文 参考訳（メタデータ） (2025-08-21T14:15:40Z) - What's in a Proof? Analyzing Expert Proof-Writing Processes in F* and Verus [2.8003002159083237]
我々は,2つの言語で作業する8人の専門家から,詳細なソースコードテレメトリの収集と解析を行うユーザスタディを実施している。
その結果、専門家が証明開発プロセスで遭遇した重要な課題や証明についてどのように考えるかについて興味深い傾向とパターンが明らかになった。
我々はこれらの知見を,AI証明アシスタントのための具体的な設計指針に翻訳する。
論文 参考訳（メタデータ） (2025-08-01T22:16:30Z) - Towards Human-Level Understanding of Complex Process Engineering Schematics: A Pedagogical, Introspective Multi-Agent Framework for Open-Domain Question Answering [0.0]
化学・プロセス産業では、プロセス・フロー・ダイアグラム(PFD)とパイプ・アンド・インスツルメンテーション・ダイアグラム(P&ID)が設計、建設、保守に不可欠である。
生成型AIの最近の進歩は、ビジュアル質問回答(VQA)のプロセス図の理解と解釈の約束を示している。
本稿では,階層的かつマルチエージェントなRetrieval Augmented Generation(RAG)フレームワークを用いた,セキュアでオンプレミスなエンタープライズソリューションを提案する。
論文 参考訳（メタデータ） (2024-08-24T19:34:04Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。