Anthropic称Claude数周验证百个开源库
热点事件持续更新
Anthropic称Claude数周验证百个开源库
2 篇报道2 个报道来源14 小时前更新
先了解这件事
AI 综述
Anthropic 称，其 Frontier Red Team 与 Theorem Labs 合作，让 Claude 将 OSS-Fuzz 中 123 个开源库的崩溃测试转化为数学问题，并在几周内生成约 1.8 亿行证明代码，由独立程序 Rocq 自动检查，几乎无需人工审核。形式化验证可证明代码不存在某些 bug，但过去只适用于小型代码库，或需投入大量专家时间。 据 The Decoder 报道，这些证明只在严格条件下成立：特定处理器架构、单线程程序和小于 64 MB 的输入。报道还称单条证明消耗数亿 token，算力成本高，Anthropic 未公布项目总成本；Opus 5.5 能用比 Opus 5 少约 40% 的 token 解决其中一半证明。该结果目前是 Anthropic 单方面公布。
AI 根据报道生成 · 13 小时前更新
最新进展10月23日 19:32
Anthropic 用 Claude 自动生成形式化验证证明并发现大量隐藏 bug报道时间线
沿着报道，了解事件的不同侧面。
10月23日
- The Decoder：AI NewsAnthropic 用 Claude 自动生成形式化验证证明并发现大量隐藏 bug
Anthropic 前沿红队与 Theorem 合作，让 Claude 将 OSS-Fuzz 中 123 个开源库的崩溃测试转化为数学问题，几周内生成了约 1.8 亿行证明代码，由独立程序 Rocq 自动检查，几乎无需人工审核。
- Anthropic精选Anthropic 发布用 Claude 大规模形式化验证软件的研究
Anthropic 在 Frontier Red Team 博客发布新研究，介绍用 Claude 对软件做大规模形式化验证。形式化验证可证明代码不存在某些 bug，但过去只适用于小型代码库或需要大量专家时间；Anthropic 与 theoremlabs 合作，用 Claude 在几周内证明了超过一百个真实开源库的安全属性。
本事件热度走势
- 可比范围当前
- 23
- 可比范围峰值
- 3410月23日 20:00
- 近 24 小时变化
- +153%
010203040
12:0018:0010月24日06:00
趋势仅比较持续完整观测到的相同主体，范围可能小于当前热度统计。移动指针或点击图表查看每小时热度；键盘可用左右方向键切换。