論文の概要: Mathematics with large language models as provers and verifiers

• arxiv url: http://arxiv.org/abs/2510.12829v1
• Date: Sat, 11 Oct 2025 20:35:25 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-10-16 20:13:28.339317
• Title: Mathematics with large language models as provers and verifiers
• Title（参考訳）: 証明子と証明子としての大規模言語モデルを用いた数学
• Authors: Hieu Le Duc, Leo Liberti,
• Abstract要約: ChatGPT は6つの IMO 問題のうち5つを解き、[Cohen, Journal of Sequences, 2025] の 6 個の数論の3分の1を閉じる。
• 参考スコア（独自算出の注目度）: 1.1029146548022293
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: During 2024 and 2025 the discussion about the theorem-proving capabilities of large language models started reporting interesting success stories, mostly to do with difficult exercises (such as problems from the International Mathematical Olympiad), but also with conjectures [Feldman & Karbasi, arXiv:2509.18383v1] formulated for the purpose of verifying whether the artificial intelligence could prove it. In this paper we report a theorem proving feat achieved by ChatGPT by using a protocol involving different prover and verifier instances of the gpt-5 model working collaboratively. To make sure that the produced proofs do not suffer from hallucinations, the final proof is formally verified by the lean proof assistant, and the conformance of premises and conclusion of the lean code is verified by a human. Our methodology was able to solve five out of six 2025 IMO problems, and close a third of the sixty-six number theory conjectures in [Cohen, Journal of Integer Sequences, 2025].
• Abstract（参考訳）: 2024年から2025年にかけて、大言語モデルの定理証明能力に関する議論は、主に難しい運動(例えば国際数理オリンピアードの問題)に対処するために、興味深い成功談を報告し始めたが、人工知能がそれを証明できるかどうかを検証するために定式化された予想(Feldman & Karbasi, arXiv:2509.18383v1)もある。 本稿では,gpt-5モデルの異なる証明器と検証器を協調的に動作させるプロトコルを用いて,ChatGPTが達成した定理証明の成果を報告する。 生成した証明が幻覚に悩まされないことを確認するために、最終証明は、リーン証明アシスタントによって正式に検証され、リーンコードの前提及び結論の適合性は、人間によって検証される。 我々の手法は、2025 IMOの6つのうち5つを解くことができ、[Cohen, Journal of Integer Sequences, 2025] の6つの数論の3分の1を閉じることができた。

関連論文リスト

• 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)
• Enumerate-Conjecture-Prove: Formally Solving Answer-Construction Problems in Math Competitions [37.10426226729792]
  本稿では,パターン駆動型推論と形式的定理証明を統合するモジュール型ニューロシンボリック手法であるLLMe-Conjecture-Prove(ECP)フレームワークを紹介する。 本稿では,様々な数学コンペティションにおける3,431の解題問題のデータセットであるConstructiveBenchを紹介する。
  論文  参考訳（メタデータ） (2025-05-24T03:52:25Z)
• Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
  この研究は、記号的突然変異を通じて形式的な定理を構成するデータ合成のフレームワークであるAlchemyを提案する。 マドリブにおける各候補定理について、書き直しや適用に使用できるすべてのイベーシブルな定理を同定する。 その結果、マドリブの定理の数は110kから6Mへと桁違いに増加する。
  論文  参考訳（メタデータ） (2024-10-21T08:04:21Z)
• Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
  証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。 Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
  論文  参考訳（メタデータ） (2024-07-14T01:43:07Z)

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

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