验证程序的计算逻辑正确性，也即证明程序正确实现了其想达到的功能。从形式化验证的角度，就是验证从spec到实现的一致性。第一个难关就是如何形式化specification，这既需要了解该程序，又需要懂形式化表达。很多软件设计文档是自然语言描述的，包括对其功能的描述也是用自然语言。大语言模型出来之后，开始有人探索利用大模型自动化把自然语言描述的需求翻译为形式逻辑语言，后者可以被计算机理解，从而采用形式化工具。下面是最近的一个工作。@有个梨GPT 也许有兴趣。
当然，这就是自动数学建模了，又是一个大的挑战，我之前写过另一篇微博讨论过，目前比较靠谱的是数学语言模板+交互式自动建模，完全自动建模的正确性很难保证。所以，目前利用大模型做翻译的方法是用来降低难度，而非完全解决问题。下面这个工作也是走这个路线。
"nl2spec: Interactively Translating Unstructured Natural Language to Temporal Logics with Large Language Models". Matthias Cosler, Christopher Hahn, Daniel Mendoza, Frederik Schmitt, and Caroline Trippel. In Proceedings of the 34th International Conference on Computer Aided Verification, July 2023.