新聞

OpenAI上周六（8/1）揭露，下一款主要模型Astra的內部版本，在數學及理論電腦科學領域取得10項研究成果，涵蓋高維幾何、編碼理論、群論、量子複雜度及格基密碼學等領域。相關問題至少已有10年未在主要結果上取得進展，多數停滯時間更久。

Astra是OpenAI尚未推出的通用模型，並非專門用來解答數學問題。The Information報導，Astra被設計為可連續數小時或數日處理複雜工作，並能協調多個AI代理人共同執行任務。OpenAI這次則展示其數學研究能力，包括尋找開放問題的解法、跨不同領域運用既有理論、提出新證明、反例及數學建構，並把論證轉換成電腦可檢查的形式化證明。

10項成果中，Astra建構出首個非sofic群，證明這類群確實存在，回應群論自1999年以來的一項核心問題；也提出反例推翻Connes剛性猜想，否定某些群可由其von Neumann代數唯一決定的長期假設。模型並解決Ehrhart體積猜想，在所有維度下確定一個凸體以質心為唯一內部格點時，所能具有的最大體積。

在理論電腦科學方面，Astra證明一般雙方量子遊戲的指數型平行重複定理，把古典複雜度理論的一項基礎原則延伸至量子領域；並證明最近向量問題難以在多項式因子範圍內近似求解。最近向量問題是格基密碼學的重要基礎問題，也是部分後量子密碼系統安全性的理論基礎。

其它成果還包括改善高維球體堆積密度、二元碼及球面碼的理論界限，提出計算矩陣永久值所需算術電路的新下界，以及改善多色三角形Ramsey數的下界。Astra另解決Erdős第146、180及183號問題。不過，10項成果性質不盡相同，其中部分完整解決既有問題或推翻猜想，部分則是改善既有界限，並非全部給出最終答案。

OpenAI表示，Astra尋找10項解法所使用的token，若依GPT-5.6 Sol API費率計算，總成本約2,000美元。數學論證由模型產生，再由人類使用同一模型協助整理成論文，之後由模型轉換成可由Lean形式化證明系統逐步檢查的證明。OpenAI也公布模型對各項解法的推理敘述，並表示公司協助整理及形式化證明，也對其正確性負責，但數學論證本身應歸功於AI系統。