FormalScience: Scalable Human-in-the-Loop Autoformalisation of Science with Agentic Code Generation in Lean¶

会议: ACL 2026
arXiv: 2604.23002
代码: https://github.com/jmeadows17/formal-science
领域: 代码智能 / 形式化 / Lean4 / 自动形式化
关键词: 自动形式化, Lean4, 物理形式化, Agent, Human-in-the-loop, 语义漂移

一句话总结¶

FormalScience 提出一个领域无关的人在环 (HITL) Agent 流水线，让单个领域专家在不会 Lean 的情况下，把非正式的科学推理（特别是物理）转写成 100% 编译通过的 Lean4 代码，并构建出首个 200 题大学物理形式化基准 FormalPhysics，系统刻画了「编译通过」但「语义漂移」的现象。

研究背景与动机¶

领域现状：把人类自然语言写的数学推导自动翻译为 Lean / Coq 等定理证明器可编译的形式化代码（autoformalisation），是 LLM × 形式化方法的明星方向。已有的基准（miniF2F、ProofNet、Lean Workbook、Herald 等）几乎全部聚焦在奥林匹克或本科数学，最近虽然有 FormalMath、Herald-Proof 把规模做到几万到几十万级，但域始终是纯数学。

现有痛点：科学领域（特别是物理）的形式化几乎是空白。原因在于：(1) 物理大量使用 Dirac 记号 $\ket{\Psi}$、矢量微积分 $\nabla\times\vec{E}$ 等领域专有符号，而 Lean4/Mathlib 不直接支持；(2) LLM 在分布外、长链推理上幻觉率随复杂度爆炸式增长；(3) 现有 Herald-Proof 等数据集的形式有效率（FV）甚至只有 2%，意味着「自动生成」与「真正能编译」之间存在巨大鸿沟。

核心矛盾：作者通过实验发现一个核心 trade-off — 形式有效性 (FV) 和 语义对齐 (FQ/LP/MC) 之间几乎正交（Spearman 系数 ≈ 0，$p>0.9$）。换言之，专门为 compile 优化的小模型（如 Kimina-7B 拿到 51.5% FV）会通过"凑出能编译的代码"来作弊，语义却完全跑偏；而对齐分高的大模型 GPT-5.1 在 zero-shot 下 FV 只有 14.5%。

本文目标：(i) 设计一个低成本（单人 / 1 月 / 50 美元）就能产出 100% FV 形式化数据集的人在环 pipeline；(ii) 给出物理领域第一个高质量基准 FormalPhysics；(iii) 系统刻画「编译通过但语义漂移」这一现象，回答「Lean 到底验证了什么」这个 epistemic 问题。

切入角度：作者把人类专家定位为与编译器 $\mathcal{L}$ 同构的二元分类器 $\mathcal{H}\in\{0,1\}$ — 既然 LLM 单独搞不定语义对齐，那就让专家在"对齐"这一关充当一个轻量级 oracle，但不要求专家会写 Lean，只判断"形式化代码对不对得上原始陈述"。

核心 idea：把自动形式化分解为「语句生成 + 形式化代码生成 + 编译纠错 + 专家对齐校验」四个嵌套循环，编译循环由 Lean 当 oracle，对齐循环由人当 oracle，两者交替直到收敛。

方法详解¶

整体框架¶

FormalScience 是一个三阶段、双 oracle 嵌套的 pipeline（Alg.1）：

