💻 computer science

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

本文提出了 FormalScience，一个面向科学领域的领域无关、人机协同智能体流水线，通过在 Lean4 中进行智能体代码生成，实现了将非正式科学推理（如物理学）高效、低成本地转化为语法正确且语义对齐的正式证明，并构建了包含 200 个大学水平物理问题的 FormalPhysics 数据集用于评估。

原作者： Jordan Meadows, Lan Zhang, Andre Freitas

发布于 2026-04-28

📖 1 分钟阅读☕ 轻松阅读

CC BY 4.0

原作者： Jordan Meadows, Lan Zhang, Andre Freitas

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

这是一篇关于如何让 AI “读懂”并“严谨证明”科学公式的论文。为了让你轻松理解，我们可以把这个复杂的科研过程想象成一个**“翻译官与数学严谨性”**的故事。

1. 背景：AI 的“翻译”危机

想象一下，你有一本非常牛的物理学笔记，上面写满了各种符号： $\psi$ （波函数）、 $\nabla$ （梯度）、 $\int$ （积分）。这些符号对物理学家来说就像母语一样自然，但对计算机来说，它们就像是**“带有方言的诗歌”**。

目前的 AI（比如 ChatGPT）虽然能读懂这些诗歌，但它在把这些“诗歌”翻译成计算机能理解的“严谨逻辑代码”（我们称之为 Lean 语言）时，经常会出问题。

问题出在哪？

“幻觉”： AI 可能会一本正经地胡说八道，写出看起来很像公式但逻辑根本不通的代码。
“语义漂移”： 这是最严重的。就像你让翻译官把“我心碎了”翻译成德语，结果他为了追求语法正确，翻译成了“我的心脏组织发生了物理性破裂”。虽然语法对了，但情感（物理本质）全丢了。

2. 核心方案：FormalScience —— “带教老师”模式

为了解决这个问题，作者提出了一个叫 FormalScience 的系统。

我们可以把这个系统想象成一个**“学徒培训计划”**：

学徒（AI Agent）： 负责把物理笔记翻译成严谨代码。
导师（人类专家）： 不直接写代码，而是坐在旁边盯着。
纠错机（Lean 编译器）： 这是一个极其严厉的老师，只要代码里有一个标点符号不对，或者逻辑有一丁点漏洞，它就会立刻发出刺耳的警报（报错）。

这个流程是这样的：

初稿： AI 尝试翻译一段物理公式。
自检： 严厉的“纠错机”检查代码，报错了就扔回给 AI 让它改。
导师审核： 代码虽然能运行了，但导师（人类）会看一眼：“嘿，你虽然写对了数学，但你把量子力学的核心逻辑给简化成小学算术了！”
迭代： AI 根据导师的意见再次修改，直到代码既能运行，又完美保留了物理灵魂。

3. 实验成果：FormalPhysics —— 物理界的“标准考卷”

作者用这套方法，亲手制作了一套高质量的“考卷”——FormalPhysics。这套考卷包含了 200 个大学水平的物理问题（量子力学、电磁学等），每一道题都有：

自然语言描述（人类看的题目）
非正式证明（人类写的推导过程）
严谨形式化代码（计算机能验证的逻辑）

通过对比测试，作者发现：现在的 AI 即使能通过考试（代码能运行），但在处理复杂的物理概念（如狄拉克符号、矢量微积分）时，依然会发生**“降维打击”**。

4. 深刻发现：什么是“语义漂移”？（重点！）

这是这篇论文最精彩的部分。作者发现，当 AI 试图把复杂的物理学翻译成计算机代码时，会犯几种“偷懒”的错误：

“降维打击”（Notational Collapse）：
- 比喻： 你让 AI 证明“一个复杂的交响乐团如何演奏”，AI 为了能写出代码，偷偷把交响乐团变成了“几个敲鼓的人”。
- 物理例子： 把复杂的量子算符（不能交换顺序的）变成了普通的复数（可以随便交换顺序的）。代码跑通了，但量子力学的灵魂没了。
“抽象升级”（Abstraction Elevation）：
- 比喻： 你让 AI 证明“如何通过复杂的导航路线到达目的地”，AI 为了省事，直接写了一句“只要一直走就能到”。
- 物理例子： 把复杂的矢量微积分计算，简化成了简单的代数代换。

5. 总结：这篇论文在干什么？

简单来说，这篇论文告诉我们：“让 AI 写出能运行的代码”并不等于“让 AI 理解了科学”。

作者通过建立一套**“人类导师 + AI 学徒 + 严厉编译器”**的协作模式，不仅造出了一套高质量的物理数据集，更重要的是，他为我们指明了 AI 在科学领域进化的方向：我们不仅要追求代码的“正确性”（能运行），更要追求“保真度”（不丢掉物理本质）。

