Theory-Scale Auto-Formalization of Logics for Computer Science¶

会议: NeurIPS 2026
arXiv: 2606.26525
OpenReview: https://openreview.net/forum?id=iKP2FDkWuw
论文: https://arxiv.org/abs/2606.26525
领域: 其他
关键词: 自动形式化, 交互式定理证明, Lean 4, 理论级基准, 形式验证

一句话总结¶

针对现有自动形式化局限于孤立命题翻译且高度依赖成熟数学库的缺陷，本文基于经典教材《Logics for Computer Science》构建了首个从零起步、覆盖85K行Lean 4代码的理论级基准LCS-Bench，并提出基于DefEq的声明等价性判定协议，揭示了前沿大模型在理论级形式化中最高仅达20.1%通过率的严峻瓶颈。

研究背景与动机¶

自动形式化旨在将非形式化的自然语言数学与逻辑文本翻译为可由证明助手机器检查的形式化定义与证明，是大模型辅助形式验证与数学推理的前沿交汇点。然而，现有的自动形式化与神经定理证明评估体系绝大多数局限于孤立命题翻译（如竞赛数学题 MiniF2F、PutnamBench）或简单单步引理生成，或者极度依赖像 Mathlib 这样庞大完备的既有数学库，从而掩盖了大模型从第一性原理构建完整理论系统的真实困难。真实的计算机科学与逻辑理论体系绝非单个定理的堆叠，而是由数百个相互交织、层层依赖的归纳语法定义、推导关系、元理论性质（如可靠性、完备性、切消定理）以及执行算法共同构成的有机整体。

这种理论级构建的核心矛盾在于：孤立命题翻译只需局部语法和类型匹配，而“理论级形式化”（Theory-Scale Auto-Formalization）要求全局上下文的高度自洽、对原著细微语义的严格忠实性，以及长依赖链条下形式定义的可推演性。更关键的是，计算机科学逻辑中普遍存在大量图表规则（如相继式演算推导树）、深嵌入式领域特定语言（DSL）、跨章节的隐含上下文约定以及复杂的变量绑定与替换机制，这些在传统数学分析或代数基准中极少出现。此外，现有评估指标多依赖类型检查（pass@k）或命题层面的逻辑等价判定（BEq+），完全无法精确校验归纳类型、构造子、计算性定义与元定理在类型论中的等价性。

为了打破这种局限，本文选择计算机科学逻辑领域的经典经典专著《Logics for Computer Science: Foundations of Automatic Theorem Proving》（Jean Gallier著）为唯一源文本，构建了完全独立于外部重型库、自底向上的理论级形式化基准。核心 idea：通过融合概念图抽取、形式签名规划、反例驱动排错与专家在环审校的人机协同流水线，将经典逻辑教材完整形式化为85K行Lean 4体系，并基于此派生出五大评测赛道与高保真定义等价性检查器DefEq Checker，开创异构理论级自动形式化评估体系。

方法详解¶

整体框架¶

构建理论级形式化基准需要从教材的非形式化文本出发，产出兼具数学忠实性与机器可验证性的Lean 4代码库，并自动转化为标准评测任务。LCS-Bench的流水线由预处理、形式化规划、Lean代码分轮实现、形式正确性审校四大阶段构成，随后通过确定性数据引擎自动构建出覆盖单项形式化（IAF）、子节形式化（SSAF）、含干扰项形式化（IAF-D）以及声明级/项级定理证明（DTP/ITP）的五大任务赛道。

%%{init: {'flowchart': {'rankSpacing': 24, 'nodeSpacing': 28, 'padding': 6, 'wrappingWidth': 400}}}%%
flowchart TD
    A["教材文本与图表<br/>Gallier 逻辑教材 Markdown"] --> B["阶段1：两层中间表示规划<br/>L1概念图 + L2形式签名图"]
    B --> C["阶段2：分轮递进实现<br/>归纳类型 → 计算函数 → 定理声明"]
    C --> D["阶段3：反例驱动排错与三方审校<br/>LSP策略证明 + 否定反例搜索 + 13类漏洞审查"]
    D --> E["专家干预与闭环重构<br/>修正隐含假设、假基石与空洞定理"]
    E --> F["LCS-Bench Lean Artifact<br/>327项目 / 4,076声明 / 85K行代码"]
    F --> G["阶段4：确定性数据引擎与DefEq检查器<br/>自动化派生5大赛道 + 内核级定义等价性判定"]

