Anthropic在严格条件下使用Claude对现有代码进行形式化验证

发生了什么

Anthropic与Theorem使用Claude验证现有软件，在几周内为Google OSS-Fuzz项目中123个开源库的测试程序生成了约1.8亿行数学证明代码。Rocq独立检查了这些证明，Anthropic称这一过程发现了数百个错误，几乎不需要人工审查。这些保证仅适用于特定处理器架构、单线程程序以及小于64 MB的输入，而单个证明消耗了数亿个token。

接下来读什么

• 今日还有哪些重要变化OlmoEarth v1.3 发布全球卫星嵌入数据和基于浏览器的地图探索工具

这件事到目前为止

Anthropic 和 Theorem 使用 Claude 对现有软件进行形式化验证：几周内，他们针对 Google OSS-Fuzz 项目中 123 个开源库的测试程序，生成了约 1.8 亿行数学证明代码。Rocq 独立检查了这些证明；Anthropic 表示，这一过程发现了数百个错误，几乎不需要人工审查。 这些保证仅适用于特定处理器架构、单线程程序以及小于 64 MB 的输入。单个证明消耗了数亿个 token，因此计算成本和狭窄的适用范围是这项工作的主要局限。