Anthropic 研究：Claude 可自动生成代码安全证明并发现隐藏漏洞

Anthropic 与 Theorem 合作，利用 Claude 为现有代码自动生成数学证明以验证其正确性。该方法在几周内生成了约 1.8 亿行证明代码，并发现了数百个常规测试难以捕捉的漏洞，包括一个存在超过十年的逻辑错误。该验证过程在特定处理器架构、单线程程序等严格条件下有效，但计算成本高昂，单个证明可能消耗数亿 token。