AI加速形式化验证：斯坦福研究半日五百美元完成专家五月工程

据WIRED报道，斯坦福研究者孙楚悦等开发的人工智能工具，以不到半天、不足500美元完成三项高技能专家手工需五个月的工程，相关论文结果正重新点燃形式化验证这一用数学证明软件无缺陷的冷门领域。企业虽已大量测试找漏洞，却很少支付更耗时的形式化验证。一批创业公司押注生成式AI能让验证变得实用甚至必要：孙楚悦八月加入并于周四公开启动的&Truth已融资7000万美元，目标最终验证任意编程语言，其研究曾用AI验证Signal加密会话相关部分代码；由Robinhood首席执行官弗拉德·滕内夫联合创办、融资2.95亿美元的Harmonic本周称其数学向AI代理Aristotle可验证C语言软件与Verilog硬件设计，并与潜在用户（含芯片商Tensordyne与英伟达）评估。上周Anthropic与Theorem宣布用AI协助发现开源软件中万亿次测试未检出的缺陷，并推出Claude附加组件。Antithesis创始人威尔·威尔逊称形式化验证对数学爱好者是「陷阱」，自家仍用其他手段挖出更多错误；维塔利克·布特林亦称其非万灵药，但仍视为对抗AI网络攻击的重要防线。波音、亚马逊与逾25亿台活跃苹果设备已含部分形式化验证代码。