月之暗面（Moonshot AI）開源理論計算機科學研究基準 TCSExam：從 Lean 形式化證明到開放猜想的全鏈路評測解析
文章摘要：月之暗面（Moonshot AI）聯合多位研究學者（Yifan Luo、Zhengying Liu、Yang Yuan、Zhilin Yang 與圖靈獎得主姚期智 Andrew Chi-Chih Yao），正式發表並開源理論計算機科學（Theoretical Computer Science, TCS）研究評測基準 TCSExam（技術論文 arXiv:2611.07962、GitHub 程式碼庫）。不同於過往僅針對單一數學競賽題或孤立程式碼片段的基準，TCSExam 將理論計算機科學的完整研究週期拆解為定理證明（Theorem Proving）、求解器工程（Solver Engineering）、**顯式構造（Constructions）與開放猜想（Open Conjectures）**四大可驗證賽道，提供包含 100 道題目的 TCSExam-Full 與 20 道題目的 TCSExam-Lite 兩套評測集。根據官方專案主頁公布的實測結果，前沿模型結合代理框架在單題最長 12 小時的運算預算下，已能在構造賽道中刷新人類文獻紀錄（如 Kimi K3 將 124 頂點無 $C_3, C_4$ 圖的邊數從 629 條推升至 630 條，GPT-6 Astra 構造出距離為 6 的 $[[25,7,6]]$ 量子糾錯碼），而 DeepSeek V4.1 Flash 1017 與 Kimi K3.1 Pro 也在開放猜想賽道中取得非零的自動化證明或證偽突破。本文根據 TCSExam 官方網站、GitHub 官方儲存庫與官方技術文件，完整整理基準架構、計分機制、8 款前沿模型榜單表現、研究突破案例與本地部署指南。
為什麼需要 TCSExam？從單點解題走向完整理論研究週期
在理論計算機科學（TCS）的實際研究中，學者的工作並非只有「寫出一段最終證明」。根據 TCSExam 技術論文與 OpenReview 論文預覽的分析，真實的理論探索往往由多個環節相互推進：研究人員會先撰寫演算法求解器（Solver）搜尋候選數學物件，透過顯式構造（Construction）收緊問題的上下界，接著將已發表的複雜定理進行形式化證明（Theorem Proving），最終累積足夠的工具與結構洞察來攻克懸而未決的開放猜想（Open Conjectures）。
過往的評估基準多半只切取其中一個斷面，例如僅測試 Lean 4 組合數學形式化的 CombiBench，或是專注於機器學習工程複製的代理基準。TCSExam 則將這四種理論研究產出整合至同一個可擴展的框架中，針對每一類任務設計獨立且嚴格的自動化驗證機制（如 Lean 核心檢查、憑證驗證與系統呼叫沙箱測試），讓大型語言模型與代理系統（Agent Runtimes）在貼近真實學術研究的環境下接受檢驗。
四大研究評測賽道與 Full / Lite 雙套件架構
根據 TCSExam 官方網站與 GitHub 儲存庫說明，基準分為 **TCSExam-Full（共 100 題）**與 **TCSExam-Lite（共 20 題，由四類題型各選 5 題組成）**兩個版本。四個研究賽道的任務配置、驗證方式與代表性研究主題整理如下：
| 評測賽道 | Full 題數 | Lite 題數 | 任務要求與提交內容 | 自動化驗證機制 | 代表性子領域與任務範例 | 資料來源 |
|---|---|---|---|---|---|---|
| 定理證明（Theorem Proving） | 20 題 | 5 題 | 針對已發表的理論計算機科學成果，撰寫完整的 Lean 形式化數學證明 | Lean 核心驗證 + 公理檢查（Axiom Checks） | 加性組合（準多項式角點界）、演算法（Dijkstra 演算法的普適最優性）、偏差理論（超越 Banaszczyk 界）、離散競標博弈（discrete-bidding-games） | TCSExam 官網 |
| 求解器工程（Solver Engineering） | 30 題 | 5 題 | 實作可重複使用的演算法求解器執行檔，並在隱藏測試實例上評估效能 | 可執行任務檢查器 + Landlock 沙箱隔離 | Full 採用線上求解器（開發期間提供即時評測回饋）；Lite 採用離線求解器（開發時僅有公開自測，提交後以隱藏實例計分） | TCSExam 官網 / GitHub |
| 顯式構造（Constructions） | 20 題 | 5 題 | 生成具備特定性質的顯式數學物件或界（Bounds），並附帶形式化驗證證明 | Lean 核心驗證 + 憑證檢查（Certificate Checks） | 極值圖論（禁止 $C_3, C_4$ 的 124 頂點圖）、量子編碼與糾錯（$[[25,7,6]]$ 量子糾錯碼） | TCSExam 官網 |
| 開放猜想（Open Conjectures） | 30 題 | 5 題 | 針對尚未解決的開放理論猜想，給出完整的形式化證明或反例證偽 | 獨立主證明槽（Independent Main Proof Slots）之 Lean 驗證 | 量子計算（Aaronson-Ambainis 猜想）、組合數學（Alon-Jaeger-Tarsi 猜想）、整數規劃（整數向上取整間隙）、圖論（Caccetta-Häggkvist 猜想） | TCSExam 官網 |
綜合評分公式與評測預算設定
為了衡量模型在常規理論推進與高風險猜想突破上的整體實力，TCSExam 官方網站定義了加權綜合指標 TCSExam Index：
$$\text{TCSExam Index} = 0.3 \times \text{Theorems} + 0.3 \times \text{Solvers} + 0.3 \times \text{Constructions} + 0.1 \times \text{Open Conjectures}$$在閱讀榜單數據時，有兩項關鍵的評測規則需要注意：
- 顯式構造（Constructions）的基準線為 100%：在構造賽道中，得分 100% 代表模型的構造結果剛好達到人類文獻的參考基準（Reference Baseline）；若得分超過 100%，則代表模型找到了比現有參考基準更優的顯式數學構造或界。
- 單題 12 小時運算預算與多次嘗試平均：根據官方榜單說明，每次評測嘗試（Attempt）最高分配 12 小時的運算預算（Compute Budget）。在官方測試中，Kimi K3、Kimi K3.1 Pro 與 DeepSeek V4.1 Flash 1017 每道題均執行 3 次完整嘗試並取平均分數；其餘對照模型則執行 1 次嘗試。
前沿模型實測榜單：TCSExam-Full 與 TCSExam-Lite 完整數據
根據 TCSExam 官方網站與 GitHub 提交紀錄，研究團隊對多款閉源與開源前沿模型進行了系統性評估。
1. TCSExam-Full 完整套件榜單（100 道題）
在涵蓋 100 道題目的完整套件中，各模型於四大賽道的得分與綜合指標表現如下（資料來源：TCSExam 官方網站）：
| 模型名稱 | 綜合指標 (Overall Index) | 定理證明 Theorems (%) | 求解器工程 Solvers (%) | 顯式構造 Constructions (%) | 開放猜想 Open Conjectures (%) | 測試嘗試次數 | 資料來源 |
|---|---|---|---|---|---|---|---|
| GPT-6 Astra | 71.9 | 70.0% | 64.7% | 104.9% | 0.0% | 1 次 | TCSExam 官網 |
| Kimi K3.1 Pro | 57.4 | 38.3% | 54.1% | 98.6% | 1.1% | 3 次平均 | TCSExam 官網 |
| Kimi K3 | 46.8 | 11.7% | 48.7% | 95.5% | 0.0% | 3 次平均 | TCSExam 官網 |
| DeepSeek V4.1 Flash 1017 | 46.0 | 6.7% | 53.1% | 91.8% | 5.6% | 3 次平均 | TCSExam 官網 |
| GLM-5.3 | 45.5 | 5.0% | 49.1% | 97.7% | 0.0% | 1 次 | TCSExam 官網 |
| Qwen3.8 Max (0902) | 44.8 | 5.0% | 49.2% | 95.1% | 0.0% | 1 次 | TCSExam 官網 |
| Grok 4.6 | 40.5 | 5.0% | 43.8% | 86.2% | 0.0% | 1 次 | TCSExam 官網 |
2. TCSExam-Lite 精簡套件榜單（20 道題）
在包含 20 道代表性題目的 Lite 套件中，研究團隊另外納入了 Claude Opus 5.5 進行對照，完整成績如下（資料來源：TCSExam 官方網站）：
| 模型名稱 | 綜合指標 (Overall Index) | 定理證明 Theorems (%) | 求解器工程 Solvers (%) | 顯式構造 Constructions (%) | 開放猜想 Open Conjectures (%) | 測試嘗試次數 | 資料來源 |
|---|---|---|---|---|---|---|---|
| Opus 5.5 | 72.3 | 80.0% | 60.5% | 100.4% | 0.0% | 1 次 | TCSExam 官網 |
| GPT-6 Astra | 67.0 | 60.0% | 63.0% | 100.4% | 0.0% | 1 次 | TCSExam 官網 |
| Kimi K3.1 Pro | 53.5 | 40.0% | 50.0% | 88.3% | 0.0% | 3 次平均 | TCSExam 官網 |
| Kimi K3 | 48.6 | 33.3% | 48.9% | 79.8% | 0.0% | 3 次平均 | TCSExam 官網 |
| GLM-5.3 | 47.0 | 20.0% | 46.1% | 90.7% | 0.0% | 1 次 | TCSExam 官網 |
| Qwen3.8 Max (0902) | 45.4 | 20.0% | 51.0% | 80.3% | 0.0% | 1 次 | TCSExam 官網 |
| DeepSeek V4.1 Flash 1017 | 42.4 | 6.7% | 54.3% | 80.2% | 0.0% | 3 次平均 | TCSExam 官網 |
| Grok 4.6 | 42.1 | 20.0% | 41.0% | 79.3% | 0.0% | 1 次 | TCSExam 官網 |
3. 榜單數據反映的四個核心現象
從 TCSExam 官方榜單的跨賽道數據中，可以清楚觀察到當前前沿模型在理論研究能力上的結構性落差：
- Lean 形式化定理證明是拉開總分差距的分水嶺：各模型在「求解器工程」（大多落在 43% 至 64% 之間）與「顯式構造」（大多落在 86% 至 104% 之間）的表現相對接近，但在「定理證明」賽道卻出現劇烈分化。在 Full 榜單中，GPT-6 Astra 取得 70.0% 的定理證明率，Kimi K3.1 Pro 則以 38.3% 位居第二（較前代 Kimi K3 的 11.7% 提升超過三倍），而其餘開源與閉源模型的定理證明得分均低於 7%。在 Lite 榜單中，Opus 5.5 則以 80.0% 的定理證明率拿下最高總分（72.3）。
- 模型在顯式構造賽道已具備超越人類基準的能力：在 Full 榜單中，GPT-6 Astra 的構造得分達 104.9%；在 Lite 榜單中，Opus 5.5 與 GPT-6 Astra 均取得 100.4%。這說明當研究問題可轉化為程式搜尋與形式化憑證驗證時，前沿模型能夠找出現有文獻未曾發現的更優構造。
- 開放猜想賽道出現非零突破：在難度最高的 30 道開放猜想（Full 套件）中，多數模型得分為 0.0%，但 DeepSeek V4.1 Flash 1017 取得了 5.6% 的解決率，Kimi K3.1 Pro 也取得 1.1% 的成績，顯示長時程代理搭配形式化驗證工具已能針對特定未解問題給出經 Lean 驗證的證明或反例。
- Kimi K3.1 Pro 在全套基準中穩居開源與國產模型首位：在 TCSExam-Full 與 TCSExam-Lite 兩份榜單中，Kimi K3.1 Pro 分別以 57.4 與 53.5 的綜合指標排名總榜第二（Full）與第三（Lite），在定理證明、求解器工程與顯式構造三個維度展現出均衡的研究能力。
模型超越人類參考基準的兩大實證研究突破
在 TCSExam 官方網站的「Research Outcomes（研究成果）」專區中，研究團隊特別展示了兩項由模型在評測過程中自主完成、並通過嚴格驗證的理論計算機科學新紀錄：
1. 極值圖論突破：Kimi K3 將 124 頂點無 $C_3, C_4$ 圖邊數從 629 推升至 630
在極值圖論（Extremal Graph Theory）中，一個經典問題是：在包含 124 個頂點且同時禁止出現三角形（$C_3$）與四邊形（$C_4$，即圍長 girth $\ge 5$）的圖中，最多可以包含多少條邊？
根據 TCSExam 官網成果報告，此前由人類學者 Goedgebeur 等人於 2025 年發表的最佳構造紀錄為 629 條邊。在 TCSExam 的顯式構造評測中，Kimi K3 成功構造出一個包含 630 條邊的 124 頂點圖，且完全不包含任何 $C_3$ 與 $C_4$ 子圖，並附上經形式化驗證的完整憑證，直接刷新了該問題的下界紀錄。
2. 量子糾錯碼突破：GPT-6 Astra 構造出距離為 6 的 $[[25,7,6]]$ 量子碼
在量子資訊與量子糾錯（Quantum Error Correction）領域，研究人員致力於用更少的實體量子位元（Physical Qubits）保護更多的邏輯量子位元（Logical Qubits），同時最大化碼距（Code Distance）。
根據 TCSExam 官網成果報告，在使 25 個實體量子位元保護 7 個邏輯量子位元的設定下，過去標準參考表（Grassl’s Code Tables）所記載的碼距上限為 5。在評測過程中，GPT-6 Astra 成功構造出一個 $[[25,7,6]]$ 量子糾錯碼，將碼距從 5 提升至 6，使其能夠偵測最多影響 5 個量子位元的錯誤，超越了既有參考表的紀錄。
儲存庫架構、支援代理環境與本地快速上手指南
根據 MoonshotAI/TCSExam GitHub 儲存庫與 DecoHack AI 早報整理，TCSExam 底層透過自動安裝的 Harbor 0.22.0 編排代理執行環境，並在求解器評分期間強制要求 Linux 核心支援 Landlock ABI 3 或更高版本，以實現容器內系統呼叫（Syscall）的安全沙箱隔離。
1. 支援的代理框架與開源授權條款
- 支援的代理執行環境（Agent Runtimes）：預設使用月之暗面開源的 Kimi Code（
kimi-code），同時原生支援 Claude Code、Codex 與 Grok Build（詳見 Agent Configuration 文件）。 - 系統硬體與環境需求：需運行於 Linux x86-64 主機，具備 Python 3.12+、Docker Engine（含 Docker Compose 與 Buildx），以及支援 Landlock ABI 3+ 的 Linux 核心。
- 多重開源授權協議：
- 專案自研程式碼與腳本：採用 Apache License 2.0 授權。
- 題目敘述、文件與網頁內容：採用 CC BY 4.0（Creative Commons Attribution 4.0 International）授權。
- 隨附研究論文（
paper.pdf）：採用 CC BY-NC-ND 4.0 授權。
2. 安裝與執行單題評測完整流程
根據 TCSExam 官方快速開始指南（Getting Started），在 Linux x86-64 環境中部署並執行評測的步驟如下：
步驟一：檢查系統依賴與 Docker Buildx 環境
sudo apt update
sudo apt install -y git curl ca-certificates nano python3 python3-venv python3-pip libarchive13t64
python3 --version
uname -m
# 確認 Docker、Compose 與 Buildx 正常運作
docker info
docker compose version
docker buildx version
docker buildx inspect --bootstrap
步驟二：複製儲存庫並安裝 tcsexam 套件
git clone https://github.com/MoonshotAI/TCSExam.git TCSExam
cd TCSExam
python3 -m venv .venv
source .venv/bin/activate
python -m pip install -e '.[runtime,backend]'
# 驗證 CLI 工具與儲存庫結構完整性
tcsexam --help
tcsexam validate
步驟三：設定代理框架與模型 API 金鑰（.env）
複製範例設定檔並填入欲評測的模型端點與 API 金鑰（預設代理為 kimi-code）：
cp .env.example .env
chmod 600 .env
# 於 .env 檔案中設定以下變數：
# TCSEXAM_AGENT="kimi-code"
# TCSEXAM_API_BASE_URL="https://YOUR_PROVIDER.example/v1"
# TCSEXAM_MODEL="YOUR_MODEL_ID"
# TCSEXAM_API_KEY="YOUR_API_KEY"
# 將環境變數載入當前終端機工作階段
set -a
source .env
set +a
步驟四：建置單一任務鏡像並執行健康檢查
以 Lite 套件中的離散競標博弈定理證明題 discrete-bidding-games 為例，可先建置任務環境並透過 tcsexam doctor 與 tcsexam prepare 預覽工作配置（不消耗模型 API 額度）：
# 列出 Lite 套件任務並建置指定題目
tcsexam list --suite lite
tcsexam source-inputs
tcsexam build --suite lite --task discrete-bidding-games
tcsexam doctor --suite lite --task discrete-bidding-games \
--output build/first-readiness.json
# 產生並預覽 Harbor 任務設定檔
tcsexam prepare --suite lite --task discrete-bidding-games \
--output build/first-job.json
python -m tcsexam.harbor_launch run \
--config build/first-job.json --print-config
步驟五：啟動正式評測並檢視驗證結果
# 啟動單次嘗試（attempts=1）、單併發（concurrency=1）評測
tcsexam run --suite lite --task discrete-bidding-games \
--attempts 1 --concurrency 1 --output build/first-job.json
評測完成後，可透過官方提供的 Python 腳本直接讀取 result.json 中的驗證器結果（verifier_result）與執行紀錄（詳見 Running Suites 文件與 Stage Budgets 文件）。
相關參考連結
- TCSExam 官方網站與互動榜單：https://moonshotai.github.io/TCSExam/
- TCSExam 線上技術文件主頁：https://moonshotai.github.io/TCSExam/docs
- GitHub 官方程式碼庫（MoonshotAI/TCSExam）：https://github.com/MoonshotAI/TCSExam
- arXiv 技術論文（arXiv:2611.07962）：https://arxiv.org/abs/2611.07962
- OpenReview 論文 PDF 預覽：https://openreview.net/pdf?id=QhGdVnRPoi
- GitHub 快速開始指南（Getting Started）：https://github.com/MoonshotAI/TCSExam/blob/master/docs/getting-started.md
- GitHub 代理配置說明（Agent Configuration）：https://github.com/MoonshotAI/TCSExam/blob/master/docs/agent-configuration.md
- GitHub 執行配置說明（Run Configuration）：https://github.com/MoonshotAI/TCSExam/blob/master/docs/run-configuration.md
- GitHub 套件運行指南（Running Suites）：https://github.com/MoonshotAI/TCSExam/blob/master/docs/running-suites.md
- GitHub 階段預算說明（Stage Budgets）：https://github.com/MoonshotAI/TCSExam/blob/master/docs/stage-budgets.md
- GitHub 資源準備指南（Resource Preparation）：https://github.com/MoonshotAI/TCSExam/blob/master/docs/resource-preparation.md
- GitHub 常見問題排解（Troubleshooting）：https://github.com/MoonshotAI/TCSExam/blob/master/docs/troubleshooting.md
- Moonshot AI 官方 GitHub 組織頁：https://github.com/moonshotai
- DecoHack AI 早報（2026-11-06 月之暗面開源 TCSExam 報導）：https://decohack.com/ai-daily/2026-11-06/