Anthropic称Claude数周生成约1.8亿行形式化验证证明
热点事件历史事件
Anthropic称Claude数周生成约1.8亿行形式化验证证明
2 篇报道2 个报道来源10 天前更新
先了解这件事
AI 综述
Anthropic 与 Theorem Labs 于10月23日发布报告《大模型正让形式化软件验证在更大规模上变得可行》，称其 Claude 模型针对 Google OSS-Fuzz 项目中123个开源软件库的239个程序入口，在几周内生成了约1.8亿行 Rocq 证明代码，并发现和修复了数百个 Bug，包括多年未被发现的漏洞。 据 Anthropic 称，这些证明由独立的 Rocq 程序自动检查，几乎不需要人工审查。研究团队还将验证推进到了汇编指令层面，以 RISC-V 指令集为基础进行证明。 需要说明的是，这些证明只在严格条件下成立：特定处理器架构、单线程程序，且输入小于 64 MB。
AI 根据报道生成 · 6 天前更新
最新进展10月23日 19:32
Anthropic 用 Claude 自动生成形式化证明验证现有代码安全性报道时间线
沿着报道，了解事件的不同侧面。
10月23日
- The Decoder精选Anthropic 用 Claude 自动生成形式化证明验证现有代码安全性
Anthropic 的 Frontier Red Team 与 Theorem 合作，让 Claude 将 OSS-Fuzz 的 123 个开源库测试转化为数学问题，几周内生成约 1.8 亿行证明代码，由 Rocq 程序自动检查，几乎不需人工审查。
- 钛媒体Anthropic发布报告：Claude生成约1.8亿行Rocq证明代码，让形式化验证规模化可行
Anthropic与Theorem Labs于10月23日发布报告《大模型正让形式化软件验证在更大规模上变得可行》，Claude模型针对123个开源软件库中的239个程序入口生成约1.8亿行Rocq证明代码，发现并修复数百个Bug，包括多年未被发现的漏洞。