关键设计¶

1. 两层中间表示规划：消解异构内容与嵌入层级分歧 教材文本包含语法符号、推导规则、算法步骤与元定理，若让大模型直接从自然语言跳跃到Lean代码，极易产生概念漂移与层级混乱。为此，规划阶段引入了两层中间表示（IR）。第一层为“概念图”（L1），以句子为粒度抽取具体名词短语节点（如“命题公式”、“左括号计数”、“相继式前件”），并通过IS-A、HAS-A、RELIES-ON、DEFINED-BY等关系建立教材自洽的概念依赖网；第二层为“形式签名图”（L2），将概念节点映射到Lean的具体实现范型（inductive、structure、def、theorem等），并明确划分“嵌入层级”（Embedding Level）：对于句法DSL采用深嵌入（归纳类型），对于语义真值采用浅嵌入（Lean的原生Prop层），对于可靠性/完备性等元定理采用混合嵌入。这一划分确保了模型在后续阶段能够把深嵌入语法当作一等公民来陈述元理论。

2. 三轮拓扑递进实现：由浅入深构建严密类型骨架 在代码实现阶段，智能体严格按照签名图的依赖拓扑序，分三轮推进，每轮均通过lake build确保即时编译： - 第1轮（类型骨架）：定义所有归纳类型与核心结构体，通过属性@[lcsitem]绑定教材编号，以@[lcsmain]标记主声明，确立整个理论的形式化词架。 - 第2轮（语义与计算）：在归纳类型之上实现计算函数（求值器、范式转换、搜寻过程）与语义谓词（可满足性、重言式、推演有效性）。 - 第3轮（定理陈述）：严格依据签名图生成所有定理与引理的类型声明，证明体全部以sorry占位，并通过专门的验证器筛除空洞声明（如将恒真式当作结论）、缺失分支以及未使用的无用声明，保证全库在理论尺度上的连贯性与类型自洽。

3. 反例驱动排错与13类漏洞审查机制：防范“假基石”与妥协性证明 在自动化证明与审查阶段，最大陷阱不是证明不出，而是“证明了不忠实于原著的假定理”。当自动化LSP策略搜索（优先级为rfl, decide, omega $\to$ simp, ring $\to$ grind, aesop）陷入停滞时，流水线并不盲目堆砌算力，而是反向尝试寻找反例——即尝试证明该陈述的否定命题 $\exists x, \neg P(x)$。一旦反例构造成功，立即确认形式化定义存在漏洞并打回重构。此外，针对大模型在长期交互中容易对错误基础“打补丁”（Accumulated workarounds）的倾向，项目总结了13类高频保真度漏洞目录（L1–L13，例如L1用存在量词替代显式状态、L4退化的自反性存在谓词、L12隐藏未注明的代数不变量、L13静默添加过强假设等），配合专家设立的强制三方审校门禁，一旦发现底层定义失真，彻底回滚全部依赖下游。

4. 内核级DefEq等价性检查器：跨异构常量的精确判题协议 对于自动形式化的评估，传统的BLEU或编辑距离毫无语义价值，而命题外延性又会导致任意两个真命题在类型论中均等价。为此，项目研发了Check.lean判定器，针对不同常量子类实施差异化等价准则： - 对常规定义（Definition）：通过reduceFully在隔离沙箱中展开内核级全透明归约，比对表达式是否满足可定义等价（ISDEFEQ）或同余闭包（GRIND）。 - 对定理（Theorem）：比对两者的陈述类型，必须满足ISDEFEQ或GRIND等价，严禁仅因命题均可证而判定一致。 - 对归纳类型（Inductive）：验证构造子集合的无序一致性，且对每个对应构造子的类型执行严格的ISDEFEQ检查。该判定器天然具备变量重命名（$\alpha$-等价）鲁棒性，且沙箱化隔离彻底杜绝了模型提交恶意全局实例或重载污染评测环境。

