FormalTCS: 大型语言模型端到端前沿形式化理论计算机科学研究基准测试

# FormalTCS：大型语言模型端到端前沿形式化理论计算机科学研究基准测试  
来源：https://arxiv.org/html/2608.20153  
丁子瑞、王轩良、张凯文、朱青付、车万翔  
哈尔滨工业大学  
\{dzrwang,xuanliangzhang,kyxu,qfzhu,car\}@ir\.hit\.edu\.cn  

###### 摘要  
大型语言模型（LLMs）在自动化理论计算机科学（TCS）研究方面展现出日益增长的潜力，但现有基准测试仍远未达到真实研究场景的要求。我们提出了 **FormalTCS**，一个经专家验证的基准测试，用于评估LLMs在前沿、端到端TCS研究中的能力。**FormalTCS** 包含175个实例，来源于2025-2026年被STOC、FOCS、SODA和COLT收录的论文，保留了论文特定的定义、假设和证明依赖关系，并提供了经专家验证的Lean形式化表达和证明。对领先LLMs的评估显示，当前模型仍远不能可靠地完成完整的研究流程。特别是，自动形式化是最大的瓶颈：在将自然语言陈述转化为形式化定理表述方面，最佳模型仅达到11.5%的性能，而在证明人类提供的形式化表述时，Pass@8为28.6%。基于 **FormalTCS**，我们进一步开发了一个自动化TCS研究框架，能够生成、形式化、过滤和证明新的陈述。在生成的64个陈述中，仅有6个最终通过专家评估和证明验证，这表明除了形式化之外，有限的研究品味仍是自主TCS研究的另一大障碍[111]。我们的代码已发布于 https://github.com/zirui-HIT/FormalTCS。  

