論文の概要: Advancing Mathematics Research with AI-Driven Formal Proof Search

• arxiv url: http://arxiv.org/abs/2605.22763v1
• Date: Thu, 21 May 2026 17:24:57 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-05-22 16:35:42.374098
• Title: Advancing Mathematics Research with AI-Driven Formal Proof Search
• Title（参考訳）: AIによる形式証明探索による数学研究の促進
• Authors: George Tsoukalas, Anton Kovsharov, Sergey Shirobokov, Anja Surina, Moritz Firsching, Gergely Bérczi, Francisco J. R. Ruiz, Arun Suggala, Adam Zsolt Wagner, Eric Wieser, Lei Yu, Aja Huang, Miklós Z. Horváth, Andrew Ferrauiolo, Henryk Michalewski, Codrut Grosu, Thomas Hubert, Matej Balog, Pushmeet Kohli, Swarat Chaudhuri,
• Abstract要約: 大規模言語モデル (LLMs) は、数学的な推論においてますます優れているが、その信頼性の欠如は数学研究における実用性を制限している。 緩和はLLMを使ってリーンのような言語で公式な証明を生成します。 オープンな問題を解くための,本手法の大規模評価を行う。
• 参考スコア（独自算出の注目度）: 20.297700405590156
• License: http://creativecommons.org/licenses/by-nc-nd/4.0/
• Abstract: Large language models (LLMs) increasingly excel at mathematical reasoning, but their unreliability limits their utility in mathematics research. A mitigation is using LLMs to generate formal proofs in languages like Lean. We perform the first large-scale evaluation of this method's ability to solve open problems. Our most capable agent autonomously resolved 9 of 353 open Erdős problems at the per-problem cost of a few hundred dollars, proved 44/492 OEIS conjectures, and is being deployed in combinatorics, optimization, graph theory, algebraic geometry, and quantum optics research. A basic agent alternating LLM-based generation with Lean-based verification replicated the Erdős successes but proved costlier on the hardest problems. These findings demonstrate the power of AI-aided formal proof search and shed light on the agent designs that enable it.
• Abstract（参考訳）: 大規模言語モデル (LLMs) は、数学的な推論においてますます優れているが、その信頼性の欠如は数学研究における実用性を制限している。 緩和はLLMを使ってリーンのような言語で公式な証明を生成します。 オープンな問題を解くための,本手法の大規模評価を行う。 我々の最も有能なエージェントは、数百ドル当たりのコストで353のうち9つを自力で解決し、44/492 OEIS予想を証明し、組合せ論、最適化、グラフ理論、代数幾何学、量子光学の研究に展開している。 LLMベースの生成とリーンベースの検証を交互に行う基本的なエージェントは、エルデシュの成功を再現したが、最も難しい問題に対してコストがかかることを証明した。 これらの知見は、AI支援による正式な証明探索の力を示し、それを可能にするエージェント設計に光を当てた。

関連論文リスト

• O-Forge: An LLM + Computer Algebra Framework for Asymptotic Analysis [5.6900369690933195]
  大規模言語モデルは、最近、IMOとPutnamの問題を解決する高度な能力を実証した。 主な困難は検証である: 提案は妥当に見えるが、厳密なチェックなしには信頼できない。 コンピュータ代数システムとフロンティア LLM を結合する LLM+CAS というフレームワークを提案する。
  論文  参考訳（メタデータ） (2025-10-14T10:07:53Z)
• Prover Agent: An Agent-Based Framework for Formal Mathematical Proofs [11.87831709160905]
  本稿では,自動定理証明のためのAIエージェントであるProver Agentを紹介する。 大規模な言語モデル(LLM)と公式な証明アシスタントであるLeanを統合している。 MiniF2Fベンチマークで88.1%の成功率を達成した。
  論文  参考訳（メタデータ） (2025-06-24T18:01:52Z)
• Enumerate-Conjecture-Prove: Formally Solving Answer-Construction Problems in Math Competitions [39.102692814217086]
  LLMは難解な解答作業に対処できるが、幻覚や不可解なステップの誤りを生じやすい。 創造性と数学的厳密性の両方を保ちながら、どのように解答-構成問題を解決するか? 本稿では,パターン駆動型推論と形式的定理証明を統合したニューロシンボリックな手法であるLLM-Conjecture-Prove(ECP)フレームワークを紹介する。 ConstructiveBenchでは、ECPは33.1%の最先端の精度(32.5%から)を達成し、公式な数学的推論を前進させる可能性を示している。
  論文  参考訳（メタデータ） (2025-05-24T03:52:25Z)
• One Example Shown, Many Concepts Known! Counterexample-Driven Conceptual Reasoning in Mathematical LLMs [75.95179490687018]
  証明生成のための数学的大規模言語モデルを活用することは、LLM研究の基本的なトピックである。 現状のLCMが証明できる能力は、学習中に関連する証明プロセスに遭遇したかどうかに大きく依存していると論じる。 人間の数学教育で一般的に用いられる「反例による防御」の教育的手法に触発されて,我々の研究は,反例を通して数学的推論と証明を行うLLMの能力を高めることを目的としている。
  論文  参考訳（メタデータ） (2025-02-12T02:01:10Z)
• LeanAgent: Lifelong Learning for Formal Theorem Proving [85.39415834798385]
  フォーマルな定理証明のための新しい生涯学習フレームワークであるLeanAgentを紹介する。 LeanAgentは継続的に一般化し、拡張可能な数学的知識を改善します。 これは23のリーンリポジトリにわたる155の定理の正式な証明を生成する。
  論文  参考訳（メタデータ） (2024-10-08T17:11:24Z)
• Can LLMs Master Math? Investigating Large Language Models on Math Stack Exchange [25.419977967846144]
  大規模言語モデル(LLM)は、様々な自然言語タスクにおいて例外的な機能を示した。 本稿では、複雑な数学的問題解決をナビゲートする上でのLLMの限界について考察する。
  論文  参考訳（メタデータ） (2024-03-30T12:48:31Z)

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

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