一个完整示例：Gentzen相继式演算中隐含侧条件的修正¶

在形式化第5章相继式演算推导规则（Definition 5.4.1）中的全称量词右引入规则（$\forall\text{:right}$）时，教材将推导规则写为： $$\frac{\Gamma \to \Delta, A[y/x]}{\Gamma \to \Delta, \forall x A}$$ 并在正文段落末尾用散文注明了两项至关重要的侧条件：本征变量条件（$y$ 不在结论相继式的自由变量集中出现，即 $y \notin \text{FV}(\text{conclusion})$）与自由代入条件（$y$ 在 $A$ 中自由可代入 $x$）。初始自动化形式化仅翻译了主规则模式：

| allRight (y : Nat) (Γ Δ Λ : List (FormulaN L)) (x : Nat) (A : FormulaN L) :
    GentzenStep1 (Sequent.mk Γ (Δ ++ [formulaSubstN A (var y) x] ++ Λ))
                 (Sequent.mk Γ (Δ ++ [FormulaN.all x A] ++ Λ))

该规则能够通过Lean编译器检查，但由于缺失侧条件，允许了不健全的逻辑推理（例如推导出 $\forall x P(x) \to P(y)$ 的错误倒置）。在随后的定理证明阶段，模型反复在分支闭合中崩溃。专家介入后定位该漏洞，将其补全为携带显式前置证明项的完整归纳构造子：

| allRight (y : Nat) (Γ Δ Λ : List (FormulaN L)) (x : Nat) (A : FormulaN L)
    (hfresh : ∀ F ∈ (Sequent.mk Γ (Δ ++ [all x A] ++ Λ)).antecedent ++
                    (Sequent.mk Γ (Δ ++ [all x A] ++ Λ)).succedent, y ∉ formulaFVN F)
    (hfreeFor : isFreeForN (var y) x A) :
    GentzenStep1 (Sequent.mk Γ (Δ ++ [formulaSubstN A (var y) x] ++ Λ))
                 (Sequent.mk Γ (Δ ++ [FormulaN.all x A] ++ Λ))

这一真实案例突显了专家在环审校与反例排查在理论级形式化中不可替代的把关作用。

评测数据衍生机制¶

依托构建完成的Lean Artifact，确定性数据引擎自动抽取出5大赛道，共包含1,271个实例： - IAF（项级形式化，327项）：输入单项教材描述、上下文依赖与骨架声明，要求生成对应的一组Lean声明； - SSAF（子节级形式化，116项）：将输入上下文扩充至完整子节，要求同时一致性生成全子节所有定义与引理（平均每项18.2个声明）； - IAF-D（含干扰项形式化，327项）：在IAF上下文中注入50%数量的相关无关声明，测试模型在长上下文下的抗干扰与关键信息检索能力； - DTP / ITP（定理证明，420 / 81项）：将定理证明体替换为sorry，要求在交互预算内填补完整无作弊证明。

实验关键数据¶

主实验：多模型在三大自动形式化赛道上的综合表现¶

评测覆盖14个主流前沿大模型，横跨零样本（Zero-shot）、扩展思考（Thinking）与智能体环境（Agentic）三种模式。在最具代表性的原子赛道 IAF 上，严格通过率普遍处于极低水平，即便是最强的 Claude Opus 4.6 在 Agentic 模式下也仅取得 20.1% 的通过率。

