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

Idea

FormalScience 将科学推导的 autoformalisation 组织为专家可介入的 agentic code generation 流程：先补齐自然语言问题与推导，再用 Lean4 编译反馈修复代码，并分别检查形式有效性与语义对应。由此构建含 200 道大学物理题及证明的 FormalPhysics，供研究科学形式化中的 alignment drift。

Research Problem

科学推导使用 Dirac notation、向量算子及领域隐含假设，不能直接套用以纯数学命题为中心的自动形式化。仅依靠 Lean 编译成功会把符号替换、抽象提升或省略物理关系后的较弱命题当作成功；同时要求领域专家先精通 Lean 又限制数据生产。

Insight

编译器负责证明给定形式命题，领域专家负责该命题是否仍表达原科学问题，两类校验不能互相替代。论文的价值在于把这种分工嵌入迭代流程并量化残余漂移；FormalPhysics 的形式有效率为 100%，而所报告的 logical preservation 和 mathematical consistency 约为 72%，因此并非全部科学语义已被证明。

Method

1. 从已有 informal proofs 和少量 gold statement–proof 示例出发，以 few-shot、多轮提示生成题目并扩展推导细节；专家检查其与原材料及示例标准的对应。
2. 代码 agent 将 statement–proof pair 转为 Lean4/Mathlib，执行编译器，把报错连同当前代码反馈给修复提示，迭代直到编译或预算限制。
3. 随后由 LLM 提供语义 alignment 评估，专家作二元接受或要求改进；改进后的代码再次经历编译修复，人工迭代受 patience 参数约束。
4. 把批量输出拆成独立 statement、proof、code 三元组，重新编译并必要时再次修复与检查，避免拆分破坏依赖。
5. 用 compiler validity、formal quality、logical preservation、mathematical consistency 等指标评估语料，并比较 zero-shot、error-feedback self-refinement 和 multi-stage agent 的形式化表现。