OpenAI公布反駁指數時間假說結果，Anthropic也公開形式化資料

OpenAI公布反駁指數時間假說（ETH）的研究結果，並公開以 Lean 驗證的形式化證明資料；Anthropic也將相關論文與形式化資料上傳至儲存庫。

OpenAI於10月26日表示，其系統得出反駁ETH的結果，並以Lean驗證形式化證明。外部專家小組將檢視這項結果的意義與適用範圍。OpenAI也宣布成立合作小組，讓電腦科學家共同驗證並說明結果。OpenAI官方公告說明了研究結果與後續審查計畫。

Anthropic則將Claude撰寫的論文及相關形式化資料發布在公開儲存庫。儲存庫介紹一種計算可滿足指派數量的演算法，以及ETH相關形式化專案。不過，僅憑儲存庫中的說明，無法認定專家已完成獨立審查。

指數時間假說（ETH）是計算複雜度理論中的假說，主張3-SAT無法在低於變數數量指數級的時間內求解。3-SAT探討的是：對於每個條件由至多三個邏輯文字組成的公式，是否存在一組變數指派，能讓所有條件都成立。這次主張的重點並非以多項式時間解決此問題，而是提出一種增長速度低於指數時間的準指數時間演算法。

準指數時間演算法即使比指數時間快，也不代表實際運算立刻具備實用速度。因此，這項結果不表示所有困難的計算都能快速完成，也不代表研究已解決P與NP問題。P與NP問題探討的是，所有能快速驗證答案的問題是否也都能快速求解。

OpenAI的形式化範圍文件描述了一種能精確計算特定編碼方式下邏輯公式可滿足指派數量的演算法。文件指出，以Lean形式化的執行時間上界，可能與另行公開的論文所列上界不同。Anthropic的儲存庫也介紹了計算可滿足指派數量的確定性圖靈機，以及ETH相關形式化資料。

Lean驗證是由電腦檢查形式化命題證明的程序。這項驗證本身無法判定形式化命題是否精確對應原始問題，也無法確立研究結果在既有研究中的意義；這些事項仍須經過數學證明審查，並另行評估結果的適用範圍。

指數時間假說過去被用作圖論、計算生物學與資料庫等領域中，分析問題難度的條件式結果前提。OpenAI表示，即使這項主張通過獨立審查，要將其轉化為更快的演算法或實際效能改善，仍需要進一步研究。既有研究前提可能改變，與應用問題立即變得容易，是兩回事。

指數時間假說的縮寫ETH與以太幣（ETH）的代號相同，但本文所指的是計算複雜度理論中的假說。這項研究與以太坊網路無關，目前公布的結果也沒有證據顯示比特幣（BTC）或以太坊的密碼系統已遭破解。外界目前正根據公開的證明與形式化資料進行獨立審查。