arXiv量子コンピュータニュース（2026年10月7日）

キーワード: 機械検証された証明 / Lean 4による量子アルゴリズムの形式化 / 実験アイデアの自動生成 / 量子デバイスTCAD / 重み5の二変量バイシクル符号

オープニング：2026年10月7日 — arxiv量子コンピュータ論文解説

期間限定特集「生成AIで量子計算をつくる」の9回目は、これまでの回路生成・コンパイル・復号・校正から離れ、生成AIの意外な使い道を扱う。言語モデルが未解決予想の証明を書く、暗号攻撃の資源見積もりを定理として形式化する、量子光学の実験アイデアを自分で考える、半導体量子ドットのデバイス設計を回す、という4本に、10月4日に紹介したIBM Researchの符号探索の続編を新着として加える。5本に共通する問いは、研究工程の一部を言語モデルに任せたとき、人間の責任がどこに残るかである。1本目はハーバード大学とマサチューセッツ工科大学（MIT）のチームで、人間が確認するのは形式化した命題が予想を正しく表しているかだけになる。2本目は香港科技大学（広州）とQudeLeap Researchで、定理の中に、引用元の資源見積もりが前提として入る。3本目はテュービンゲン大学とマックス・プランク光科学研究所などのAI-Mandelで、アイデアの意味づけは人間が後から行った。4本目は西安電子科技大学のzenDotで、言語モデルが操作するのは較正前の参照デバイスのモデルである。5本目は、言語モデルによる探索と無作為抽出の比較で、確定した距離を持つ候補の割合と、構造の網羅性が逆の結果になった。5本とも計算・形式検証・シミュレーションの範囲で、実機での実験は含まない。

論文1: 言語モデルが証明しLean 4が検証した量子近似最適化の予想

出典: A Machine-Verified Proof of a Quantum-Optimization Conjecture. arXiv:2606.29687 (2026).

量子近似最適化アルゴリズム（QAOA）の原論文以来10年以上未解決だった予想を、言語モデルが証明し、その証明を証明支援系Lean 4が端から端まで検証したという、生成と検証を分けた研究の進め方が明確な成果なので選んだ。著者はハーバード大学数理科学応用センターのUri Kol氏、MIT理論物理学センターのMaor Ben-Shahar氏、MIT電子工学研究所のKfir Sulimany氏とDirk Englund氏の4人で、2026年6月29日の投稿である。対象はFarhi、Goldstone、Gutmann（FGG）が挙げた「不一致の環（ring of disagrees）」で、n個のスピンを環に並べたMaxCut、すなわち周期境界の1次元反強磁性イジング模型である。FGGは、nが偶数で2p+2≤nのとき、深さpのQAOAの最適な近似比が次の値にちょうど一致すると予想した。

$$r_p^{*} = \frac{2p+1}{2p+2}$$

p=1はFGG自身が、p=2はWangらがフェルミオン解析で証明し、MbengらはJordan-Wigner変換で問題をp個の独立な運動量モードに分解して、残留エネルギーが下限1/(2p+2)を持つことを示していた。予想が成り立つことは、2p個の角度で全モードの擬スピンを同時にコスト軸へ揃えられること、つまり2p本の超越方程式が実数解を持つことと同値で、Mbengらはp=128まで数値で確認したが、存在の証明は欠けていた。

著者らは、並行研究で作った量子情報のLeanライブラリにQAOAの定義、Jordan-Wigner変換、Andersonの擬スピンによるモード分解を形式化し、残った存在命題だけを1つの定理としてClaude Fable 5に渡した。モデルは自然言語で証明計画を立て、Leanのコンパイラの応答を受けて修正し、構成を試す前にはPythonで数値確認もした。命題と定義はモデルに見せる前に固定され、モデルは一度も変えていない。得られた証明は、各モードの伝播関数をSU(2)へ持ち上げると量子信号処理（QSP）の系列になることに気づき、モードごとの残差を1つの非対角成分に帰着させるものだった。

$$\varepsilon_k = 2\,\lvert G_{21}(k)\rvert^{2}$$

