FORMALTCS

Name: FORMALTCS
Creator: 哈尔滨工业大学
Published: 2026-08-20T23:13:41+08:00

arXiv2026-08-20 更新2026-08-22 收录

LLM形式化定理证明

理论计算机科学推理评估

数据链接：

https://github.com/zirui-HIT/FormalTCS 数据链接链接失效反馈

官方服务：

资源简介：

FORMALTCS 是由哈尔滨工业大学构建的专家验证基准数据集，旨在评估大语言模型在前沿理论计算机科学（TCS）研究中的端到端能力。该数据集包含175个实例，每个实例源自2025-2026年STOC、FOCS、SODA和COLT会议录用的论文，涵盖13个TCS研究领域，平均每个实例的Lean证明包含22条语句。数据集通过人工专家与LLM协作的方式构建，从原始论文中提取核心主张、自然语言定理与证明、形式化定理与Lean证明，并经过多轮人工审核确保正确性。FORMALTCS主要用于诊断LLM在TCS研究全流程（包括定理提炼、自动形式化、证明生成等阶段）的能力瓶颈，特别是揭示当前模型在数学建模和形式化转化方面的核心短板。

FORMALTCS is an expert-validated benchmark dataset developed by Harbin Institute of Technology, designed to evaluate the end-to-end capabilities of large language models (LLMs) in cutting-edge theoretical computer science (TCS) research. This dataset includes 175 instances, each sourced from papers accepted at the 2025–2026 STOC, FOCS, SODA, and COLT conferences, spanning 13 TCS research domains. On average, each instance's Lean proof contains 22 statements. The dataset is constructed through collaboration between human experts and LLMs: core claims, natural language theorems and their proofs, formalized theorems, and Lean proofs are extracted from original papers, and multiple rounds of manual reviews are conducted to ensure correctness. FORMALTCS is primarily used to diagnose the capability bottlenecks of LLMs across the entire workflow of TCS research, including stages such as theorem extraction, automated formalization, proof generation and other relevant phases, and specifically to uncover the core shortcomings of current models in mathematical modeling and formalization transformation.

提供机构：

哈尔滨工业大学

创建时间：

2026-08-20

原始信息汇总

数据集概述

基本信息

数据集名称：FormalTCS Benchmark
数据集地址：https://github.com/zirui-HIT/FormalTCS
核心内容：包含 175 个来自理论计算机科学论文的核心定理的 Lean 4 形式化基准测试集，以及用于评估前沿模型和代理循环的评估框架。每项数据都包含自然语言描述和基于 Mathlib 的已验证 Lean 4 形式化证明。

数据构成

数据集包含两类条目：

100 个证明条目（collection.json）：提供参考 Lean 证明。
75 个陈述条目（statements.json）：仅提供形式化陈述，无参考证明。

每个条目以独立的 Lake 项目形式组织，存放于 benchmark/theorems/ 和 benchmark/proofs/ 目录下，每个项目包含定理文件（以 by sorry 占位）、Lake 配置及依赖清单。

四个评估任务

任务名称	输入	输出	评估指标
定理引出 (CC2NC)	核心主张	自然语言主张	LLM-Rubric
自动形式化 (NC2FT)	自然语言主张	形式化定理	BEq+
证明引出 (C2NP)	自然语言主张，形式化定理	自然语言证明	LLM-Rubric
定理证明 (FT2FP)	形式化定理	形式化证明	Pass@1

技术环境

Python 版本：≥ 3.10
Lean 工具链：leanprover/lean4:v4.32.2，需安装 elan
Mathlib 依赖：所有项目共享一个预构建的 Mathlib，固定在 905b95818eb32af7874a58b427f50c1711a5e96c 提交版本
沙箱工具：bwrap（bubblewrap）、git
模型驱动：支持 Codex、Claude Code 和 dsh 三种命令行工具

评估框架 (`evaluate/`)

支持运行、评分、状态查询、用量统计和结果报告等操作
包含可恢复的会话机制，中断后可继续
评分方式：
- LLM-Rubric：按逻辑性(0.4)、完整性(0.3)、正确性(0.2)、清晰性(0.1)加权评分
- BEq+：在单个 Lean 命令中证明候选陈述与参考陈述等价
- FT2FP：严格编译、环境级公理审计和内核重放三重验证

自动研究模块 (`auto_research/`)

采用“规划器 → 形式化器 → 评判器”的三代理循环结构：

规划器：提出研究目标
形式化器：将目标编译为 Lean 陈述（最多三轮编译器反馈）
评判器：将形式化陈述翻译回自然语言并过滤新颖性
接受的主张发布到 auto_research/results/，随后按 FT2FP 流程进行证明

搜集汇总

数据集介绍

构建方式

