メニュー
暗号セクション
ケンブリッジの新興企業は、自社のシステムがアーロンソン・アンバイニス予想を3日で証明し、それを裏付けるリーン形式化を行ったと述べている
2026 年 11 月 10 日火曜日 · 14:08 EST · 3 分で読めます
AIでは
共有
設立からわずか 2 か月のスタートアップが、20 年近く研究者を悩ませてきた量子コンピューティングの疑問を解決したと発表しました。
物理的スーパーインテリジェンス (PSI) は、2026 年 11 月 6 日にアーロンソン・アンバイニス予想を証明したと発表しました。この研究では、社内の研究システムと非公開の人体モデルを併用しており、システムの稼働 3 日目に証拠が得られたと同社は述べています。
さらに衝撃的なのは、問題を提起した人の一人からの反応です。スコット・アーロンソン氏は、証拠に完全には従っていないと述べた。とにかく彼はそれを信じています。
PSIが実際に証明したこと
アーロンソン・アンバイニス予想は、量子コンピューターが実際に速度に関して古典的なコンピューターに勝てるのはいつになるのかという基本的な質問に関するものです。この計画は 2008 年頃に初めて浮上し、2014 年に正式な声明が発表されました。
数学的核心を取り除いたこの予想は、ブール立方体上のすべての有界低次多項式には影響力のある変数があると述べています。
研究結果によると、この証明により、決定問題に対するランダムなオラクルに対する指数関数的な量子的優位性が排除されます。部分的な結果は以前の問題を少しずつ解決していました。これまで完全な証拠は得られていなかった。
PSI は、その成果を 13 ページの論文および完全なリーン形式化として公開しており、どちらも物理スーパーインテリジェンス組織の下で GitHub でホストされています。
なぜリーンが力仕事をしているのか
Lean は数学用に構築されたプログラミング言語です。人間の審判員に頼ってすべてのステップを読んでチェックするのではなく、証明をコードとして書き、カーネルと呼ばれる小さな信頼できるプログラムが、各ステップが最後のステップから論理的にたどっていることを検証します。
AI、テクノロジー、そしてそれらが動く市場について、毎日 1 回のブリーフィングで説明します。
毎日。無料。暗号通貨、金融、政策にわたる 34,000 人以上の読者に加わりましょう。
私たちはあなたのプライバシーを尊重します。いつでも購読を解除してください。
ここのスケールはかなりのものです。 PSI の形式化は、公理やプレースホルダーを追加せずに、9,454 行と 648 の定理まで実行されます。
研究結果では、複数のカーネルを使用して形式化が独立して再チェックされたことも指摘されています。
アーロンソン氏が完全には理解していない事柄についても喜んで承認しようとするのは、まさにこの検証層のためです。同氏は、証明がリーンで自動的に形式化され、PSI が結果を共有した一流の研究者チームによって説明されたため、正しいと信じていると述べた。
否定的な結果とそれが役立つ理由
この発見は、より高速な量子アルゴリズムのロックを解除するものではありません。ドアが閉まります。
Turturean氏はTechCrunchに対し、実際的な観点から次のように説明した。
「これは否定的な結果であり、人々は、わかった、私たちはもうそこに目を向けていないことを知ることができました。」
結果には明らかな限界もあります。研究結果では、Shor のアルゴリズムなどの構造化された高速化には影響を及ぼさないことが示されています。この証明は、量子的利点のすべての性質ではなく、非構造化入力に対する量子的利点を制約します。
そもそもPSIって誰だよ
PSI はマサチューセッツ州ケンブリッジに拠点を置く公益法人です。 Breakthrough Energy Ventures が主導するシード資金 5,800 万ドルにより、2026 年 9 月に設立されました。
そのタイムラインは注目に値します。 9月に最初の資金調達を行った企業は、11月初旬までに約20年来の未解決の問題について結果を出した。
人間的な視点も目を引きます。 PSI はシステムの一部として非公開の人体モデルを使用しました。これは、結果の一部が外部の研究者が現在アクセスできない AI 機能から得られたことを意味します。
開示: この記事はディエゴ・アルマダ・ロペスによって編集されました。コンテンツの作成およびレビュー方法の詳細については、編集ポリシーをご覧ください。
あなたが持っているものに関するニュース
株式と仮想通貨をフォローしてください。 Pro の何百もの出版社からのニュースを読んでください。
プライバシーポリシー