これで条件は、反回文的な1つの多項式がp個の節点で零になることに変わり、ユニタリー性から規格化定数がちょうど1/(2p+2)に決まる。相補的な多項式はFejér–Rieszの定理で存在し、Haahの分解で角度へ戻せるので、最適角度の存在が構成的に示され、その自由度から2のp乗通りの最適角度が出る。この縮退はMbengらが数値で見ていたものである。著者らは、この予想に関する先行論文はどれもQSPを使っておらず、QSPの統一的整理にもQAOAは含まれないと述べる。人間が確認する必要があるのは、形式化した命題と定義が予想を正しく表しているかだけで、証明の正しさはLeanのカーネルが保証し、Mathlibと同じ古典的公理系だけでコンパイルが通った。ただし対象は自由フェルミオンに帰着する特殊な模型で、一般のQAOAでは動的リー代数がはるかに大きく、同じ手法がそのまま効くわけではない。著者らは、ほぼ同時期に同じ問題を扱った独立の研究があることも注記している。

論文2: エージェントによるショアのアルゴリズムのLean形式化とRSA-2048・P-256の資源見積もり

出典: Building Shor's Algorithm in Lean: An Agentic Formalization of Quantum Attacks on RSA-2048 and P-256. arXiv:2607.14082 (2026).

1本目が単一の予想の証明だったのに対し、こちらは暗号攻撃という応用規模の主張を、位数発見から可逆算術回路、資源見積もりまで1つの証明言語でつなごうとする形式化で、P-256の秘密鍵復元を定量的な成功確率と資源とともに機械検証した最初のLean開発だと著者らが述べているので選んだ。著者はQudeLeap Research（上海）と香港科技大学（広州）のLei Zhang氏、Yusheng Zhao氏、Hongshun Yao氏、Xin Wang氏の4人で、2026年7月15日の投稿である。進め方は「エージェント形式化」と呼ばれ、ソフトウェアのエージェントが文献を調べ、主張を数学的な義務に分解し、Leanのコードを書いて証明を修復する。人間は科学的な主張と引用元との対応を審査し、Leanのカーネルが証明を検査する。RSA-2048の側では、位数発見、因数の復元、可逆なモジュラー算術、Ekerå–Håstadの短い離散対数による経路を、P-256の側では、有限巡回群の離散対数、素体の算術、楕円曲線の点演算、スカラーの復元を形式化した。

結果の定理は、RSA-2048では成功確率2/3以上、論理量子ビット6.19×10³、Toffoliゲート8.1×10⁹、深さ6.42×10⁹、古典算術演算3.69×10⁴で因数を返す量子アルゴリズムが存在する、というものである。1回の試行の値はQuantum誌（第5巻433）の見積もりを使い、1回の失敗確率を1/2以下として3回の独立試行で失敗を1/8以下にするので、Toffoli数と深さが3倍になる。P-256では成功確率2/3以上、論理量子ビット2.33×10³、Toffoliゲート1.26×10¹¹、Toffoli深さ1.16×10¹¹で、測定後の古典処理は7演算である。既存のQbricks、Qafny、Coqによる形式化と比べると、モジュラー算術を抽象的なオラクルとして残さず回路として構成した点が違いだと著者らは整理する。一方で限界も明記されている。最終定理では、成功確率、古典演算数、量子資源の値が別々の証明書として前提に入っており、公開鍵だけを入力とする具体的な回路の実行から全項目を導くことは今後の統合課題である。引用元が「測定深さ」として報告した値を、この定理では「最大回路深さ」と呼んでいて、両者を結ぶには追加の議論が要ると著者ら自身が書いている。P-256でも、曲線の定数の性質と、一般の巡回群とP-256の部分群との対応は仮定として置かれている。資源は誤り訂正や物理量子ビットを含まない論理回路のモデルである。

論文3: 言語モデルエージェントが量子光学の実験アイデアを考え設計まで行うAI-Mandel

出典: Towards autonomous quantum physics research using LLM agents with access to intelligent tools. arXiv:2511.11752 (2025).

研究課題そのものを人間が与えず、言語モデルが着想から実験設計までを行い、そのうち2件が独立した後続論文になったという、「何を研究するか」まで生成AIに任せた例なので選んだ。著者はテュービンゲン大学の機械学習科学クラスターとマックス・プランク光科学研究所のSören Arlt氏とMario Krenn氏、イェーナ大学のXuemei Gu氏の3人で、2025年11月13日の投稿であり、今日の新着ではない。名前は量子光学の先駆者Leonard Mandelにちなむ。AI-Mandelは、OpenAIの推論モデルo4-miniを独立に動かす2つのエージェント系からなる。アイデア生成系では、研究者役のエージェントが、PyTheusの説明、arXivの量子物理論文から無作為に選んだ3本の要旨、影響の大きい未開拓方向を予測するImpact4Castの2概念を受け取って案を出し、新規性の審査役と、PyTheusで実装できるかの審査役が差し戻す。実装系のエージェントは、アイデアをPyTheusへの指示に書き換え、エラーが返れば修正する。PyTheusは、量子光学実験の具体的な構成を探索する既存のAIツールである。

