编程智能体的隐藏bug，被上交IPADS团队用数学逻辑给揪出来了 (opens in new tab)

从一键生成操作系统内核，到从零手搓一个 C 编译器，编程智能体（Coding Agent）的能力边界正在疯狂扩张。但一个更棘手的问题是：这些代码，真的对吗？当自动生成的代码规模迅速膨胀，一个幽灵般的挑战始终挥之不去：代码能跑，但逻辑深处的 bug 多到令人头皮发麻。对于大语言模型（LLM）来说，写出语法正确的“砖块”轻而易举，但距离用这些砖块搭建一座安全稳固的“摩天大楼”仍有显著的差距。因此，如何更好地保障大规模代码的正确性，正成为一个日益重要的问题。近日，上海交通大学 IPADS 研究团队打造了形式化方法智能体 FM-Agent，首次实现了面向大规模系统的全自动正确性推理。在 Anthropic、NVIDIA 等用顶尖编程智能体生成的多个大规模系统（单个系统规模高达 14.3 万行）中，FM-Agent 成功找到了 522 个隐藏 bug。值得关注的是，这些 bug 经过单元测试、差分测试、多智能体交叉审查等手段都未能发现。图丨相关论文（来源：arXiv）相关论文以《FM-Agent：通过基于大语言模型的霍尔逻辑推理将形式化方法扩展至大规模系统软件》（FM-Agent: Sca...