FormalScience：用Lean实现可扩展的人机协同科学自动形式化
将非正式的数学推理自动转化为形式化可验证代码，一直是大型语言模型面临的重大挑战。特别是在物理等科学领域，狄拉克符号、向量微积分等专业工具给形式化带来了额外难度，现有的LLM和智能体方法尚未有效解决。为此，研究者提出了FormalScience——一个与领域无关的人机协同智能体流水线，能让单个领域专家（即使没有深厚的形式化语言经验）以较低的经济成本，生成语法正确且语义对齐的非正式推理形式化证明。
核心创新：FormalPhysics数据集与智能体方法
作为概念验证，团队将FormalScience应用于物理学，构建了FormalPhysics数据集。该数据集包含200道大学水平的LaTeX物理问题与解答（主要涵盖量子力学和电磁学），以及对应的Lean4形式化表示。与现有的形式化数学基准相比，FormalPhysics不仅实现了完美的形式化有效性，而且其语句复杂度更高，更贴近真实科研场景。
研究者在自动形式化任务上评估了多种开源模型和商业系统，测试了零样本提示、带错误反馈的自我修正，以及一种新颖的多阶段智能体方法。结果显示，当前基于LLM的方法在科学形式化上仍存在明显局限。
关键发现：语义漂移的系统性刻画
该工作首次系统性地刻画了物理自动形式化中的语义漂移现象，提出了符号坍缩（notational collapse）和抽象提升（abstraction elevation）等概念。这些概念揭示了当完全语义保真无法实现时，形式化语言究竟验证了什么。例如，符号坍缩指多个非正式符号在形式化中被映射到同一个Lean对象，导致信息丢失；抽象提升则表现为用更一般的数学结构替代特定物理语境，虽然保持语法正确，却改变了原意。
开源与交互式界面
团队已开源完整代码库，并提供了一个交互式UI系统，方便用户在科学领域直接进行自动形式化和定理证明。这一工具降低了形式化验证的门槛，有望推动AI在科学发现中的可信应用。
行业意义
FormalScience的出现，标志着AI形式化从纯数学向跨学科科学迈出了关键一步。它不仅为物理、化学等领域的自动推理提供了可行路径，也为构建可验证的科学知识库奠定了基础。随着LLM能力的提升和智能体方法的成熟，人机协同的形式化有望成为科学研究的标配工具。