187個のアイデアが生まれ、804回の実装のうち739回が成功し、187個中184個が少なくとも1回は実装された。著者らは184個を調べ、特に面白い7件を示した。論理量子ビットの量子もつれ交換を、共有もつれもベル測定も使わず、光子対の発生源の区別不能性で行う案は、1本目の後続論文になった。離れた2量子ビット間の非局所SWAPの案では、解析中に、標準とは異なる資源を使う新しい量子テレポーテーションが構成要素に含まれていることを著者らが見つけ、2本目の論文にした。このほか、光子クトリット2個の間の伝令付きSUMゲート、測定で非線形性を作る量子パーセプトロン、もつれ交換とテレポーテーションの順序を重ね合わせる超チャネルなどがある。限界も具体的である。AI-Mandel自身は、自分の解が新しいテレポーテーションの変種であることに気づけず、その意味づけは人間が行った。使えるツールはPyTheus1つで、新規性の見積もりや多様性の出し方も人間の研究者とは異なる。成果は実験設計の青写真であり、実験室での実証は含まれない。

論文4: 言語モデルを組み込んだ半導体量子デバイスの設計プラットフォーム

出典: zenDot: An LLM-integrated quantum TCAD platform for semiconductor quantum-device design and optimization automation. arXiv:2608.16048 (2026).

生成AIを量子回路ではなく、量子ビットを作る半導体デバイスの設計に使い、言語モデルが代理モデルではなく物理ソルバーそのものを操作する構成なので選んだ。著者は西安電子科技大学（杭州研究院と集積回路学部）のZeheng Wang氏、Yan Liu氏、Yue Hao氏、Genquan Han氏の4人で、2026年8月17日の投稿である。古典の半導体開発では、材料・形状・工程から電気特性までを計算でつなぐTCADが設計を支えてきたが、量子ドットでは静電計算、電荷安定図と輸送、多体状態、量子ビットのモデルが別々のコードに分かれ、パラメータを手で入れ直している、というのが著者らの問題意識である。zenDotは、材料と層、ゲート、電極を定義した1つのデバイス状態を、18個の計算部品と18個の可視化部品に共通の登録簿で渡す。デスクトップ画面、Pythonのインターフェース、組み込みの言語モデルエージェントは同じ部品を呼び出し、エージェントが提案した計算は、実行前にデバイスとの整合性を検査される。

デモはSi/SiO₂の横型二重量子ドットで、左右のドットのレバーアーム0.28941 eV/V、帯電エネルギー36.73 meVが鏡映対称性と整合し、交換エネルギー1.019 µeV、トンネル結合93.174 µeVを同じデバイス状態から得た。ここからハイブリッド量子ビット、トンネル電荷量子ビット、一重項三重項量子ビットの3つのモデルを評価した。一重項三重項量子ビットでは、ドット間の磁場差25 mTのとき、z回転の誤差は5.99×10⁻⁸でも、万能な2ゲートのうち悪い方の不忠実度が0.759になる。万能制御を目的にゼーマン勾配を走査すると1.90 mTが選ばれ、不忠実度は0.0259と約29分の1になった。ただしこの改善はプラットフォームの走査によるもので、言語モデルの成果ではない。言語モデルは3つの課題で各6回、計18回の設計反復を行い、ハイブリッド量子ビットのQ値は161412.67から220112.30へ、トンネル電荷量子ビットのQ値は225.07から809.67へ上がった。ゲート長を変えてデバイスを作り直す課題では、不忠実度は6.273816×10⁻⁸から6.272891×10⁻⁸へと、ほとんど変わらなかった。著者ら自身、これは最適化能力の比較ではなく運用形態の実証だとし、使ったのは1つのローカル言語モデルで、評価は課題ごとに6回だと書いている。参照デバイスは作製した素子への当てはめではなく内部で整合したモデルで、緩和はゲート忠実度に含まれず、材料と形状の不確かさも伝播させていない。

