論文の概要: Auditing an AI-Generated Mathematical Proof: A Correction to a Greedy Conditioning Lemma in Quantum Parallel Repetition
- arxiv url: http://arxiv.org/abs/2608.14673v1
- Date: Mon, 03 Aug 2026 15:12:46 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-08-23 14:54:39.956674
- Title: Auditing an AI-Generated Mathematical Proof: A Correction to a Greedy Conditioning Lemma in Quantum Parallel Repetition
- Title（参考訳）: AIによる数学的証明の検証:量子並列反復におけるグレディコンディショニング・レムマの補正
- Abstract要約: このメモは明示的な反例を与え、意図された継続条件を特定し、完全な正当性証明を提供する。
しかし、これは主並列反復定理の独立な検証として解釈されるべきではない。
- 参考スコア（独自算出の注目度）: 0.0
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Chapter 6 of OpenAI's *Ten Advances in Mathematics and Theoretical Computer Science* claims an exponential parallel-repetition theorem for all finite two-player, one-round entangled games. Early in the proof, the chapter uses a quantitative greedy conditioning lemma. The lemma is meant to select a small set of coordinates (D) such that, after conditioning on winning every coordinate in (D), a randomly chosen remaining coordinate is won with average probability at least (1-δ). The statement is correct, but the proof as printed contains a polarity error. Its continuation test is written in terms of average success, while the next step requires a coordinate with a large conditional failure probability. That implication is false, and even simple examples can leave the printed procedure without a valid next move. This note gives an explicit counterexample, identifies the intended continuation condition, and supplies a complete corrected proof. The repair is local: it leaves the statement of the lemma and the parameters used later in the chapter unchanged. It should not, however, be read as an independent verification of the main parallel-repetition theorem. More broadly, the example shows how a mathematically plausible AI-generated argument can hide a small but decisive reversal between complementary events.
- Abstract（参考訳）: OpenAIの *10 Advances in Mathematics and Theory Computer Science* の第6章では、有限個の2つのプレイヤーと1ラウンドの絡み合ったゲームに対して指数関数的並列反復定理が主張されている。
証明の初期段階では、この章は量的欲求条件の補題を用いている。
補題は、(D)における各座標の勝利を条件づけた後に、ランダムに選択された残余座標が、平均確率(1-δ)で獲得されるような、小さな座標群(D)を選択することを意図している。
主張は正しいが、印刷された証明には極性誤差が含まれている。
その継続テストは平均的な成功の観点から書かれており、次のステップでは大きな条件付き故障確率の座標を必要とする。
この意味は偽りであり、単純な例でさえ、有効な次の動きなしに印刷された手続きを残せる。
このメモは明示的な反例を与え、意図された継続条件を特定し、完全な正当性証明を提供する。
修復は局所的であり、補題の文言と章で後に使われるパラメータはそのまま残されている。
しかし、これは主並列反復定理の独立な検証として解釈されるべきではない。
より広い範囲で、この例は、数学的に証明可能なAI生成の議論が、補完的な出来事の間の小さなが決定的な逆転を隠すことができることを示している。
関連論文リスト
- Trust the Spec, Not the Code - A Specification-First, AI-Assisted Case Study in Online Banking [1.6796354350132203]
形式的な仕様は、早期エラー検出、明示的な不変性、設計による正しさを約束するが、その表記コストは主流の実践から遠ざかっている。
AIは推論と証明に十分な精度の中間仕様言語として機能する、と我々は主張する。
仕様は、著者、レビュー、証明、洗練の成果物となり、コードは再生可能な出力になる。
論文 参考訳（メタデータ） (2026-09-07T11:35:49Z) - The Condition-Number Barrier in Sparse Least Squares [77.64108812086542]
AxiotisとSviridenkoは[AS21]において、凸最適化における制限条件数への線形依存はスパース時間アルゴリズムでは改善できないと推測した。
我々は、最小二乗目的に対する予想下界を確立し、ランダム化された完全体積小セット展開仮説に基づく条件付けを行う。
論文 参考訳（メタデータ） (2026-08-03T17:57:01Z) - The Time-Space Complexity of Checking Multiple Assertions in Quantum Programs [0.5524804393257919]
複数のアサーションを含む量子プログラムをチェックするには、しばしば追加の空間を使用するか、プログラムを追加の時間で実行する必要がある。
n$のアサーションを持つプログラムの場合、単純な戦略は$n$のアシラを使ってすべての$n$の結果を学習する。
代替手段は1つのアンシラを使用するが、$n$ラウンドでプログラムの実行を繰り返し、ラウンド毎に1つのアサーションをチェックする。
論文 参考訳（メタデータ） (2026-07-13T15:09:04Z) - Ten Digits on a Train: AI-Assisted Verification of Two Eigenvalue Problems [0.0]
本稿では、そのような2つの計算に関する人間-AIコラボレーションについて報告する。
特異な自己随伴シュルディンガー作用素に対して、証明された零数とディリクレ=ノイマンブラケットは、完全な負スペクトルを10個の十進点に証明する。
微妙な非正規原子分子ベンチマークでは、以前は未解決の共鳴対が分離され、各部材は10桁に囲まれている。
論文 参考訳（メタデータ） (2026-06-22T18:03:59Z) - LeanMarathon: Toward Reliable AI Co-Mathematicians through Long-Horizon Lean Autoformalization [104.06650149974585]
信頼性の高い研究レベルのLean AutoformalizationのためのマルチエージェントハーネスであるLeanMarathonを紹介します。
4つのコントラクトスコープエージェントがこの青写真を構築し、監査し、証明し、修復する。
我々は4つのErds問題にまたがる最近の2つの研究論文でLeanMarathonを評価した。
論文 参考訳（メタデータ） (2026-06-03T20:09:39Z) - Yanasse: Finding New Proofs from Deep Vision's Analogies, Part 1 [51.56484100374058]
システムはマドリブの27の上位領域の戦術的利用分布を抽出する。
zスコアを計算して、ソースエリアで多用されるが、ターゲットエリアで稀または欠落している戦術を特定する。
これは、GPUアクセラレーションされたNPハードアナログを用いて、ソースとターゲットの証明状態と一致する。
論文 参考訳（メタデータ） (2026-04-19T03:27:16Z) - A Constructive Proof of Rice's Theorem and the Halting Problem via Hilbert's Tenth Problem [0.0]
ライスの定理は、プログラムの非自明な意味的性質は決定不可能である。
Hilbert's Tenth Problem (MRDP) の不決定性に対する構成的証明を提案する。
議論は2つの別個の含意として構成され、可解性に関する解離を主張せず、P(bot)を検査しない。
論文 参考訳（メタデータ） (2026-04-11T20:45:58Z) - The Aldous--Lyons Conjecture II: Undecidability [3.8370118222043694]
調整された非局所ゲームである$G$が与えられた場合、$G$が特別な種類の完全戦略を持つ場合と、$G$のすべての戦略が完璧ではない場合とを区別することは決定不可能である。
共役紙 [BCLV24] に導入された還元を用いて、この不決定性の結果はアルドゥス=リヨン予想に対する負の答えを意味する。
論文 参考訳（メタデータ） (2024-12-30T22:59:56Z) - Some consequences of Sica's approach to Bell's inequalities [55.2480439325792]
ルイ・シカ(Louis Sica)は、ベルの不等式は、あるステーションで観測された結果の時系列が、他のステーションの設定が変更されても変化しないという仮説から導いた。
本稿では,Sicaのアプローチを非理想的効率と実時間構造に拡張する。
論文 参考訳（メタデータ） (2024-03-05T13:59:52Z) - Global Nash Equilibrium in Non-convex Multi-player Game: Theory and
Algorithms [66.8634598612777]
ナッシュ均衡(NE)はマルチプレイヤーゲームにおいて全てのプレイヤーに受け入れられることを示す。
また、一般理論から一歩ずつ一方的に利益を得ることはできないことも示している。
論文 参考訳（メタデータ） (2023-01-19T11:36:50Z) - Connes implies Tsirelson: a simple proof [91.3755431537592]
コンヌ埋め込み問題は同期的ツィレルソン予想を意味することを示す。
また、コンネスの代数 $mathcalRomega$ の異なる構成もコンネス埋め込み問題に現れる。
論文 参考訳（メタデータ） (2022-09-16T13:59:42Z) - multiPRover: Generating Multiple Proofs for Improved Interpretability in
Rule Reasoning [73.09791959325204]
我々は、自然言語の事実と規則の形で明示的な知識を推論することを目的としている言語形式推論の一種に焦点を当てる。
PRoverという名前の最近の研究は、質問に答え、答えを説明する証明グラフを生成することによって、そのような推論を行う。
本研究では,自然言語規則ベースの推論のために複数の証明グラフを生成するという,新たな課題に対処する。
論文 参考訳（メタデータ） (2021-06-02T17:58:35Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。