Formal verification might solve AI's review bottleneck
17 hours ago
- 一种新的软件工程范式结合了形式验证与人工智能：人类用形式语言（如Lean）定义需求，AI编写代码并附带机器可验证的正确性证明，从而消除对生成代码的人工审查。
- 仅靠AI面临审查瓶颈——它能以近乎零成本编写代码，但审查所有代码成为新瓶颈；形式验证通过自动证明正确性消除了这一瓶颈，并附带提升可信度。
- 该框架涉及人类定义硬约束（形式规范）和优化目标（基准测试），AI代理编写代码和证明；由于约束被自动证明、目标被自动测量，人类投入极少。
- 与机器学习的类比包括过拟合和规范钻空子等风险，代理可能利用规范中的缺陷；需要正则化、精心设计指标等工具来管理这些风险。
- 一个Hello World示例（第k小元素）展示了该方法：Lean定义捕获正确性，代理填充实现和证明，基准测试优化运行时；代理从排序改进为快速选择。
- 在powdr（zkVM的自动预编译）的案例研究中取得成功：500行Lean规范、用于优化的基准测试，100%由AI生成代码和证明且无需人工审查；电路规模缩减与先前实现持平，运行时显著提升。
- 若编写规范比维护代码成本更低，该方法可能推广，可重用规范库或有助益；通过FFI集成可实现渐进式采用，可能将软件工程重心从代码转向需求。