模型	评测模式	IAF 编译率 (%)	IAF 通过率 (%)	SSAF 编译率 (%)	SSAF 通过率 (%)	IAF-D 通过率 (%)
Claude Opus 4.6	Agentic	99.4 ± 0.5	20.1 ± 0.7	96.6	5.2	—
Claude Sonnet 4.6	Agentic	98.5 ± 0.2	18.0 ± 0.5	96.6	3.4	—
GPT-5.4	Agentic	73.4 ± 0.6	16.1 ± 0.4	—	—	—
Kimi K2.5	Agentic	73.3 ± 1.9	15.3 ± 0.9	92.2	3.4	—
GLM-5	Agentic	61.0 ± 1.3	14.7 ± 0.4	96.6	4.3	—
MiniMax-M2.5	Agentic	78.7 ± 1.1	12.1 ± 0.1	85.3	2.6	—
Qwen V3.2	Agentic	29.4	5.5	0.9	0.0	—
GPT-OSS-120B	Agentic	14.4 ± 0.6	2.1 ± 0.3	—	—	—
Claude Opus 4.6	Thinking	77.1 ± 1.7	17.6 ± 0.3	56.9	4.3	16.2
Claude Sonnet 4.6	Thinking	66.9 ± 1.0	17.9 ± 0.8	42.2	2.6	15.6
GPT-5.4	Thinking	73.9 ± 1.0	16.3 ± 0.6	—	—	—
Kimi K2.5	Thinking	53.0 ± 0.4	14.4 ± 0.4	31.9	6.9	11.0
Claude Opus 4.6	Zero-shot	70.5 ± 0.9	16.8 ± 0.5	50.0	2.6	14.1
Claude Sonnet 4.6	Zero-shot	57.4 ± 0.4	15.0 ± 0.3	40.5	5.2	12.8
GPT-5.4	Zero-shot	58.5 ± 1.4	15.4 ± 0.4	—	—	—
GLM-5	Zero-shot	41.0 ± 0.7	13.9 ± 0.6	10.3	0.9	10.7

消融与细粒度特征影响分析¶

研究团队对N=554个基准项目进行了正交的5维度人工特征标注，并在Claude Opus 4.6的6轮聚合实验（N=1,950次试验）上系统测定了各特征对通过率的相对影响差值 $\Delta = r_{\text{with}} - r_{\text{without}}$。

特征维度	特征标签 (Tag)	样本数 (n)	通过率差值 $\Delta$ (pp)	统计显著性	核心归因说明
表层表述	篇幅极短 (`len-short`)	664	+12.5	$p < 0.001$	局部上下文自包含，翻译难度低
	包含图表 (`references-figure`)	131	-16.1	$p < 0.001$	推导树/规则图需跨模态转化为归纳DSL
	非形式记号 (`informal-notation`)	149	-15.9	$p < 0.001$	排版符号无法字面映射，需要符号抽象
	包含具体实例 (`concrete-instance`)	451	-13.6	$p < 0.001$	具象推导案例难于提炼通用类型声明
学科主题	语义真值 (`semantic`)	603	+19.6	$p < 0.001$	解释与可满足性抽象好，与标准数学库契合
	语法机制 (`syntactic`)	1645	-16.4	$p < 0.001$	相继式、推导步等繁重底层设施极易出错
	算法步骤 (`algorithm`)	198	-19.3	$p < 0.001$	程序性证明搜索伪代码形式化为纯函数困难
数学词汇	变量替换与绑定 (`binders-subst`)	674	-12.9	$p < 0.001$	$\alpha$-重命名、自由变量防捕获机制极易缺项
	高阶构造 (`higher-order`)	90	+17.9	$p < 0.001$	高阶函数与谓词抽象更符合现代函数式类型论
定义形态	谓词定义 (`predicate-def`)	281	+12.2	$p < 0.001$	单个`Prop`级归纳关系推导结构简单明晰
	互递归定义 (`mutual-recursion`)	24	-17.5	$p < 0.05$	多个类型相互递归极易触发Lean停机性报错

关键发现¶

