AI将引爆主流:形式化验证即将迎来黄金时代?
作者：微信文章关于AI对软件开发的影响，已有太多讨论，但有一个角度鲜有人提及——我认为，AI将让形式化验证这一曾经“高冷”数十年的技术，正式进入软件工程的主流舞台。
小众的尖端技术
像Rocq、Isabelle、Lean、F*、Agda这类证明助手和面向证明的编程语言早已存在。它们能让你为某段代码写出形式化规范，然后从数学上证明代码始终满足这一规范，哪怕是在你从未想到要测试的边界情况下。这些工具曾用于开发一些大型的形式化验证软件系统，比如操作系统内核、C编译器、加密协议栈。
但目前，形式化验证主要还是研究项目在用。工业界的软件工程师——哪怕是做医疗设备、飞机等高可靠性系统的开发者——也很少采用形式化方法。原因在于，书写证明既极其困难（需要博士级别的专业知识），又极其耗费人力。
举一个著名的例子：截至2009年，经过形式化验证的seL4微内核包含8700行C代码，但为了证明其正确性，花费了20人年、写下了20万行Isabelle证明代码。这意味着，每行C代码平均需要23行证明和近半个人日的工作量。此外，全球可能只有几百人（粗略估计）掌握这类证明的撰写，因为这需要对证明系统有极其精深的了解。
用经济学的话说：对大多数系统而言，出错的预期成本，低于用形式化证明去消除这些错误的预期成本。或许也因为，软件缺陷的代价往往被外部化——承担成本的是用户，而非开发者。但即便开发者承担代价，形式化验证本身也太难、太贵了。
AI正在改变规则
直到最近，情况终于出现转机。基于大语言模型的编程助手不仅在编写实现代码方面越来越出色，还在书写多种语言的证明脚本上展现潜力。目前，仍需要具备专业知识的开发者进行引导，但不难想象，未来几年这个过程可能完全自动化。一旦实现，形式化验证的经济模型将彻底颠覆。
如果形式化验证成本大幅降低，我们将有能力验证更多软件。不仅如此，AI也创造了对形式化验证的更大需求：与其靠人工审查AI生成的代码，我宁愿让AI向我证明，它生成的代码是正确的。如果它能做到，我会毫不犹豫地选择AI生成的代码，而不是可能藏着手工bug的人工代码。
实际上，我认为撰写证明脚本是大语言模型的最佳应用场景之一。它即便“胡编乱造”也没关系，因为证明检查器会拒绝无效的证明，并迫使AI重新尝试。检查器本身是一小段经过验证的代码，几乎不可能有错误证明蒙混过关。
挑战并未消失
这并不意味着软件会突然变得完美无缺。随着验证过程自动化，挑战将转向如何正确定义规范：你怎么知道被证明的性质，真的是你关心的性质？读写形式化规范仍需要专业知识和缜密思考。但与手写证明相比，编写规范要容易得多、快得多——这已是巨大进步。
我们还可以期待AI助理在编写规范时提供帮助，在形式化语言和自然语言之间进行翻译。尽管可能存在语义细微处的丢失风险，但这是可控的。
想象一下这样的未来：我们可以用高级、声明式的方式，描述希望代码具备的性质，然后AI直接生成实现代码及其符合规范的证明——这想想就令人激动。它将彻底改变软件开发的本质：我们甚至无需再费心查看AI生成的代码，就像我们不会去看编译器生成的机器码一样。
主流化的三个推力
总结来说，有三个力量正推动形式化验证走向主流：
成本骤降：形式化验证即将变得极为经济；
AI需求：AI生成的代码需要形式化验证，以便我们绕过人工审查仍能确信其正确性；
精确制衡：形式化验证的精确性，正好弥补了大语言模型的不精确和概率性本质。
三者合一，意味着形式化验证很可能在可见的未来成为主流。我猜想，不久后的限制因素将不再是技术，而是人们需要意识到：形式化方法在实践中已切实可行——这需要一场认知与文化上的转变。
页:
[1]