Prediction: AI will make formal verification go mainstream
5 months ago
- #AI
- #Software Engineering
- #Formal Verification
- 人工智能预计将推动形式化验证技术进入主流软件工程领域
- Rocq、Isabelle、Lean、F*和Agda等形式化验证工具支持对代码正确性进行数学证明
- 当前形式化验证过程劳动密集且需要博士级专业能力，仅限研究项目使用
- 以大型语言模型为代表的AI能自动生成验证脚本，大幅降低形式化验证成本与门槛
- AI生成代码必须通过形式化验证才能确保正确性，无需人工复核
- 形式化验证的精确性恰好弥补了大型语言模型的概率性缺陷
- 未来核心挑战将转向如何正确定义规范，而非编写证明过程
- AI可协助实现自然语言描述与形式化规范之间的双向转换
- 形式化验证能否成为主流，既取决于技术进步，也关乎行业文化的接纳程度