論文の概要: Gödel Test: Can Large Language Models Solve Easy Conjectures?

• arxiv url: http://arxiv.org/abs/2509.18383v1
• Date: Mon, 22 Sep 2025 20:11:40 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-09-24 20:41:27.562785
• Title: Gödel Test: Can Large Language Models Solve Easy Conjectures?
• Title（参考訳）: Gödelテスト: 大規模言語モデルは容易に導出できるか?
• Authors: Moran Feldman, Amin Karbasi,
• Abstract要約: 我々はG"odel Test"を提案し、モデルが非常に単純で未解決な予想に対して正しい証明を生成できるかどうかを評価する。 アルゴリズム最適化における 5 つの予想に対する GPT-5 の性能について検討する。 GPT-5は、最終的にG"odel Test"を通過させるフロンティアモデルに向けた初期のステップを表す可能性がある。
• 参考スコア（独自算出の注目度）: 40.906606632144694
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Recent announcements from frontier AI model labs have highlighted strong results on high-school and undergraduate math competitions. Yet it remains unclear whether large language models can solve new, simple conjectures in more advanced areas of mathematics. We propose the G\"odel Test: evaluating whether a model can produce correct proofs for very simple, previously unsolved conjectures. To this end, we study the performance of GPT-5 on five conjectures in combinatorial optimization. For each problem, we provided one or two source papers from which the conjecture arose, withheld our own conjecture, and then assessed the model's reasoning in detail. On the three easier problems, GPT-5 produced nearly correct solutions; for Problem 2 it even derived a different approximation guarantee that, upon checking, refuted our conjecture while providing a valid solution. The model failed on Problem 4, which required combining results from two papers. On Problem 5, a harder case without a validated conjecture, GPT-5 proposed the same algorithm we had in mind but failed in the analysis, suggesting the proof is more challenging than expected. Although our sample is small, the results point to meaningful progress on routine reasoning, occasional flashes of originality, and clear limitations when cross-paper synthesis is required. GPT-5 may represent an early step toward frontier models eventually passing the G\"odel Test.
• Abstract（参考訳）: 最近のフロンティアAIモデルラボの発表は、高校と学部の数学コンペティションにおける強力な結果を浮き彫りにした。 しかし、より高度な数学領域において、大きな言語モデルが新しい単純な予想を解くことができるかどうかは不明である。 我々はG\"odel Test"を提案し、モデルが非常に単純で未解決な予想に対して正しい証明を生成できるかどうかを評価する。 そこで本研究では,組合せ最適化における5つの予想に対する GPT-5 の性能について検討する。 それぞれの問題に対して、予想が生じた1つか2つの元となる論文を提出し、それ自身の予想を裏付け、そのモデルの推論を詳細に評価した。 GPT-5は、より簡単な3つの問題に対して、ほぼ正しい解を生み出した。 モデルは問題4で失敗し、2つの論文の結果の組み合わせが必要になった。 検証された予想のない難しいケースであるイシュー5では、GPT-5は我々が念頭に置いていたのと同じアルゴリズムを提案したが、解析に失敗し、証明は予想よりも難しいことを示唆した。 サンプルは小さいが,本研究の結果は,定期的な推論,創発性のフラッシュ,紙間合成が必要な場合の明確な制限について有意義な進展を示唆している。 GPT-5は、最終的にG\"odel Test"をパスするフロンティアモデルに向けた初期のステップを表すかもしれない。

関連論文リスト

• Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving [36.20164235042574]
  本研究では,レムマ型全耐久推論モデルである textbfSeed-Prover を提案する。 IMOレベルの競合問題を解決するために、深い推論と広い推論の両方を可能にする3つのテストタイム推論戦略を設計する。 シード・プロバーは、過去のIMO問題の78.1%ドルを証明し、ミニF2Fを飽和させ、パットナムベンチで50%以上を達成し、それまでの最先端よりも大きな差を付けた。
  論文  参考訳（メタデータ） (2025-07-31T17:00:30Z)
• Towards Solving More Challenging IMO Problems via Decoupled Reasoning and Proving [48.22540519786074]
  最近の研究では、非公式な精度は80%を超え、公式な成功はPutnamBenchのようなベンチマークで8%以下である。 低レベルの証明生成から高レベルの推論を分離する新しいフレームワークを提案する。 提案手法は,2000年以降のIMO問題に対して,従来のオープンソース証明者が未報告の課題として評価した。
  論文  参考訳（メタデータ） (2025-07-07T22:38:49Z)
• Solving Inequality Proofs with Large Language Models [46.71658812761115]
  不等式証明は様々な科学・数学分野において不可欠である。 これにより、大きな言語モデル(LLM)の需要が高まるフロンティアとなる。 我々は、Olympiadレベルの不平等を専門家が計算したデータセットであるIneqMathをリリースした。
  論文  参考訳（メタデータ） (2025-06-09T16:43:38Z)
• Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving [72.8626512877667]
  我々は,2025年4月5日現在,数学問題の自動証明生成における最先端(最先端)性能を実現する,オープンソースの言語モデルであるGoedel-Proverを紹介した。 まず、自然言語の数学問題をNuminaデータセットからLean 4で等価な形式ステートメントに変換するためにLLMをトレーニングします。 次に,一連のプロデューサをトレーニングすることで,形式証明の大規模なデータセットを開発する。 最後に、Goedel-Pset-v1-solvedというデータセットを取得し、Goedel-Pset-v1から800K以上のステートメントの証明を含む。
  論文  参考訳（メタデータ） (2025-02-11T15:27:35Z)
• MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
  MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。 5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。 我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
  論文  参考訳（メタデータ） (2024-02-14T05:57:58Z)
• Large Language Models' Understanding of Math: Source Criticism and Extrapolation [0.0]
  GPT-4モデルの数学的理解を評価する。 GPT-4が基本的な数学的概念さえも理解したことを示す科学的証拠を見つけることは困難である。
  論文  参考訳（メタデータ） (2023-11-12T07:52:32Z)
• PRover: Proof Generation for Interpretable Reasoning over Rules [81.40404921232192]
  本稿では,ルールベース上の二項質問に応答し,対応する証明を生成するトランスフォーマーモデルを提案する。 本モデルは,効率的な制約付き学習パラダイムを用いて,証明グラフに対応するノードやエッジを予測できることを学習する。 我々は、QAと証明生成のための有望な結果を示すために、合成、手書き、人文による規則ベースの実験を行う。
  論文  参考訳（メタデータ） (2020-10-06T15:47:53Z)

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

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