令人头疼的数学或能拯救氛围编程

斯坦福研究员Chuyue Sun和她的计算机科学家团队开发出一款AI工具，不到半天、花费不到500美元就完成了一个工程项目，而三位资深专家手工完成同样的工作花了五个月。这一巨大的时间和成本缩减来自Sun近期发表的一篇论文，也是让“形式化验证”这一冷门编程与数学交叉领域重新回到聚光灯下的早期成果之一。几十年来，开发者一直设想用数学方法证明软件没有缺陷，但这个过程漫长而繁琐，需要工程师对软件目标写出精确陈述，并把代码转换成可验证的公式。尽管企业已经在用复杂的测试手段尽可能多地发现软件缺陷，但鲜有公司愿意为形式化验证掏钱，而后者能捕捉到更多异常行为。如今，一批创业公司押注生成式AI将让形式化软件验证既可行又必要。Sun于今年8月加入、周四正式公开亮相的&Truth就是其中之一。Sun的研究通过用AI验证即时通讯应用Signal中部分加密对话代码，展示了这项技术的潜力。 &Truth首席科学官Ilya Sergey打了个比方：“桥梁、建筑不会倒塌，是因为人们在建造之前做了数学计算。为什么代码不这样做？用数学推理的技术一直都有，只是难以规模化。”&Truth已从投资者手中融资7000万美元，目标是最终能验证任何编程语言。竞争对手Harmonic由Robinhood CEO Vlad Tenev联合创办，已获得2.95亿美元融资，本周宣布其数学导向的AI智能体Aristotle支持验证用C语言编写的软件和用Verilog编写的硬件设计，并正在与潜在用户评估这项技术，包括芯片制造商Tensordyne和英伟达——后者的风投部门是该创业公司的投资方之一。就在上周，Anthropic和验证创业公司Theorem联合宣布，他们用AI协助发现了开源软件中的缺陷，而这些缺陷是数万亿次测试都未能检测到的。他们还为Claude推出了一款附加组件，帮助其他开发者进行验证。初始项目的成本未披露。最大的承诺是未来软件运行更可靠、安全问题更少。但AI能否将形式化验证从NASA和苹果等机构最关键的系统推广到广泛使用，仍是未知数。这项技术仍处于原型阶段，需求虽然旺盛，但客户愿意付多少钱、偏好以何种方式采用，尚不清楚。形式化验证依赖于对计算机和人如何与软件交互做出假设，一些专家怀疑它能否捕捉到用户操作失误和硬件故障引发的缺陷。运营缺陷猎杀AI软件创业公司Antithesis的Will Wilson称形式化验证对他这样的数学爱好者来说是个“陷阱”。Antithesis花了几百万美元对其部分网络安全防御进行形式化验证，Wilson形容这个过程“极其折磨人”。然而该公司仍用自己的工具发现了额外错误，Antithesis也在多家客户已形式化验证过的软件中发现了缺陷。Wilson说：“它能给你一些保证，但只有强大的穷举测试才能证明你的保证是真的。”正如创建以太坊的工程师Vitalik Buterin今年早些时候在博客中所写，“形式化验证不是万能药。”但他和其他支持者仍然相信，它将成为防御AI系统发动网络攻击和造成破坏的重要手段。