Anthropic 让 Claude 自主生成数学证明验证代码安全性

Anthropic 联合 Theorem 利用 Claude 自主生成约 1.8 亿行数学证明代码，对 Google OSS-Fuzz 中的 123 个开源库进行形式化验证。该方法在严格条件下（特定架构、单线程、输入小于 64MB）自动发现深层 Bug，但计算成本高昂且适用范围有限。