Anthropic的Claude现在能自动编写代码并证明其安全性
decoder ·
Anthropic与Theorem合作,展示了其AI模型Claude能够自动生成数学证明,以验证现有软件代码的正确性。在最近的一个项目中,Claude在短短几周内为Google OSS-Fuzz项目的123个开源库生成了约1.8亿行的证明代码。这一自主过程涉及将崩溃测试转化为数学问题并分析编译后的机器码,随后由独立工具Rocq对结果进行核查。在此验证阶段,Claude发现了数百个传统测试方法多年来未能找到的漏洞,包括广泛使用的PDF阅读器中的关键安全缺陷。然而,这些形式化证明存在严格限制,仅适用于特定的处理器架构、单线程程序以及小于64 MB的输入。尽管计算成本仍然高昂,但Anthropic指出,较新的模型正变得更为高效,解决类似证明所需的Token数量更少。该公司旨在使基于AI的形式化验证像标准软件测试一样成为常规流程,从而可能彻底改变开发者对AI生成代码的信任与审查方式。
decoder