艾倫森相信 AI 證明正確：Shor 演算法不受影響

艾倫森（Scott Aaronson）表示，他相信人工智慧（AI）研究系統產生的證明是正確的，但自己還沒有完全理解整份證明。艾倫森是艾倫森－安拜尼斯猜想的共同提出者。

艾倫森8日在個人部落格寫道：「我相信這份證明是正確的。」他表示，信心來自 Lean 證書對證明各步驟的檢查，以及研究人員對內容的審視。

AI研究公司 Physical Superintelligence（PSI）6日宣布，其研究系統運用未公開的 Anthropic 模型完成證明。系統在執行的第三天完成整份證明，PSI並表示，之後兩度改進下界。本報先前曾報導PSI公布艾倫森－安拜尼斯猜想證明。

模型的具體名稱尚未公開。艾倫森表示，他不清楚AI研究系統和其中使用的模型各自對證明有多少貢獻。

艾倫森－安拜尼斯猜想比較在沒有特殊規則的隨機輸入下，量子演算法與一般演算法所需的輸入查詢次數。這項研究探討的是：一般演算法能否用較少的查詢，近似量子演算法回答「是」或「否」的機率。

問題開始受到研究的時間，與論文公開的時間應分開看。PSI將這項猜想描述為自2008年起未解的問題；艾倫森與安德里斯・安拜尼斯（Andris Ambainis）的原始論文則於2009年11月5日首次刊登在 arXiv。

PSI的研究說明提出一項定理：若一個次數為 d 的有界多項式，其變異數至少為 ε，便至少有一個影響力較大的變數。該變數影響力的下界為 (8√15/(125π⁴))·ε^(5/2)/d⁶；研究也提出較簡化的下界 (ε/d)^7。

此處的變數影響力，指改變一個輸入位元後，多項式輸出會變動多少。這項定理探討的是特定輸入與查詢複雜度條件，並非判斷量子電腦在所有計算中是否都比一般電腦快。

Lean是一種工具，可將數學命題與證明寫成形式語言，再由電腦檢查是否符合邏輯規則。PSI的公開儲存庫說明，Lean已檢查形式化後的命題與證明。

不過，儲存庫也指出，讀者仍須自行比對形式化命題是否準確表達原始猜想。因此，Lean檢查的是輸入命題與證明之間的邏輯連結，並不會自動保證將問題轉寫成形式語言的過程正確。

麻省理工學院研究人員 Guy Blanc，以及史丹佛大學研究人員 Jordan Docter、Carmen Strassle 與 Li-Yang Tan，7日公開一份解說證明邏輯的文件。四人表示，他們從PSI取得證明後進行審查，並撰寫了解說。

研究人員也在文件中說明，撰寫過程使用了 Anthropic 公開的模型。他們表示，未從PSI或 Anthropic 收取金錢報酬。

研究人員表示，沒有計畫將解說文件投稿至學術會議或期刊。文件公開不代表這份證明已通過同儕審查。

艾倫森強調，不應將這項結果擴大解讀為量子優勢全面消失。研究範圍限於隨機輸入下的特定判定問題，以及量子查詢複雜度。

他表示，這項結果不影響用於質因數分解的 Shor 演算法，也不影響量子物理或化學模擬。這項公開研究也沒有評估虛擬資產密碼技術的安全性。

研究範圍是特定數學猜想的證明與形式化驗證，並未提出與半導體產業的直接關聯。