論文の概要: Autonomous disproofs of the sum-product conjecture over $\mathbb R$ with GPT-5.5 Pro

• arxiv url: http://arxiv.org/abs/2607.20525v1
• Date: Thu, 09 Jul 2026 23:28:37 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-07-27 00:46:13.217555
• Title: Autonomous disproofs of the sum-product conjecture over $\mathbb R$ with GPT-5.5 Pro
• Title（参考訳）: GPT-5.5 Proによる$\mathbb R$上の総積予想の自律的解法
• Abstract要約: GPT-5.5 Pro 上に構築した問題に依存しない3段プロンプトパイプラインを提案する。 エージェントが自律的に生成した正しい証明は、和積予想が8つの独立トライアルのうち7つのアーケードの$mathbb R$に対して偽であることを示している。
• 参考スコア（独自算出の注目度）: 5.634825161148485
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: OpenAI's recent disproof of the Erdős unit distance conjecture marked a milestone for AI in mathematics. It also inspired another breakthrough: a human disproof of the Erdős--Szemerédi sum-product conjecture over $\mathbb R$. In this paper, we present a simple agent built on GPT-5.5 Pro. Using a problem-agnostic, three-stage prompting pipeline -- proof-plan proposal, proof construction, and review -- the agent autonomously generated correct proofs that the sum-product conjecture is false over $\mathbb R$ in 7 of 8 independent trials; in the remaining trial, it identified an unresolved gap in its argument. The seven proofs are diverse: some are close to existing unit-based constructions, while others avoid units by using $L^p$-type regions of algebraic integers. The system used an average of 132.4k reasoning tokens per trial. We release the code, intermediate outputs, and generated proofs, providing a reproducible, data-contamination-free case study in autonomous proof generation.
• Abstract（参考訳）: OpenAIの最近のエルデシュ単位距離予想の反抗は、数学におけるAIのマイルストーンとなった。 エルデシュ=ゼメレーディの総和積予想が$\mathbb R$を上回り、人間の反抗がもたらされた。 本稿では, GPT-5.5 Pro 上に構築した簡易エージェントについて述べる。 問題に依存しない3段階のプロンプトパイプライン -- 証明計画の提案、証明構築、そしてレビュー -- を用いて、エージェントは自律的に、和積予想が8つの独立した試験のうち7ドルの$\mathbb R$に対して偽であることを示す正しい証明を作成した。 7つの証明は多様であり、いくつかは既存の単位ベース構成に近いが、他の証明は代数整数の$L^p$型領域を使用することで単位を避ける。 このシステムは1回の試験で平均132.4kの推論トークンを使用した。 我々は、コード、中間出力、および生成された証明を公開し、自律的証明生成における再現可能な、データ汚染のないケーススタディを提供する。

関連論文リスト

• The Condition-Number Barrier in Sparse Least Squares [77.64108812086542]
  AxiotisとSviridenkoは[AS21]において、凸最適化における制限条件数への線形依存はスパース時間アルゴリズムでは改善できないと推測した。 我々は、最小二乗目的に対する予想下界を確立し、ランダム化された完全体積小セット展開仮説に基づく条件付けを行う。
  論文  参考訳（メタデータ） (2026-08-03T17:57:01Z)
• Geometric Measurements of the Axiom of Choice in Neural Proof Embeddings [0.2538209532048866]
  我々はLean 4のカーネルレベルの公理依存性の追跡を用いて、選択の公理が証明空間に測定可能な幾何学的相関を持つことを示す。 このシグネチャは長さ,ファイル,著者,トピックコントロールに留まり,正規化証明源で訓練されたフルソースエンコーダの下で複製されることを示す。
  論文  参考訳（メタデータ） (2026-06-26T19:57:00Z)
