Test, Don't (Just) Verify
5 months ago
- #AI
- #Software Engineering
- #Formal Verification
- 人工智能正使形式验证成为主流——AI辅助的机械证明公司获得融资，新用户开始采用Lean等证明助手工具
- 形式验证面临两大挑战：多数软件缺乏形式化规范，以及证明工程实施难度高
- AI辅助编程推动规范驱动开发，激励可执行规范创建，同时赋能程序优化器和翻译器
- 形式验证能证明程序无缺陷，例如CompCert C编译器在错误检测方面优于GCC和Clang
- AI擅长编写证明，可与可验证奖励强化学习(RLVR)结合提升性能
- 自动形式化是AI辅助验证编程中可信计算基(TCB)的关键但脆弱环节
- 证明助手速度缓慢源于使用皮亚诺数等归纳类型，但可通过高效编码和提取技术解决
- 验证需要领域特定模型，这类模型创建困难（如运行时性能领域）
- 测试通过证伪补足验证，如Rocq生态中的QuickChick工具所示
- 验证引导开发(VGD)融合验证版与生产版实现，利用测试确保正确性与速度
- 随机测试与形式验证对软件工程未来同等重要，二者形成互补关系