输入：一批非正式证明 $\mathcal{D}$（如 LaTeX 推导）+ 一个少量金标准对 $\mathcal{D}^*=\{(\mathcal{S}_i,\mathcal{P}_i)\}_{i=1}^{N'}$（论文中 $N'=5$）。
阶段 A (in-context 语句重写)：用 few-shot 模板 $T_{fs}$ 让 LLM 把粗糙证明 $d$ 重写成与 $\mathcal{D}^*$ 风格对齐的 $(S,P)$ 对，得到中间数据 $X=\sum_{d\in\mathcal{D}} S\big(\mathcal{M}(T_{fs}(d,\mathcal{D}^*);P_a)\big)$。
阶段 B (编译纠错循环 $\mathcal{R}$)：用模板 $T_g$ 生成初始 Lean 代码 $C^{(0)}=\mathcal{M}'(T_g(x))$，定义 Lean compiler 工具 $\mathcal{L}(C)=(0,\varepsilon)$ 若编译通过、$(1,e)$ 否则返回错误 $e$；迭代 $C^{(t+1)}=\mathcal{M}'(T_c(x,C^{(t)},e))$ 直到 $t^*=\min\{t:\mathcal{L}(C^{(t)})=(0,\varepsilon)\}$。
阶段 C (专家对齐循环)：专家以二元分类器身份判断 $\mathcal{H}^{(k)}=\mathcal{H}(\mathcal{M}'(T_g(x),C^{(k)}))\in\{0,1\}$，若不对齐 ($\mathcal{H}=1$) 就在 prompt $P_g$ 引导下再生成一版并嵌套调用 $\mathcal{R}$ 重新编译；patience $\mathcal{P}$ 控制最大轮数。
输出：三元组 $(S,P,C)$，其中 $C$ 是 100% Lean4 可编译代码。最终对所有 $C$ 再过一次 $\mathcal{L}$，对失败样本再走一遍 Eq.3-5。

关键设计¶

双 oracle 嵌套循环（编译 oracle + 人 oracle）:
- 功能：把"语法正确"和"语义对齐"这两个本质上不同的目标用两个 oracle 解耦。
- 核心思路：内圈 $\mathcal{R}$ 用 Lean compiler 当严格 oracle 反复修代码到能编译；外圈让物理专家以 $\{0,1\}$ 二元分类器身份只判断对齐，完全不需要专家会写 Lean，但可以借助 LLM 生成的对齐自评 $\mathcal{M}'(T_g(x), C^{(k)})$ 作为辅助阅读材料。两层嵌套保证了每次"对齐修订"都会再过一遍编译循环，防止人为修正打破语法。
- 设计动机：作者发现 LP/MC 这类语义指标与 FV 几乎正交（$\rho\approx 0$），单 oracle 无法同时把两个轴拉高；用 LLM-as-judge 当外圈又会陷入"模型骗模型"。专家做二元判断比逐行改 Lean 成本低数个数量级 — 整套 FormalPhysics 由一位物理博士 1 个月 / 50 美元做完。
few-shot 模板 + 金标准对齐 $T_{fs}(d,\mathcal{D}^*)$:
- 功能：把杂乱的原始 LaTeX 证明 $d$ 重写成结构、粒度与 $\mathcal{D}^*$ 一致的 $(S,P)$ 对，作为后续形式化的输入。
- 核心思路：用 in-context learning 让 LLM 学习金标准 $\mathcal{D}^*$ 的"粒度规约"（哪些步骤要细化、哪些 textual context 要补），后处理函数 $S$ 再把多题 batch 输出拆成单独的 statement-proof 对。这一步等价于一次「informal-to-informal refactor」，但用了固定 prompt $P_a$ 让专家在此处也介入校验。
- 设计动机：物理证明常常省略很多步骤（如"利用对称性可得"），而 Lean 形式化要求每一步都显式。先把信号-噪声比拉高，再去做 informal → formal 翻译，能显著降低后续编译循环的迭代次数。
Agent 基线中的结构错误 vs 语义错误分流:
- 功能：在第三类（agentic）baseline 中，把 Lean 编译错误分成两类、走不同补救路径。
- 核心思路：基于 smolagents 的 CodeAgent 框架（ReAct 循环），先用 surface guard 拒绝包含 forbidden token / 未完成证明 / 不合规 import 的代码；编译失败时根据错误分类：结构错误（syntax、unknown identifier、缺 module）触发整段重写并按错误类型加 hint；语义错误（type mismatch、unsolved goals）由 patch agent 输出最小 unified diff 做局部修补。最多 25 轮 ReAct cycle。
- 设计动机：作者发现 7B 小模型（如 DeepSeek-Prover-7B）甚至会因为加了错误反馈而 FV 下降（13% → 4.5%），说明它们没有从错误信号中学习的基本能力；大模型则受益于细粒度的错误分流。GPT-OSS-20B 在这套 agentic pipeline 下 FV 从 4.5% 飙到 31%（zero-shot → agentic），但仍远不如带人的 FormalScience（100% FV）。

损失函数 / 训练策略¶

本文不训练模型，只做 inference-time pipeline 设计。所有 LLM 调用都用现成模型：FormalPhysics 数据构建用 GPT-5.1 + Claude-Opus-4.5；基线评测覆盖 Qwen2.5-Coder-7B、DeepSeek-Prover-V2-7B、Kimina-Autoformalizer-7B、GPT-OSS-20B、Qwen3-Sonnet-14B（Claude-Sonnet-4.5 蒸馏到 Qwen3-14B）、Qwen3-Coder-30B、GPT-5.1。LLM-as-judge 用 GPT-4.1-mini（temperature 0.2），并用 Qwen2.5-Coder-7B-Instruct 做 ≈ 6000 对二判 inter-judge agreement。

实验关键数据¶

主实验¶

不同 pipeline 在 FormalPhysics 上的语句形式化分数（GPT-4.1-mini 当 judge）：

方法	模型	FV (%)	FQ (%)	LP (%)	MC (%)
Zero-Shot	Kimina-7B	51.5	6.5	10.5	9.5
Zero-Shot	GPT-OSS-20B	4.5	68.5	73.0	72.5
Zero-Shot	GPT-5.1	14.5	79.5	76.5	77.0
Self-Refine	GPT-5.1	17.0	82.5	82.0	82.0
Agentic	Qwen3-Sonnet-14B	52.0	1.0	10.5	6.5
Agentic	GPT-OSS-20B	31.0	73.0	72.5	73.0
FormalScience (ours)	GPT-5.1 + Claude-4.5	100.0	73.5	72.0	72.5

FormalPhysics 与现有 Lean4 基准的统计对比（200 样本随机抽样）：

数据集	Objects	Formulae	FV (%)	LP (%)	MC (%)
miniF2F	3.14 ± 1.55	3.21 ± 1.53	88.0	92.0	92.0
ProofNet	3.67 ± 1.48	3.62 ± 1.52	95.5	77.5	77.5
FormalMATH	4.47 ± 2.45	4.53 ± 2.62	97.5	98.0	96.5
Herald-Proof	6.57 ± 2.32	6.42 ± 2.37	2.0	94.5	94.0
FormalPhysics	6.41 ± 2.34	6.22 ± 2.13	100.0	72.0	72.5

消融实验¶

按 pipeline 复杂度递增的消融（GPT-OSS-20B）：

配置	FV (%)	FQ (%)	LP (%)	MC (%)	说明
Zero-shot	4.5	68.5	73.0	72.5	只 prompt，无反馈
+ Self-refine	7.5	70.5	77.0	79.0	加编译错误反馈，FV 涨 3pp
+ Agentic (ReAct + diff)	31.0	73.0	72.5	73.0	加结构/语义错误分流，FV +26.5pp
+ Human (FormalScience)	100.0	73.5	72.0	72.5	再加人对齐 oracle，FV → 满分

关键发现¶

FV 与语义对齐几乎正交：FV 与 FQ/LP/MC 均值的 Spearman、Pearson 系数都接近 0（$p>0.9$），证明 trade-off 是结构性的而非个例。Kimina-7B 是极端案例 — 用 compile shortcut 拿 51.5% FV 但 FQ 只有 6.5%。
Self-refinement 几乎免费午餐失败：加 2× token 成本换来的 FV / 对齐提升 < 3pp，但在独立 7B judge 下 GPT-5.1 能涨 +9pp，指标对 judge 选择敏感。
Agentic 大幅缩小 FV 差距：GPT-OSS-20B 从 4.5% 飙到 31%，且对齐分基本不掉，说明 ReAct + 结构/语义错误分流确实能让中型开源模型把 Lean 当工具用。
「自动形式化是一种 emergent 能力」：14B、30B 不一定比 7B 强，关键在 参数量 × 神经-符号集成 × test-time scaling 三者同时到位；GPT-5.1 单独 zero-shot 只有 15% FV，进 FormalScience 直接到 100%。
物理比奥赛更难：FormalPhysics 的 Objects/Formulae 比 miniF2F、ProofNet、Lean Workbook 多约 2 倍，与 Herald-Proof 同级，但 Herald-Proof 的 FV 只有 2%，FormalScience 的 100% 是断崖式领先。

亮点与洞察¶

把人当 oracle 用，不当 annotator 用：传统 HITL 让人写代码或改 label，本文只让人做"对齐 yes/no" 的二元判断，把人当成廉价 oracle 嵌进算法循环中，这种「人=轻量分类器」的抽象方式可以迁移到任何需要语义判断的任务（如 RLHF 偏好标注、code review）。
首次定量刻画"编译通过 ≠ 语义对齐"：作者引入 Notational Collapse、Abstraction Elevation 等漂移分类，明确指出当 $\ket{\Psi}$ 被 Lean 当成复标量 $\Psi$ 时，Lean 验证的根本不是量子力学。这种"形式系统验证了什么"的元问题以前没人正面回答。
Trade-off 的存在性比方法本身更有价值：FV 与对齐的 $\rho\approx 0$ 这一发现本身就是一个领域级别的负面结果，对未来设计 reward / loss 有指导意义 — 不能再用单一 compile pass rate 当 RL reward。
可扩展性论证：单专家 1 月 / 50 美元 / 200 题 ≈ $0.25/题，意味着一个 10 人专家组可以在同等时间产出 2000 题，对 fine-tune 物理形式化模型来说是切实可行的。

局限与展望¶

作者承认：(1) FormalPhysics 只 200 题，做 fine-tune 基准还不够大，定位是 evaluation set；(2) 物理只覆盖量子力学 + 电磁学两个子域，未覆盖广义相对论、统计力学；(3) Lean4 / Mathlib 对矢量微积分和 Dirac 记号无原生支持，导致 LP/MC 注定低（72%），不是 pipeline 的锅而是 Mathlib 的锅。
隐藏的扩展性瓶颈：所谓"人当二元 oracle"听上去廉价，但实际上专家要先看懂 Lean 代码才能判断对齐，门槛比想象中高；论文没汇报每题平均要多少次 human-in-the-loop 迭代和单次判断耗时。
judge 依赖：GPT-4.1-mini 与 Qwen2.5-7B 两个 judge 的 phi 系数只有 0.28-0.37，绝对分数能差 9pp，说明 LLM-as-judge 给的对齐分数仍有较大噪声，本文的"alignment 不变"结论需要谨慎对待。
改进思路：(1) 在 Mathlib 中先建一套 Dirac/矢量微积分 DSL，能从根本上抬高 LP/MC 天花板；(2) 把外圈"人 oracle"换成 fine-tune 过的对齐验证器，朝全自动 FormalScience-v2 迭代；(3) 把漂移分类（Notational Collapse 等）作为 RL reward 的负项，让模型主动避免低质量编译通过。

评分¶

新颖性: ⭐⭐⭐⭐ 双 oracle + 物理域 + 漂移分类的组合很新，但单看 HITL 形式化本身不算革命。
实验充分度: ⭐⭐⭐⭐ 跨 3 类 pipeline × 7 模型 × 2 judge 全套跑完，inter-judge agreement 也做了。
写作质量: ⭐⭐⭐⭐ 公式编号清晰，Alg.1 / Alg.2 给出完整伪代码，漂移分类配图直观。
价值: ⭐⭐⭐⭐⭐ 推开了"科学形式化"这扇门，给社区一个高质量物理基准 + 一个明确的 trade-off 负面结果。