• Mathematics with large language models as provers and verifiers [1.1029146548022293]
  ChatGPT は6つの IMO 問題のうち5つを解き、[Cohen, Journal of Sequences, 2025] の 6 個の数理論の予想の約3分の1を閉じる。
  論文  参考訳（メタデータ） (2025-10-11T20:35:25Z)
• Gödel Test: Can Large Language Models Solve Easy Conjectures? [40.906606632144694]
  我々はG"odel Test"を提案し、モデルが非常に単純で未解決な予想に対して正しい証明を生成できるかどうかを評価する。 アルゴリズム最適化における 5 つの予想に対する GPT-5 の性能について検討する。 GPT-5は、最終的にG"odel Test"を通過させるフロンティアモデルに向けた初期のステップを表す可能性がある。
  論文  参考訳（メタデータ） (2025-09-22T20:11:40Z)
• Safe: Enhancing Mathematical Reasoning in Large Language Models via Retrospective Step-aware Formal Verification [56.218970738892764]
  Chain-of-Thoughtプロンプトは、大規模言語モデル(LLM)から推論能力を引き出すデファクトメソッドとなっている。 検出が極めて難しいCoTの幻覚を緩和するために、現在の方法は不透明なボックスとして機能し、彼らの判断に対する確認可能な証拠を提供しておらず、おそらくその効果を制限する。 任意のスコアを割り当てるのではなく、各推論ステップで形式数学言語Lean 4で数学的主張を明確にし、幻覚を識別するための公式な証明を提供しようとしている。
  論文  参考訳（メタデータ） (2025-06-05T03:16:08Z)
• 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)
• Post-quantum encryption algorithms of high-degree 3-variable polynomial congruences: BS cryptosystems and BS key generation [0.0]
  本稿では,3変数のBeal-Schurコングルースに基づく量子後暗号アルゴリズムを構築する。 この結果を用いて、単純でセキュアな量子後暗号アルゴリズムを生成する。
  論文  参考訳（メタデータ） (2024-08-14T14:19:46Z)
• MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
  MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。 5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。 我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
  論文  参考訳（メタデータ） (2024-02-14T05:57:58Z)
• Partial Proof of a Conjecture with Implications for Spectral Majorization [0.43512163406551996]
  我々は、$ntimes n$, $nleq 6$, positive definite matrices の性質に関する予想に関する新しい結果を示す。 我々は、コンピュータ支援とAIに基づく証明の将来について、一般的な考察で結論付けている。
  論文  参考訳（メタデータ） (2023-09-04T01:02:19Z)
• NaturalProver: Grounded Mathematical Proof Generation with Language Models [84.2064569475095]
  自然数理言語における定理証明は、数学の進歩と教育において中心的な役割を果たす。 本研究では,背景参照を条件づけて証明を生成する言語モデルであるNaturalProverを開発する。 NaturalProverは、短い(2-6ステップ)証明を必要とするいくつかの定理を証明でき、40%の時間で正しいと評価された次のステップの提案を提供することができる。
  論文  参考訳（メタデータ） (2022-05-25T17:01:18Z)
• Generating Natural Language Proofs with Verifier-Guided Search [74.9614610172561]
  NLProofS (Natural Language Proof Search) を提案する。 NLProofSは仮説に基づいて関連するステップを生成することを学習する。 EntailmentBank と RuleTaker の最先端のパフォーマンスを実現している。
  論文  参考訳（メタデータ） (2022-05-25T02:22:30Z)
• multiPRover: Generating Multiple Proofs for Improved Interpretability in Rule Reasoning [73.09791959325204]
  我々は、自然言語の事実と規則の形で明示的な知識を推論することを目的としている言語形式推論の一種に焦点を当てる。 PRoverという名前の最近の研究は、質問に答え、答えを説明する証明グラフを生成することによって、そのような推論を行う。 本研究では,自然言語規則ベースの推論のために複数の証明グラフを生成するという,新たな課題に対処する。
  論文  参考訳（メタデータ） (2021-06-02T17:58:35Z)

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

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