FormalScience：借助Lean智能体代码生成实现可扩展的人机协同科学自动形式化

将非形式化的数学推理形式化为可形式化验证的代码，对大语言模型而言是一项重大挑战。在物理等科学领域，领域专用的工具体系（如Dirac记号、向量微积分）带来了额外的形式化挑战，现代LLM与智能体方法尚未应对。为辅助科学领域的自动形式化，我们提出FormalScience：一个领域无关的人机协同（human-in-the-loop）智能体流水线，使单个领域专家（无需深厚的形式语言经验）能够以低经济成本产出语法正确且语义对齐的非形式化推理形式证明。将FormalScience应用于物理，我们构建了FormalPhysics，一个包含200道大学水平（LaTeX）物理题及解答（以量子力学与电磁学为主）的数据集，并附有它们的Lean4形式表示。与既有形式数学基准相比，FormalPhysics实现了完美的形式有效性，且陈述复杂度更高。我们通过零样本提示、带错误反馈的自我精炼以及一种新颖的多阶段智能体方法，在本数据集的陈述自动形式化任务上评估开源模型与专有系统，并探索现代基于LLM的方法在自动形式化上的局限。我们首次系统刻画了物理自动形式化中的语义漂移，提出记号坍缩与抽象抬升等概念，揭示了当完全语义保留不可得时形式语言所验证的究竟是什么。我们发布了代码库以及基于交互式UI的FormalScience系统，以促进物理学之外科学领域的自动形式化与定理证明。https://github.com/jmeadows17/formal-science