理论级扩展带来灾难性断崖：从单项形式化（IAF）扩展到子节级整体形式化（SSAF）时，即使顶级模型在智能体循环下编译成功率高达 96.6%，严格通过率依然骤降至 3%~5%。这证明智能体环境仅能帮助模型修复局部语法与符号拼写错误，却无法协助模型理清跨声明的全局语义一致性。
干扰项显著破坏检索与形式化聚焦：在注入半数无关依赖项的 IAF-D 任务中，所有模型的通过率均无一例外地下跌 1~3 个百分点，表明在真实理论库演化过程中，如何从庞大前置库中精准提取紧凑依赖依然是关键瓶颈。
测试期算力（TTC）边际收益递减与“过度思考”陷阱：在带有扩展思考通道的评测中，错误尝试消耗的推理 Token 数反而是正确尝试的中位数的 4~6 倍。模型在陷入错误时倾向于无止境发散与纠缠，单纯拉长思维链无法弥补对于复杂归纳结构与变量替换规则的理解缺失。
错误类型高度集中于表达式不匹配（NMExpr）：在通过 Lean 编译但未能通过等价检查的代码中，绝大部分错误均为表达式语义不等价（70%~90%），而类型构造子缺失（CMiss）或常量子类错误（NMKind）极罕见，说明模型完全学会了“依葫芦画瓢”生成合法的Lean骨架，但充斥着语义偏离的实质错误。

亮点与洞察¶

跳出Mathlib舒适圈的独立理论级基准：过去形式化研究高度依赖 Mathlib 提供的庞大基座，使得模型退化为“库函数拼凑器”。LCS-Bench 从最底层的归纳数据类型和推导步手工搭建出 85K 行无外力支撑的代码库，确立了衡量从零构建完备领域理论能力的黄金标准。
DefEq 判题协议填补高保真形式化评测空白：以往工作苦于“等价性无法判定”而退化采用不严谨的文本编辑距离或宽松的证明替代，本文设计的内核级沙箱化全展开判题机制（Algorithm 1）不仅兼顾了 $\alpha$-重命名鲁棒性与同余闭包，也为后续复杂软件验证与数学形式化提供了可泛化的自动阅卷基石。
反例驱动与漏洞图谱的工程方法论启示：在形式化复杂系统时，大模型在遭遇瓶颈时极具“自我妥协”倾向，会悄悄弱化前提或构造空洞定理以逃避报错。引入反例搜索与 13 类真实漏洞审查机制，为未来由 LLM 驱动的大规模软件规范形式化给出了严谨的纠偏范式。

局限与展望¶

前沿深层元定理的机器证明缺口：全库中仍有 45% 的定理未能在 Lean 中完全闭合（主要集中于终极切消定理、高阶完备性与复杂停机性证明），目前依赖专家人工保真度审查，未来需引入更先进的神经引导符号推演以实现 100% 机械化验证。
单一教材体系的领域局限：LCS-Bench 局限于经典的计算机科学逻辑专著，尚未覆盖操作系统内核验证、类型系统演进或分布式一致性协议等其他典型软件工程理论领域。
评测闭环与自我演化的计算开销：在全展开沙箱中运行复杂归纳定义的 DefEq 检验消耗显著的内核时间，限制了超大规模实时在线强化学习（RL）的快速评估反馈吞吐。

评分¶

新颖性: ⭐⭐⭐⭐⭐ 首次提出并实现理论级计算机科学逻辑自动形式化基准，提出DefEq检验协议。
严谨度: ⭐⭐⭐⭐⭐ 历经6人月专家审查，建立13类保真度漏洞目录，结合反例搜索杜绝虚假证明。
实验充分度: ⭐⭐⭐⭐⭐ 涵盖14个前沿模型、3种推理模式、5大赛道以及554项的正交特征影响分析。
写作质量: ⭐⭐⭐⭐⭐ 结构清晰严谨，深入剖析形式化过程中的认知盲区与类型论陷阱。
实用价值: ⭐⭐⭐⭐⭐ 为推动大模型进入真实软件验证、深度规范合成与神经定理证明提供了严苛的标尺。