形式化验证或能解决AI的审查瓶颈

形式化验证作为一种严格的数学方法，正在成为解决AI生成代码审查瓶颈的关键技术。传统软件工程中，AI生成的代码需要经过人工审查才能确保正确性，而这已成为开发效率的瓶颈。然而，形式化验证通过将代码的规范形式化，使得AI生成的代码无需人工审查即可自动验证其正确性。

文章以电路优化器为具体案例，详细展示了这一方法的实际应用。电路优化器的核心任务是确保输出电路与输入电路等价（即功能相同），同时尽可能减小电路规模。团队使用Lean语言编写了约500行的规范，精确描述了优化器正确性的含义。编写规范耗时约两天，加上一天的团队审查。之后，AI代理根据这些规范生成了所有优化器代码及其证明，整个过程几乎不需要人工干预。团队仅通过检查CI标签和基准测试结果来“审查”PR，完全不审查生成的代码。

基准测试结果表明，优化器在电路规模缩减方面与之前的Rust实现相当，尽管运行时速度较慢，但最近三天内最慢的测试用例速度提升了三倍以上。团队通过FFI将Lean编译的C代码集成到现有的Rust代码库中，逐步替换组件，无需重写整个代码库。

作者认为，这种方法的关键在于编写和审计规范的成本必须低于编写和维护代码的成本。未来，可复用的规范库和模块化方法可能使形式化验证更广泛地应用。软件开发可能最终从关注代码转向关注需求，关键属性被形式化，其他部分通过提示和测试验证。开发者可能不再直接看到生成的代码，甚至不知道其编程语言。这为AI时代的软件工程提供了全新方向，有望显著缩短从开发到部署的周期。