FORMALTCS基准数据集源于2025至2026年间发表于STOC、FOCS、SODA及COLT四大顶会的175篇论文，每篇遴选一个核心理论贡献作为实例。构建过程由五位具有顶会发表经验的专家主导，辅以GPT-5.6-sol等模型提升效率。每个实例历经多阶段标注：先提炼不超过36词的核心主张，再由专家撰写自包含的自然语言定理陈述及其证明草图。采用Lean 4.32.2与Mathlib形式化，通过蓝图DAG分解证明结构，逐节点生成并人工验证形式化定理与证明，确保无sorry等规避手段。所有标注经独立专家复核及交叉验证，保证语义忠实与类型正确。

特点

FORMALTCS具备显著的前沿性与研究现实性。其数据源自最新会议论文，经黑盒审计证实污染风险极低，能真实评估模型对新兴理论问题的推理能力。基准覆盖13个理论计算机子领域，实例难度高，平均形式化证明含22条语句与29.6个节点。尤为独特的是，数据集完整保留了论文特有的定义、假设与多层证明依赖，避免了传统基准的简化处理。此外，每个实例提供从自然语言核心主张到Lean证明的完整信息链，支持对研究流程的细粒度诊断，为探索大模型在端到端理论计算机科学研究中的能力边界提供了可靠工具。

使用方法

FORMALTCS设计了四个递进任务以解耦研究流程：核心主张到自然语言定理的提炼（CC2NC）、自然语言定理到形式化陈述的自动形式化（NC2FT）、基于非形式证明生成策略（C2NP），以及从形式化定理构造Lean证明（FT2FP）。各任务采用人工标注输入独立评估，避免错误传播。评估指标因任务而异，自然语言任务使用LLM-Rubric，形式化任务采用BEq+双向定理证明，定理证明则用Pass@k并强制禁用sorry。基准还可驱动多智能体研究框架，用于自动生成与筛选新理论主张，探索模型的研究品味。

背景与挑战

背景概述

FORMALTCS数据集由哈尔滨工业大学的研究团队于2026年创建，旨在评估大型语言模型在前沿理论计算机科学研究中的端到端能力。该数据集包含175个实例，源自2025至2026年间被STOC、FOCS、SODA和COLT顶级会议接收的论文，覆盖13个主要研究领域，并配备专家验证的Lean形式化证明。其核心研究问题是检验LLM能否从自然语言的核心主张出发，完成从定理提取、自动形式化到形式证明的完整研究流程。FORMALTCS的提出填补了现有基准在管线的完整性、内容的时效性和问题真实性上的空白，为LLM的理论计算机科学研究能力提供了精细化的诊断工具，对推动自动化科研具有重要影响力。

当前挑战

FORMALTCS面临的挑战主要存在于两个层面。首先，在领域问题层面，当前LLM在端到端TCS研究流程中表现不佳，尤其是自动形式化环节成为最突出的瓶颈，最佳模型仅能达到11.5分，远低于人类提供形式化定理后的证明能力（28.6分），这表明模型在将自然语言转化为严谨的数学形式方面的能力严重不足；其次，在构建过程中，研究者需从最新会议论文中提取核心主张并重构自包含的自然语言陈述，同时完成专家验证的Lean形式化证明，这一过程要求高度专业知识，且需应对数据污染风险及证明复杂度的挑战，最终仅6条候选主张通过专家评估，凸显了研究品味与新颖性的生成难题。

常用场景

经典使用场景

FORMALTCS作为面向理论计算机科学前沿研究的大规模语言模型评估基准，其经典用途在于对模型在端到端研究流程中的综合能力进行精细剖析。该基准将研究流程分解为定理激发、自动形式化、证明启发与定理证明四个核心任务，每个任务均对应真实会议论文中的具体问题，并要求模型在保留论文特定定义、假设与证明依赖的条件下完成输出。研究者可借助该基准系统性地诊断模型在从自然语言核心主张到严格Lean证明转换过程中的优势与短板，从而为优化模型架构与训练策略提供可靠依据。

衍生相关工作

基于FORMALTCS衍生出的相关工作主要集中于两个方向：其一是面向端到端自动形式化与证明生成的系统改进，例如借鉴其分阶段评测思路设计蓝图辅助证明生成框架，或利用其专家验证的Lean证明作为训练数据，提升模型在数学建模与定理转换上的表现；其二是研究品味与科研创新能力的探索，该基准的后续研究常围绕如何自动评估生成主张的新颖性与价值展开，催生了结合强化学习与进化搜索的多智能体科研框架的迭代。此外，该数据集也推动了针对前沿会议论文泄露风险检测方法的发展，并促进了理论计算机科学各子领域基准的融合与标准化。

数据集最近研究