AI 評測與形式化推理
FormalTCS Tests the Research Workflow With 175 Lean Problems; Automated Formalization Scores Just 11.5 at Best
FormalTCS extracts research-grade problems from top theoretical computer science papers published over the past two years, measuring models stage by stage as they turn natural-language claims into machine-verifiable proofs. The best model achieves a Pass@8 of 28.6 when proving already-formalized theorems, but translating natural language into correct Lean theorem statements remains the primary bottleneck.
FormalTCS breaks theoretical computer science research into stages: understanding the core claim, constructing a natural-language description, formalizing the theorem, planning a proof strategy, and generating a Lean proof. The dataset contains 175 instances drawn from papers accepted to STOC, FOCS, SODA, and COLT in 2025 and 2026. It preserves each paper’s custom definitions, assumptions, and proof dependencies, with experts creating and validating the Lean versions.
The researchers used Codex, Claude Code, and the DeepSeek harness to test the GPT-5.6, Claude 5, and DeepSeek-V4 families. Claude Opus 5 scored 68.7 on natural-language proof-strategy generation, but only 11.5 in the NC2FT stage, which generates formal definitions and theorems from natural-language claims. GPT-5.6 Sol likewise fell from 67.9 to 10.6. When humans supplied the formalized theorem first, Opus 5 achieved a Lean-proof Pass@8 of 28.6. This suggests that the difficulty lies not only in proof search, but also in identifying mathematical objects, quantifiers, assumptions, and types and encoding them accurately.
The team also built a research loop comprising a planner, formalizer, and judger. Of the 64 novel claims proposed by the system, only six ultimately passed both expert assessment of their value and formal proof verification, revealing that “research taste” remains a second hurdle beyond formal correctness. The authors conducted a black-box contamination audit using anonymized excerpts. Text-reconstruction similarity for the two strongest models was below 9.6%, although this can only reduce—not eliminate—concerns about training-data leakage. The natural-language stages also relied partly on LLM-based evaluation. From an engineering perspective, the key takeaway is that without independent definition checking and formalization-verification layers, automated theorem-proving agents may begin an entire chain of reasoning from an incorrect proposition even when the proof strategy appears plausible.