📖 AI 总结

Anthropic与Theorem合作的研究表明，大语言模型已能在较大规模上生成形式化证明，使形式化软件验证从过去需要多年专家投入的高门槛工作，转变为可用于真实项目的可行手段。研究使用Claude在RISC-V汇编代码层面为100多个真实开源软件库证明了安全属性，据称这是首次将AI形式化验证大规模应用于生产级汇编代码。验证过程中，Claude还发现了此前经数万亿次测试仍未被检测到的缺陷。文章指出，即便是经过充分测试的成熟软件也普遍存在漏洞，而形式化验证能够提供代码不存在特定违规缺陷的证明。随着模型能力提升，形式化验证有望成为安全软件开发流程的常规组成部分。