这是一篇关于利用智能体（Agentic）代码生成技术在 Lean4 形式化语言中实现科学领域“人机协同自动形式化”（Human-in-the-Loop Autoformalisation）的研究论文。

以下是该论文的详细技术总结：

1. 问题背景与挑战 (Problem)

**自动形式化（Autoformalisation）**是指将非形式化的数学推理（如 LaTeX）转换为可由形式化系统（如 Lean）验证的代码的过程。目前该领域面临三大核心挑战：

科学领域的特殊性： 物理学等学科包含大量领域特定符号（如狄拉克符号 $\langle \psi | \phi \rangle$ 、矢量微积分 $\nabla$ 等），现代大语言模型（LLM）和现有的形式化库（如 Mathlib）对这些符号的支持不足。
语义漂移（Semantic Drift）： 当 LLM 试图将复杂的物理概念转化为形式化代码时，往往会为了通过编译而牺牲物理含义，导致“形式上正确但物理上错误”的情况。
现有基准测试的局限： 现有的数学形式化数据集（如 miniF2F）多侧重于纯数学，缺乏具有高复杂度、包含大量物理对象和公式的科学推理数据集。

2. 研究方法 (Methodology)

论文提出了两个核心成果：FormalScience 流程和 FormalPhysics 数据集。

A. FormalScience：人机协同智能体流水线

这是一种领域无关的、低成本的半自动形式化流程，分为四个阶段：

非形式化 QA 生成与对齐： 利用 LLM 将原始的数学推导扩展为包含上下文的“问题-解答”对，并由人类专家进行对齐校验。
代码生成与迭代纠错： 采用智能体模式，利用 Lean 编译器（Tool $L$ $L$ ）的错误反馈进行迭代。
- 结构性错误（Syntax/Module）： 触发全量重新生成。
- 语义性错误（Type mismatch/Unsolved goals）： 使用专门的“补丁智能体”（Patch Agent）通过最小化统一差异（Unified Diff）进行局部修复。
形式化语言对齐（关键步骤）： 引入人类专家作为二元分类器。即使代码通过了编译，专家仍需判断其是否保持了原始物理问题的语义。如果不满足，则重新生成。
后处理与最终验证： 确保所有生成的证明在 Lean4 中完全通过验证。

B. FormalPhysics 数据集

利用上述流程构建了一个包含 200 个大学水平物理问题（量子力学、电磁学）的基准数据集，包含：非形式化陈述、LaTeX 推导过程以及对应的 Lean4 形式化证明。

3. 核心贡献 (Key Contributions)

提出了 FormalScience 框架： 一种高效、可扩展且低成本（单专家一个月约 50 美元）的科学领域形式化数据生成方案。
构建了 FormalPhysics 基准： 填补了物理领域形式化验证数据集的空白，其复杂度（对象和公式数量）显著高于现有数学基准。
系统性表征了“语义漂移”： 首次对物理自动形式化中的语义丢失进行了分类学研究，定义了四种漂移模式：
1. 符号坍缩 (Notational Collapse)： 将复杂的算符（如位置/动量算符）简化为标量，导致量子力学特性丢失。
2. 抽象提升 (Abstraction Elevation)： 用抽象代数性质取代具体的矢量微积分运算。
3. 证明策略替换 (Proof Strategy Substitution)： 使用与原推导不同的数学路径完成证明。
4. 隐式前提选择 (Implicit Premise Selection)： 识别并显式化了原推导中未说明的逻辑前提（这是唯一具有正面意义的漂移）。

4. 实验结果 (Results)

性能对比： 实验评估了多种 LLM（如 GPT-5.1, Claude-Opus, Qwen 系列）在三种推理模式下的表现。
- 智能体表现： 采用“智能体代码生成流水线”的开源模型（GPT-OSS-20B）在形式化有效性（FV）上达到了 31%，显著优于零样本或简单的自我修正方法。
- 对齐-有效性权衡： 发现了一个显著的现象——形式化有效性（能否编译）与语义对齐度（是否符合物理）之间存在负相关。模型为了让代码通过编译，往往会采取“符号坍缩”或“抽象提升”等手段。
数据集质量： FormalPhysics 在形式化有效性（FV）上达到了 100%，在复杂度上远超 miniF2F 和 ProofNet。

5. 研究意义 (Significance)

科学验证的自动化： 该研究为实现自动化的科学事实核查、探索和验证提供了技术路径。
指导模型训练： 通过提供高质量、高复杂度的物理形式化数据，可以用于微调专门针对科学领域的数学大模型。
可解释性贡献： 通过对语义漂移的定量分析，揭示了形式化系统在处理非数学领域（如物理）时的局限性，为构建更具“物理感知力”的 AI 系统指明了方向。