FormalTCS: Benchmarking End-to-End Frontier Formal Theoretical Computer Science Research of Large Language Models
作者: Dingzirui Wang, Xuanliang Zhang, Keyan Xu, Qingfu Zhu, Wanxiang Che
分类: cs.CL
发布日期: 2026-08-20
💡 一句话要点
提出FormalTCS基准以评估大语言模型在理论计算机科学研究中的表现
🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)
关键词: 大语言模型 理论计算机科学 自动化研究 形式化验证 基准测试
📋 核心要点
- 现有的基准测试无法真实反映大语言模型在理论计算机科学研究中的应用效果，存在明显的不足。
- 本文提出FormalTCS基准，包含175个经过专家验证的实例，旨在评估LLMs在TCS研究中的表现。
- 实验结果显示，当前模型在自动形式化方面表现不佳，且生成的声明通过率极低，反映出研究品味的缺乏。
📝 摘要（中文）
大语言模型（LLMs）在自动化理论计算机科学（TCS）研究中展现出越来越大的潜力，但现有基准与真实研究环境相去甚远。本文引入了FormalTCS，一个经过专家验证的基准，用于评估LLMs在前沿、端到端的TCS研究中的表现。该基准包含175个实例，来源于2025-2026年接受的STOC、FOCS、SODA和COLT论文，保留了论文特定的定义、假设和证明依赖关系，并附有专家验证的Lean形式化和证明。对领先LLMs的评估显示，当前模型在完整研究流程中仍远未可靠完成，尤其是在自动形式化方面，最佳模型在将自然语言声明翻译为形式定理陈述时仅取得11.5的分数，而在证明人类提供的形式声明时则为28.6。基于FormalTCS，我们进一步开发了一个自动化的TCS研究框架，生成、形式化、过滤和证明新的声明。在生成的64个声明中，只有6个最终通过专家评估和证明验证，表明除了形式化之外，有限的研究品味也是自主TCS研究的另一大障碍。
🔬 方法详解
问题定义：本文旨在解决现有基准测试无法真实反映大语言模型在理论计算机科学研究中的应用效果的问题。当前方法在自动形式化和研究品味方面存在显著不足。
核心思路：提出FormalTCS基准，通过专家验证的实例来评估LLMs在TCS研究中的表现，特别关注自动形式化的能力。
技术框架：整体架构包括生成、形式化、过滤和证明新声明的自动化研究框架。主要模块包括实例生成、形式化处理、专家评估和证明验证。
关键创新：最重要的创新在于引入了FormalTCS基准，提供了一个真实的评估环境，并揭示了当前LLMs在自动形式化和研究品味方面的局限性。
关键设计：在生成声明时，采用了专家验证的Lean形式化，确保了声明的准确性和有效性。实验中对模型的评估采用了Pass@8等指标，反映了模型在不同任务上的表现。
🖼️ 关键图片
📊 实验亮点
实验结果显示，当前最佳模型在将自然语言声明翻译为形式定理时仅取得11.5的分数，而在证明人类提供的形式声明时则为28.6，表明自动形式化是主要瓶颈。此外，生成的64个声明中仅有6个通过专家评估，显示出研究品味的缺乏。
🎯 应用场景
该研究的潜在应用领域包括自动化理论计算机科学研究、智能辅助证明系统以及教育领域的自动化学习工具。通过提升大语言模型在TCS研究中的表现，未来可能推动相关领域的研究效率和质量。
📄 摘要（原文）
Large language models (LLMs) have shown growing potential for automated theoretical computer science (TCS) research, yet existing benchmarks remain far from realistic research settings. We introduce \ourbenchmark, an expert-validated benchmark for evaluating LLMs on frontier, end-to-end TCS research. \ourbenchmark contains $175$ instances drawn from papers accepted to STOC, FOCS, SODA, and COLT in 2025-2026, preserving paper-specific definitions, assumptions, and proof dependencies, with expert-verified Lean formalizations and proofs. Evaluations of leading LLMs reveal that current models remain far from reliably completing the full research pipeline. In particular, autoformalization is the sharpest bottleneck: the best model achieves only $11.5$ on translating natural-language claims into formal theorem statements, compared with $28.6$ Pass@8 when proving human-provided formal statements. Building on \ourbenchmark, we further develop an automated TCS research framework that generates, formalizes, filters, and proves new claims. Of $64$ generated claims, only $6$ ultimately pass expert evaluation and proof verification, indicating that beyond formalization, limited research taste remains another major barrier to autonomous TCS research.