論文5: 言語モデル主導のプログラム進化による重み5の二変量バイシクル符号の探索

出典: Large Language Model-Guided Discovery of Weight-Five Bivariate Bicycle Codes. arXiv:2610.06623 (2026).

10月4日に紹介したIBM Researchの重み6の符号探索の続編で、今回は同じ層の割り当てで無作為に抽出する対照実験を3回置き、言語モデルの探索が何に効き何に効かないかを数値で示した新着なので選んだ。著者はIBM ResearchのJuan Cruz-Benito氏の単著で、2026年10月5日の投稿である。重み6のBB符号は2つの三項式で作るが、今回は二項式と三項式の組み合わせ（2+3）で、スタビライザーの重みもデータ量子ビットの次数も5になる、より制約の強い族を扱う。OpenEvolveで300反復のキャンペーンを4本走らせ、多項式の組を出力するPython関数をClaude Opus 5とGPT-5.6 Solのアンサンブルに変異させた。CSS型では性能指数kd²/nを、非CSS型の摂動BB（PBB）では距離5以上を目的にし、距離はBP–OSDで順位づけした後、上位をMILPや網羅探索で厳密に確定した。CSS型の距離評価に使った6つの格子だけで、正規化した二項式と三項式の組は13,656,867通りある。

目録には1,142個の符号案が入り、うち1,081個が言語モデル生成のプログラムに由来する。連結な最良のCSS符号は[[96,4,10]]、[[140,6,10]]、[[180,4,14]]で、性能指数は4.17、4.29、4.356である。ただし[[96,4,10]]は、探索後の照合で、LinとPryadkoが網羅列挙したアーカイブの位数48の巡回群上の構成と等価だった。重み5で確定した性能指数の最大は、同じアーカイブにある非可換群C₁₁×S₃上の[[132,4,12]]の4.364で、今回の発見をわずかに上回る。また、1,142個中409個は非連結、つまり小さな符号の重ね合わせであり、確定距離を持つクラスの73.1%が同じ連結成分の繰り返しを含んでいた。対照実験では、正の距離が記録されたCSS案936個のうち816個（87.18%）が距離5以上と確定したのに対し、同じ格子と次元帯の配分で6,444個を重複なく無作為に抽出した3回の対照では72.50〜74.26%だった。一方、無作為抽出の方がより多くの連結クラスを覆い、3回とも[[180,4,14]]のクラスを引き当てた。著者自身、キャンペーン側の分母は正の距離が記録された観測だけで、失敗や距離0の呼び出しは含まれないため、試行あたりの収率や総計算量の比較にはならないと限界に書いている。評価は符号のパラメータと連結性、理想的な相互作用の順序までで、シンドローム抽出回路、回路レベルの雑音、論理誤り率は次の段階とされる。

まとめ

今日の5本は、量子計算の研究工程の上流と周辺に生成AIを置き、人間の責任がどこに残るかで分かれた。FGG予想の証明では、言語モデルが量子信号処理という別分野の道具を持ち込み、10年以上の空白を埋めたが、人間の確認は命題の形式化が正しいかの一点に縮まった。ショアのアルゴリズムの形式化では、可逆算術まで回路として構成した一方、最終定理の資源値は引用元の見積もりを前提として受け取っている。AI-Mandelは187個のアイデアから2本の後続論文を生んだが、新しいテレポーテーションに気づいたのは人間だった。zenDotでは、言語モデルが物理ソルバーを直接操作できることを示したが、大きな改善はプラットフォームの走査によるもので、モデルの設計反復による改善は小さい。重み5の符号探索では、言語モデルは距離の高い候補の割合を上げたが、構造の網羅では無作為抽出が勝った。5本とも、実機での実証と回路レベルの評価はまだ含まれない。

参考ソース

• 論文1: A Machine-Verified Proof of a Quantum-Optimization Conjecture. arXiv:2606.29687
• 論文2: Building Shor's Algorithm in Lean: An Agentic Formalization of Quantum Attacks on RSA-2048 and P-256. arXiv:2607.14082
• 論文3: Towards autonomous quantum physics research using LLM agents with access to intelligent tools. arXiv:2511.11752
• 論文4: zenDot: An LLM-integrated quantum TCAD platform for semiconductor quantum-device design and optimization automation. arXiv:2608.16048
• 論文5: Large Language Model-Guided Discovery of Weight-Five Bivariate Bicycle Codes. arXiv:2610.06623