Anthropic发布形式化验证报告

发生了什么

据钛媒体报道，10月23日Anthropic与Theorem Labs团队发布报告《大模型正让形式化软件验证在更大规模上变得可行》。报告称，Claude模型针对123个开源软件库的239个程序入口，生成约1.8亿行Rocq证明代码，并发现修复数百个Bug。该研究将验证推进至汇编指令层面，以RISC-V指令集为基础进行证明；Anthropic方面称，这是首次大规模利用AI在汇编代码层面将形式化验证应用于生产软件。