人工智能形式化验证研究扩大规模，安全边界仍需明确
编辑部 · 发布 2026/10/23 · 更新 2026/10/23
钛媒体报道，Anthropic 与 Theorem Labs 研究利用大模型为开源程序生成形式化证明。报告覆盖一百二十三个软件库的二百三十九个程序入口，并把验证推进到汇编指令层面。研究尝试让模型生成可由证明系统检查的代码，以降低传统人工验证的成本。报道同时强调，这与通过大量测试寻找错误不同，核心在于检查给定条件下的程序性质。
钛媒体报道，Anthropic 与 Theorem Labs 研究利用大模型为开源程序生成形式化证明。报告覆盖一百二十三个软件库的二百三十九个程序入口，并把验证推进到汇编指令层面。
研究尝试让模型生成可由证明系统检查的代码，以降低传统人工验证的成本。报道同时强调，这与通过大量测试寻找错误不同，核心在于检查给定条件下的程序性质。
形式化验证不等于证明整个系统绝对安全。假设、规范和覆盖范围之外仍可能存在缺陷，依赖管理、修复审查和实际部署也不能由证明结果替代。
来源：钛媒体