剛剛，姚期智與楊植麟兩位AI大牛首次聯手發表新論文。
11月8日消息，智能紀元AGI獨家獲悉，近期，圖靈獎得主、中國科學院院士、清華大學交叉資訊研究院院長姚期智團隊，聯合月之暗面（Kimi）創始人楊植麟等人發表論文：《TCSEXAM：在TCS研究的全範圍內評估前沿大型語言模型》。
這不是一篇關於某個新模型的論文。他們做了一件更狠的事，給 9 個前沿大模型出了一張理論電腦科學的考卷。
考卷名叫TCSExam基準，100 道題，覆蓋 TCS 研究的完整鏈條。判分的不是人，是 Lean 證明器和可執行檢查器。
結果出來了。GPT-6 Astra 在裸命題定理證明上拿了 70%，第二名 Kimi K3.1 Pro 是 38.3%，剩下六個模型最高不超過 11.7%。
更有意思的是構造題環節。
其中，GPT-6 Astra 平均得分 104.9，超過了人類公開參考基線。Kimi K3 單獨做出了兩個改進，一個是 124 頂點無三角形圖的邊數從 629 推到 630，另一個是量子糾錯碼 [[25,7,6]] 的最小距離從 5 提到 6。
但 30 道公開猜想，沒有任何一個模型完整證明或證偽了其中任何一道。
那麼，為什麼要給 TCS 出一張考卷？
理論電腦科學不是刷題能解決的學科。
一個 TCS 研究者的日常工作大概分四塊。證明定理，寫求解器跑算例，構造滿足特定性質的數學對象，以及對著那些幾百年沒人解決的公開猜想死磕。
之前的 AI 評測基準只覆蓋其中一塊。TCS-BENCH 和 FormalTCS 只做定理形式化證明，FrontierCS 只做程序任務。沒有人把四塊拼在一起考過。
這就導致一個問題。我們知道 GPT-6 能證明定理，也知道它能寫程式碼，但不知道它能不能像一個真正的 TCS 研究者那樣，完整地走完一個研究周期。
TCSExam 就是來回答這個問題的。
而100 道題怎麼出的？完整版 TCSExam-Full 有 100 道專家稽核過的任務，分四條賽道。
定理證明賽道 20 道，全部從近年 TCS 論文裡摘出來的研究級命題。模型要輸出 Lean4 證明，三種難度設定，bare 模式只給命題本身，ladder 模式給中間引理，guided 模式再加證明思路。
求解器工程賽道 30 道。給問題規範和一個簡單基線程序，模型輸出可復用的求解程式碼，然後在大量隱藏測試實例上跑。
構造賽道 20 道。模型要生成具體的數學對象，比如碼、圖、幾何構型，附帶性質證書。打分對標人類公開記錄，100 分是參考基線，超過 100 就是比人類做得更好。
公開猜想賽道 30 道。模型要嘗試證明或證偽未解決的猜想，判分是二元的，完全解決得 100，否則 0。
還有一個輕量版 TCSExam-Lite，每條賽道 5 題共 20 題，任務嘗試量減少 80%，但打分規則不變。
整個出卷流程極其嚴格。專家篩選課題之後，Agent 輔助寫形式化聲明和打分器，再由獨立 review agent 總和檢查碼原始論文的一致性。試點階段淘汰了超過 40 道定理題。異常高分結果會觸發二次溯源校驗。
那麼，誰考得最好？
根據論文，GPT-6 Astra 是毫無疑問的第一名。
定理證明 bare 模式下 70% 的完成率，意味著 20 道研究級定理它完整證明了 14 道。在不給任何中間提示的情況下，這個數字放在人類博士生裡也是頂尖水平。
求解器賽道 Astra 的相對得分是 64.7%，在 IWLS2023 邏輯綜合任務上，它生成的程序在大量算例上優於公開競賽參考。
構造賽道 Astra 平均 104.9 分。這是整篇論文最值得注意的數字，因為它意味著 AI 在某些具體數學構造上，已經超過了人類目前公開的最好結果。
Kimi K3 排第二。它的亮點不在定理證明，而在兩個具體構造上。一個是 124 頂點無三角形無 4 環圖，人類最好的構造是 629 條邊，Kimi K3 給出了 630 條邊的構造。另一個是量子糾錯碼，[[25,7,5]] 是人類已知的最好參數，Kimi K3 推到了 [[25,7,6]]。
DeepSeek 的表現很分裂。DeepSeek V4.1 Flash 0910 在 bare 定理證明上一道都沒做出來，但它在構造任務裡產出過優於參考基線的結果。
8 個同時參加完整版和輕量版的模型，綜合指數排名的斯皮爾曼相關係數是 0.93。28 對模型排名裡有 26 對順序保持一致。這意味著 20 道題的輕量版就能基本代表 100 道題完整版的區分度。
但這篇論文最重要的結論，不是誰考了第一。
是大模型在 TCS 上的能力分佈極其不均勻。
同一個模型，可能在裸命題定理證明上一道都做不出來，但在構造任務上能改進人類的公開記錄。DeepSeek V4.1 Flash 0910 就是最極端的例子，bare 定理證明 0 分，但構造任務有產出。
另一個發現是提示的槓桿效應。Kimi K3 在 bare 模式解決了 3 道定理，到了 guided 模式能解決 7 道。這說明模型其實知道很多證明片段，只是不知道怎麼把它們串起來。給它中間引理和思路提示，能力立刻翻倍。
第三個發現可能是最重要的。那怕模型沒有完整解決公開猜想，它也能產出有數學價值的中間結果。GPT-6 Astra 給出了 Alon-Jaeger-Tarsi 猜想在 F₅域下 n≤9 的形式化驗證特例，拓展了人類之前已知的範圍。這些特例和邊界結果，雖然不能直接解決猜想，但本身就是數學貢獻。
之前我們評測大模型做數學，要麼看定理證明完成率，要麼看競賽題得分。這篇論文告訴我們，中間產出同樣重要。一個模型可能解不出最終猜想，但它能幫數學家把某個特例驗證了，把某個上界改進了，把某個求解器跑通了。這就是實實在在的科研貢獻。
那麼，離真正的 AI 數學家還有多遠？
30 道公開猜想，0 個完整解決，這個數字很說明問題。
大模型現在能做的，是在給定框架內改進已有結果，是把已知的證明片段重新組合，是在人類畫好的邊界裡再往前推一小步。
真正的猜想解決需要的東西不一樣。它需要跳出現有框架，提出全新的概念和方法，需要在黑暗裡找到方向。這些能力，目前的大模型還不具備。
論文裡提到，有兩個模型復用了 OpenAI 已經公開的 Ryser 猜想和 MIRUP 猜想反例，完成了兩道公開猜想任務。這不是原創發現，只是搬運。
姚期智和楊植麟做這件事的意義，不在於宣佈 AI 數學家已經誕生。而在於第一次給 TCS 研究的完整鏈條建了一個可復現、可自動校驗的評測框架。
有了這個框架，後面模型迭代到什麼程度，就有了一把統一的尺子。
現在的第一名是 GPT-6 Astra，綜合指數 71.9。這個數字明年會是多少，我們等著看。 (智能紀元AGI)