但一个更棘手的问题是：这些代码，真的对吗？当自动生成的代码规模迅速膨胀，一个幽灵般的挑战始终挥之不去：代码能跑，但逻辑深处的 bug 多到令人头皮发麻。 对于大语言模型（LLM）来说，写出语法正确的“砖块”轻而易举，但距离用这些砖块搭建一座安全稳固的“摩天大楼”仍有显著的差距。因此，如何更好地保障大规模代码的正确性，正成为一个日益重要的问题。 在 Anthropic、NVIDIA 等用顶尖编程智能体生成的多个大规模系统（单个系统规模高达 14.3 万行）中，FM-Agent 成功找到了 522 个隐藏 bug。值得关注的是，这些 bug 经过单元测试、差分测试、多智能体交叉审查等手段都未能发现。 论文作者包括上海交通大学 IPADS 团队的陈海波教授、王肇国教授和丁浩然博士。目前，研究团队已推出 FM-Agent 源码和网站[2,3]，提供 FM-Agent 在线服务，用户提供代码压缩包、API Key 和模型名称后即可开始验证。 那么，FM-Agent 是如何将形式化方法用于大规模系统的？要理解这个问题，我们得先回溯到图灵奖得主托尼·霍尔（Tony Hoare）早在 20 世纪 60 年代为代码验证指明的方向——组合式推理（Compositional Reasoning）。 组合式推理的基本思想非常优雅：为了验证复杂系统的正确性，首先把它拆解成一个个独立的小函数。然后，给每个函数写一份精确的形式化规约（Formal Specification），即一份用数学语言写成的“说明书”，说明执行函数前程序状态需要满足什么条件（前置条件），执行后函数保证输出什么样的结果（后置条件）。最后，只要分别证明每个函数的实现（Implementation）和规约一致，就能直接推理出整个系统满足正确性。 尽管组合式推理的愿景很美好，但一个关键的现实问题是，形式化规约需要靠人类专家用极其严谨的数学公式手写，人力成本高昂。在 LLM 生成代码的时代，迅速放大了这个痛点。 陈海波对 DeepTech 表示：“当编程智能体可以生成 10 万行以上代码时，开发者对内部的函数行为本就一知半解，为成百上千个函数编写形式化规约更不可行。因此，尽管相关工作在自动生成证明方面取得了长足的进步，但是从本质上来看形式化方法仍然是‘屠龙之术’，难以推广至大规模系统软件。” 此前，也有研究工作测验考试用 LLM 自动生成规约，但却掉入了“将错就错”的陷阱：通过分析函数本身的实现来反推规约。但如果函数实现本身就有 bug，那么反推出来的规约也容易被误导。 这就像是鹦鹉学舌（复述函数的工作流程），把 bug 当成正确行为写进去，会直接导致后续的验证无法发现 bug。关键在于，函数本身可能不可靠，但调用它的上下文往往更接近真实需求。 为了解决这一问题，FM-Agent 提出了新方法：既然函数自己的实现可能会骗人，那就去问函数的“上级”——那些调用它的函数。下图展示了调用者驱动的规约自动生成方法，基本思想是结合函数实现、调用者期望和领域背景知识，让 LLM 为函数生成规约。 王肇国对 DeepTech 解释：这就像是甲方（调用方）交给乙方（被调用函数）一个任务，要求输入合格的材料（前置条件），必须交付合格的产品（后置条件）。哪怕乙方在内部施工时偷工减料、走了弯路（bug），甲方对这份工作的原始要求依然是清晰且正确的。 从本质来看，FM-Agent 做了两件事：一是重新定义规约的来源，二是用 LLM 完成推理过程。FM-Agent 就是那个拿着甲方原始合同，去验收乙方成果的质检员。 如下图所示，FM-Agent 提出了一种创新的自上而下规约生成范式：从用户对系统整体正确行为的期望出发，逐步推导出每个函数应满足的规约。这样做可以避免被具体实现误导，生成的规约描述的是函数“应该做什么”，而不是“怎么做”。 在推理过程的可靠性方面，研究团队并不是直接让 LLM 判断代码是否正确，而是将思维链（Chain of Thought）与霍尔逻辑的推理规则相结合，引导 LLM 逐步推导每个代码块执行后程序状态所满足的性质，最终检查程序状态是否符合“说明书”的要求。 此外，对于可能存在 bug 的函数，LLM 会基于推理过程测验考试生成测试用例来触发 bug，只有成功触发的 bug 才会被最终报告给开发者，进一步提升了 bug 上报的准确性。 那么，如何在绝对严谨与工程可用之间取得平衡呢？FM-Agent 的基本思路是：先分析 LLM 擅长什么，然后将其与传统形式化验证流程进行对照，判断哪些步骤可以适当放宽对“绝对严谨”的要求，从而换取“工程可用”。 这一平衡的关键在于利用 LLM 的两项能力：一是在提供函数调用上下文的前提下，能够理解每个函数的意图；二是在处理较短程序时，能根据输入准确推导输出。它们分别支撑了 FM-Agent 自动生成规约和自动推理程序正确性的能力。 尽管已有规约，但新的问题接踵而至。“用户通常使用自然语言描述系统设计，FM-Agent 生成的规约也是自然语言，而传统形式化验证器只支持基于数学公式的推理，二者存在巨大的语义鸿沟。”丁浩然表示。 针对这一问题，研究团队发现了一个关键事实：LLM 对于小段代码的执行结果预测极其精准。结合 LLM 对代码和自然语言的理解能力，FM-Agent 大胆泛化了霍尔逻辑中的推理规则，让 LLM 直接基于自然语言规约对函数的正确性进行逻辑推理。 如上图所示，FM-Agent 逐段推理代码执行后的程序状态描述（注释部分），即后置条件，一直推理到函数返回，检查最终的程序状态描述是否违背了规约里对最终程序状态的要求。 这些系统此前已经过开发者的单元测试、集成测试、差分测试甚至多智能体交叉代码审查等。然而，FM-Agent 在这些“层层设防”的坚固堡垒中，依然挖出了 522 个新 bug。 除了导致系统崩溃、结果错误这种显性问题，FM-Agent 还发现一些更深层的逻辑隐患。例如，编译器 CCC 中发现的一些 bug 会导致代码虽然可以正常编译，但是代码的执行结果却是错的。这种“无声无息”的 bug 不会导致系统崩溃或任何明显异常，但危害极大且难以被发觉。 当前编程智能体之所以会引入这种“细思极恐”型 bug，很可能与其训练数据中包含了类似的错误代码有关。陈海波指出，未来若想进一步提升编程智能体生成代码的可靠性，一个关键方向是对训练数据进行更严格的筛选，尽可能使用正确无误的代码来训练智能体，这或许也是未来 FM-Agent 的应用场景之一。 此外，FM-Agent 还会基于推理过程提供的信息，自动生成能触发 bug 的测试用例。例如对于编译器 CCC，FM-Agent 会生成 C 程序作为测试用例，并将 CCC 的编译结果与参考实现（例如 GCC）比较。“这种可复现的证据链，对于辅助理解和修复 bug 非常重要。”王肇国表示。 在 LLM 时代，如何让形式化方法的脚步快速跟上编程智能体的发展速度变得越发重要。FM-Agent 并非追求传统形式化验证那种绝对完美的数学证明，而是利用 LLM 的推理能力在绝对严谨与工程可用之间找到一个绝佳平衡点。 随着 FM-Agent 这类技术成熟，未来的软件工程范式可能会发生根本性变化。人类开发者的核心工作流有可能会变为：首先由人用自然语言对整个系统编写设计文档，之后由 AI 根据设计文档生成代码，然后 AI 对代码找 bug 并自动修复。 人将从“编写-调试-修复”的循环中解放出来，转移到需求分析与系统设计上，设计文档的质量直接决定了 AI 生成代码的准确性和可维护性。 新的软件开发流程可能给软件工程的教育和人才培养领域带来颠覆性的改变。当前的培养课程重点是编程语言、数据结构、算法实现、调试技巧等，在“AI 生成+验证”的范式下，这些传统能力大部分可能不再是核心的培养目标。因此，抽象建模能力、领域知识深度、系统思维、思辨能力等将变得越来越重要。 研究团队认为，随着形式化方法的不断进步，形式化验证的下一个“圣杯”是贯穿软硬件全栈的端到端保证。这涉及多个大规模系统的正确性保障，而操作系统内核正是全栈中的关键一环。完全自动化的操作系统内核验证，可以视作通往软硬件全栈端到端保证的重要里程碑。 在 20 世纪 60 年代，托尼·霍尔提出了今天形式化验证的重要基石——霍尔逻辑，然而直到他今年逝世前，形式化验证仍然囿于人力成本，难以扩展至大规模软件中。 FM-Agent 提出了首个面向大规模系统的全自动组合式推理框架，回应了这份夙愿，也为形式化方法卸下“屠龙术”的沉重铠甲，大步走向千行百业开辟了一条全新的道路。当 AI 负责写代码，另一个 AI 负责证明它是对的，软件工程的核心问题，正在被重新定义。