AI 評測與形式化推理
FormalTCS 以 175 個 Lean 題目測試研究流程，自動形式化最高僅 11.5 分
FormalTCS 從近兩年頂級理論計算機科學論文抽取研究級問題，逐段測量模型由自然語言主張產生機器可驗證證明的能力。最佳模型在證明既有形式化定理時達 28.6 Pass@8，但將自然語言轉成正確 Lean 定理陳述仍是主要瓶頸。
FormalTCS 將理論計算機科學研究拆成理解核心主張、建立自然語言敘述、形式化定理、規劃證明策略及產生 Lean 證明等階段。資料集包含 175 個實例，來源為 2025 至 2026 年獲 STOC、FOCS、SODA 與 COLT 接收的論文，保留各論文自訂的定義、假設與證明依賴，並由專家建立及驗證 Lean 版本。
研究以 Codex、Claude Code 與 DeepSeek harness 測試 GPT-5.6、Claude 5 及 DeepSeek-V4 系列。Claude Opus 5 在自然語言證明策略生成取得 68.7 分，但由自然語言主張產生形式定義與定理的 NC2FT 階段只有 11.5；GPT-5.6 Sol 亦由 67.9 降至 10.6。當人類先提供形式化定理後，Opus 5 的 Lean 證明 Pass@8 可達 28.6，顯示困難不只在證明搜尋，更在辨識數學物件、量詞、假設及型別並準確編碼。
團隊另建立 planner、formalizer 與 judger 組成的研究迴圈。系統提出的 64 項新主張中，最後只有 6 項同時通過專家價值判斷及形式證明驗證，暴露「研究品味」仍是形式正確性之外的第二道關卡。作者以匿名片段進行黑箱污染稽核，兩個最強模型的文字重建相似度低於 9.6%，但這只能降低、不能排除訓練資料洩漏疑慮；自然語言階段亦部分依賴 LLM 評分。工程上值得關注的是，自動定理證明代理若沒有獨立的定義檢查與形式化驗證層，即使證明策略看似合理，仍可能從錯誤命題開始整條推導。