論文の概要: From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier

• arxiv url: http://arxiv.org/abs/2607.07779v1
• Date: Wed, 08 Jul 2026 17:46:36 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-07-10 14:45:27.303165
• Title: From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier
• Title（参考訳）: 研究者から研究へ:研究フロンティアにおける大規模言語モデル駆動形式数学
• Abstract要約: AI4Mathシステムの次の飛躍は、事前に定義された問題解決者から研究エージェントへの決定的なシフトを必要とする。 この分野の体系的なレビューを行い、データセット、自動形式化、証明合成について紹介する。
• 参考スコア（独自算出の注目度）: 109.93387172162984
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Recent developments in AI for Mathematics (AI4Math), especially Large Language Model (LLM)-driven theorem provers, has achieved remarkable success in formal proof generation for well-defined mathematical problems through Interactive Theorem Proving (ITP) languages. However, current systems remain fundamentally limited in tackling frontier research mathematics, such as discovering new theorems or resolving open conjectures, which are often open-ended, under-specified, and involve multiple layers of abstraction. We argue that the next leap in AI4Math systems requires a decisive shift from predefined problem-solvers to research agents that can address frontier mathematical challenges with rigorous formal mathematical reasoning. In this position paper, we provide a systematic review of the field, covering datasets, auto-formalization, and proof synthesis. More importantly, we identify core limitations of existing systems in serving as mathematical research agents, examining issues across datasets, relational structure, mathematical exploration, tool ecosystem, and human-AI collaboration, outlining a strategic road-map for the future of AI4Math.
• Abstract（参考訳）: 数学のためのAI(AI4Math)、特にLarge Language Model(LLM)駆動の定理証明器は、対話的定理証明(ITP)言語を通して、よく定義された数学問題の形式的証明生成において顕著な成功を収めている。 しかしながら、現在のシステムは、新しい定理の発見や開予想の解決など、フロンティアの研究数学に取り組む際に、基本的に制限されている。 AI4Mathシステムの次の飛躍は、厳密な形式的な数学的推論によって、フロンティア数学の課題に対処できる、事前定義された問題解決者から研究エージェントへの決定的なシフトを必要とする、と我々は主張する。 本稿では,その分野の体系的なレビューを行い,データセット,自動形式化,証明合成について述べる。 さらに重要なことは、数学研究エージェントとして機能する既存のシステムの中核的な限界を特定し、データセット、関係構造、数学的探索、ツールエコシステム、AI4Mathの将来に向けた戦略的ロードマップを概説する。

関連論文リスト

• MathCoPilot: An Interactive System for Human-AI Symbiotic Paradigm of Mathematical Research [62.221184989046826]
  MathCoPilotは、数学研究のための新しいAI共生パラダイムを具現化したループシステムである。 MathCoPilotは3つのコア機能を統合する: 証明をナビゲート可能なステップに分解するインタラクティブな証明青写真、適応的な知識ベース検索とリーン統合された反復検証を備えた自動証明スキルオーケストレーション、トピック駆動の紙検索と自動形式化を検証可能なリーン知識ベースに統合する。
  論文  参考訳（メタデータ） (2026-07-16T05:22:40Z)
• MechMath Agent Team: LLM Driven Agents for Mathematical Research [17.23955320294417]
  MechMath Agent Team (MMAT) は、数学研究の全サイクルを通して共同パイロットとして機能するように設計された大規模言語モデル駆動エージェントである。 我々は、システムの責任をコントロール、実行、拡張プレーンに分離する三部構成のハーネスアーキテクチャを設計する。 我々は、数論、代数的複素性理論、微分代数、作用素代数、不等式における開問題に関するMMATを評価する。
  論文  参考訳（メタデータ） (2026-07-05T16:37:40Z)
• Artificial Intelligence for Mathematical Reasoning: An Integrated Survey of Language Models, Neuro-symbolic Systems, and Verified Discovery [3.9943798586374784]
  この調査は、この分野の進化の統一的な説明を提供する。 i)テキストや図面に対する非公式な推論、MWPの解法、マルチモーダル幾何、RLMの解法、(ii)自動形式化、戦術予測、コンパイラ誘導修理、証明探索を含む証明アシスタントの形式的推論、(iii)システム構築の提案、境界の改善、オープンな問題に対する攻撃を支援する数学的発見、(iv)CoTプロンプト、ツールの使用、プロセス報酬モデル、VLVRなど、推論およびトレーニング時のテクニック。
  論文  参考訳（メタデータ） (2026-06-07T16:50:07Z)
• Towards Autonomous Mathematics Research [48.29504087871558]
  Aletheiaは、自然言語のエンドツーエンドの解を反復的に生成し、検証し、修正する数学研究エージェントである。 具体的には、AletheiaはGemini Deep Thinkの高度なバージョンで、推論の問題に挑戦している。 我々は、オリンピアード問題から博士レベルのエクササイズまで、AI支援数学研究におけるいくつかのマイルストーンを通じて、アレクシアを実証する。
  論文  参考訳（メタデータ） (2026-02-10T18:50:15Z)
• Large Language Models for Mathematical Analysis [3.7325315394927023]
  この研究は、数学的推論における重要なギャップに対処し、信頼できるAIの進歩に寄与する。 DEMI-MathAnalysisデータセットを開発した。 また,LLMの問題解決能力を高めるためのガイドフレームワークも設計した。
  論文  参考訳（メタデータ） (2024-12-28T20:37:55Z)
• Formal Mathematical Reasoning: A New Frontier in AI [60.26950681543385]
  我々は公式な数学的推論を提唱し、AI4Mathを次のレベルに進めるには不可欠であると主張している。 既存の進捗を要約し、オープンな課題について議論し、将来の成功を測るための重要なマイルストーンを想定します。
  論文  参考訳（メタデータ） (2024-12-20T17:19:24Z)
• Data for Mathematical Copilots: Better Ways of Presenting Proofs for Machine Learning [85.635988711588]
  我々は,大規模言語モデルの能力向上には,数学的データセットの設計におけるパラダイムシフトが必要であると論じる。 1949年にG. P'olyaが導入した「動機付き証明」の概念は、より良い証明学習信号を提供するデータセットの青写真として機能する。 数学データセットに特化して設計されたアンケートでは、クリエーターにデータセットを含めるよう促します。
  論文  参考訳（メタデータ） (2024-12-19T18:55:17Z)
• math-PVS: A Large Language Model Framework to Map Scientific Publications to PVS Theories [10.416375584563728]
  本研究では,大規模言語モデル(LLM)の高度な数学的概念の定式化への適用性について検討する。 我々は、研究論文から数学的定理を抽出し、形式化する、Emphmath-PVSと呼ばれる自動過程を構想する。
  論文  参考訳（メタデータ） (2023-10-25T23:54:04Z)
• A Survey of Deep Learning for Mathematical Reasoning [71.88150173381153]
  我々は過去10年間の数学的推論とディープラーニングの交差点における重要なタスク、データセット、方法についてレビューする。 大規模ニューラルネットワークモデルの最近の進歩は、新しいベンチマークと、数学的推論にディープラーニングを使用する機会を開放している。
  論文  参考訳（メタデータ） (2022-12-20T18:46:16Z)

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

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