## 1 引言  
理论计算机科学（TCS）通过数学方法研究计算的基本原理，包括计算模型、算法、计算复杂性和可计算性的极限[26 (https://arxiv.org/html/2608.20153#bib.bib31); 27 (https://arxiv.org/html/2608.20153#bib.bib32)]。TCS是一个重要的研究课题，因为它为理解哪些问题可以计算以及如何高效解决提供了理论基础。鉴于TCS的根本重要性以及大型语言模型（LLMs）日益强大的自主研究能力[3 (https://arxiv.org/html/2608.20153#bib.bib29)]，越来越多的研究开始探索LLMs执行TCS相关研究任务的能力。例如，LCS-Bench [8 (https://arxiv.org/html/2608.20153#bib.bib19)]从教科书中提取TCS知识构建基准测试，而TCS-Bench [4 (https://arxiv.org/html/2608.20153#bib.bib14)]评估LLMs根据自然语言陈述生成TCS定理证明的能力。然而，现有TCS基准测试与真实TCS研究仍存在显著差距：  
(i) **研究流程不完整**：现有基准测试主要评估孤立的能力，如自动形式化或证明生成。它们未能提供端到端评估来判断LLMs能否从零开始进行TCS研究，因此难以确定当前模型在整个研究过程中的失败点。  
(ii) **内容过时**：现有基准测试主要基于教科书材料或Mathlib [15 (https://arxiv.org/html/2608.20153#bib.bib20)] 等库中已有的定理构建。因此，它们对LLMs推理前沿TCS研究的能力提供的见解有限，并且可能因基准测试定理或相关材料出现在模型训练数据中而受到污染。  
(iii) **问题设置简化**：现有基准测试通常关注相对独立、定义完整明确的定理。相比之下，真实的TCS论文涉及论文特定的定义和假设，以及引理和定理之间的多层依赖关系。因此，现有基准测试无法衡量LLMs在现实环境中解决复杂、研究级别的TCS问题的能力。  

为弥合这些差距，我们推出了 **FormalTCS**，该基准测试旨在更真实地评估LLMs参与前沿TCS研究的能力。在GPT-5.6-sol [18 (https://arxiv.org/html/2608.20153#bib.bib27)] 的协助下，我们聘请了五位人类专家从TCS顶级会议收录的论文中收集和标注示例。与现有基准测试相比，**FormalTCS** 在三个方面更忠实评估TCS研究能力：  
(i) **端到端评估**：**FormalTCS** 将TCS研究流程分解为五个阶段，并逐步评估LLMs将自然语言TCS核心陈述转化为相应严格Lean证明的能力。这种设计能够对LLMs在整个TCS研究过程中的能力和瓶颈进行细粒度诊断。  
(ii) **前沿研究内容**：**FormalTCS** 构建于2025年和2026年被FOCS、STOC、SODA和COLT收录的论文。我们还根据源论文是否可能已被评估LLMs接触过进行额外过滤，从而在保持基准测试时效性的同时降低数据污染风险。  
(iii) **真实研究问题**：**FormalTCS** 评估直接取自真实TCS论文的核心理论问题，同时保留其论文特定的定义、假设和证明依赖关系。因此，它能更准确地衡量LLMs推理和证明研究级别TCS结果的能力。  

**表1：FormalTCS 揭示的主要发现。**  
我们在 **FormalTCS** 上评估了一系列领先的LLMs，发现总结于表1 [1 (https://arxiv.org/html/2608.20153#S1.T1)]。总体而言，当前最先进的模型仍难以有效执行端到端TCS研究，凸显了LLM-based TCS推理进一步发展的必要性，并证明了 **FormalTCS** 的必要性。特别是，我们发现**主要瓶颈在于将自然语言核心陈述转化为适当的形式化定义和定理表述**，当前最先进的LLMs仅能实现10%的性能。这表明当前LLMs的数学建模能力仍是TCS研究的主要限制。此外，基于 **FormalTCS**，我们开发了一个端到端TCS研究框架，支持从提出TCS核心陈述到生成严格Lean证明的完整流程。实验表明，现有LLMs能够为自身提出的核心陈述生成严格证明。然而，人工检查显示，大多数提出的陈述缺乏新颖性，表明**当前模型在TCS领域的研究品味仍不成熟**。  

我们的贡献可总结如下：  
1. 我们引入了 **FormalTCS**，一个基于真实研究问题的基准测试，用于评估LLMs在前沿TCS研究中的端到端能力。  
2. 我们的实验揭示了当前LLMs的一个关键瓶颈：将自然语言核心陈述转化为适当的形式化定义和定理表述，这表明数学建模仍是当前LLMs的主要弱点。  
3. 基于 **FormalTCS**，我们开发了一个用于TCS的端到端LLM研究框架，并发现，尽管当前模型通常能证明自己构建的陈述，但它们提出新颖且有意义的研究陈述（即其研究品味）的能力仍然有限。  

## 2 FormalTCS 简介  
### 2.1 总体统计  
**图1：FormalTCS 覆盖的研究领域分布。**  
**FormalTCS** 是一个经专家验证的基准测试，旨在评估LLMs在前沿TCS研究中的端到端能力。它包含175个实例，每个实例来源于一篇不同的研究论文，共涵盖175篇论文。我们使用Lean 4.32.2 [15 (https://arxiv.org/html/2608.20153#bib.bib20)] 及其对应的Mathlib版本，这是标注时可用的最新版本。我们通过以下维度确保 **FormalTCS** 的质量：  
(i) **高难度**：在所有实例中，经专家验证的Lean证明平均包含22.0个语句和29.6个节点，表明该基准测试涉及大量的形式化和证明复杂性。  
(ii) **高多样性**：如图1 [1 (https://arxiv.org/html/2608.20153#S2.F1)] 所示，**FormalTCS** 涵盖TCS的13个主要研究领域。这种广泛的覆盖使基准测试能够评估LLMs在多样化TCS问题上的研究能力。  

### 2.2 数据格式  
**表2：FormalTCS 的数据字段。**  
**FormalTCS** 的数据格式总结于表2 [2 (https://arxiv.org/html/2608.20153#S2.T2)]。每个实例包含对应端到端TCS研究流程不同阶段的信息，使我们能够诊断当前LLMs在研究流程每个阶段的能力和瓶颈。重要的是，每个实例都附带一个经专家人工验证的严格Lean证明。这种专家验证确保了形式化的正确性和可靠性，从而保证了 **FormalTCS** 的整体质量。我们在附录C [3 (https://arxiv.org/html/2608.20153#A3)] 中提供了 **FormalTCS** 的代表性案例。  

## 3 FormalTCS 的标注  
**图2：FormalTCS 的标注流程。**  
本节描述构建 **FormalTCS** 所使用的标注流程，如图2 [2 (https://arxiv.org/html/2608.20153#S3.F2)] 所示。五位人类专家参与标注过程。每位标注者都在顶级TCS会议上发表过多篇论文，并在该领域拥有丰富的研究经验。鉴于从选定论文中形式化证明的难度很大，我们使用LLM辅助来降低标注成本，同时利用GPT-5.6-sol和Codex保持数据质量。标注过程中使用的提示词见附录B.1 [4 (https://arxiv.org/html/2608.20153#A2.SS1)]，附录A [5 (https://arxiv.org/html/2608.20153#A1)] 报告了标注者的相关信息及额外的标注细节。尽管使用了LLMs作为辅助工具，但所有最终标注都经过人工检查并在必要时进行修订，以确保语义忠实性、类型正确性和简洁表述，而非保留模型引入的风格性痕迹。关于标注者间一致性和人工验证通过率的额外结果见附录E [6 (https://arxiv.org/html/2608.20153#A5)]。  

### 3.1 源论文  
我们的源论文库由2025年和2026年被STOC、FOCS、SODA和COLT收录的论文组成。这一选择旨在确保高研究质量的同时降低基准测试污染的可能性。我们首先使用自动脚本扫描所有接收的论文，并执行初步筛选以确定哪些论文似乎研究TCS问题。然后，人类专家手动检查每篇候选论文，验证其相关性并确定其是否包含合适的核⼼结果及该结果的严格证明。此外，我们进行黑盒审计以评估保留的论文是否可能在模型训练期间被接触过。具体来说，我们在不提供检索访问或论文元数据的情况下查询GPT-5.6-sol和Claude-Opus-5。输入包括部分定理陈述、证明的初始片段以及对论文结果的匿名化描述，要求模型重建缺失内容。我们发现两个模型的完成相似度均低于9.6%，表明所选数据的污染风险相对较低。详细的黑盒审计讨论见附录G [7 (https://arxiv.org/html/2608.20153#A7)]。  

### 3.2 核心陈述  
对于每篇保留的论文，人类专家为其核心理论结果之一撰写简明摘要。摘要必须少于36个单词，并应尽量避免使用不必要的数学符号，以使生成的陈述既紧凑又无需额外上下文即可理解。当同一篇论文的多个陈述都可合理地作为核心陈述时，标注者选择最能代表论文核心贡献的那个。这一标准反映了 **FormalTCS** 的主要目标：评估LLM能否从给定的核心陈述中恢复相关定理及其证明，而不是模型能否识别论文中哪个结果最重要。对于每篇论文，两位专家独立撰写候选核心陈述。然后第三位专家比较两个候选，选择更强的表述作为最终标注。  

### 3.3 自然语言陈述  
接下来，我们构建与所选核心陈述相关的源论文定理对应的自然语言陈述。如果原始定理独立于周围论文即可理解，即其陈述包含所有必要的假设和定义，我们直接保留该定理陈述作为其非正式版本。如果定理依赖于论文其他地方引入的定义或假设，人类专家会收集缺失信息，并将定理重写为独立的陈述，同时避免不必要的冗长。每个重写的定理随后由另一位专家审查，以确保其独立性，并且其假设和定义忠实于源论文。  

### 3.4 形式语言定理和证明  
在此步骤中，我们为每个实例构建待证明的形式定理及其对应的Lean证明，为评估LLMs的TCS证明能力提供可靠基础。遵循先前工作[12 (https://arxiv.org/html/2608.20153#bib.bib22); 35 (https://arxiv.org/html/2608.20153#bib.bib21)]，我们首先使用LLM结合源论文内容，为选定的核心陈述生成证明蓝图DAG。人类专家随后验证生成的蓝图是否忠实遵循原始论文的证明结构，以及每个节点关联的陈述是否与源论文中的相应结果一致。然后，我们根据原始论文中的依赖顺序，调用LLM逐一证明DAG中的节点。每个节点证明后，人类专家检查Lean证明是否严格且忠实于原始论文中的相应论证，并验证是否使用了如 `sorry` 或额外公理等跳过证明的构造。完整的Lean证明构建完成后，另一位专家执行独立的端到端审查并修复任何剩余问题。最终验证的产物作为形式语言证明。最后，我们从此证明中提取目标定理以及陈述它所需的定义闭包，并替换定理陈述中的证明主体。