验证程序的计算逻辑正... - @蔡少伟的微博 - 微博

验证程序的计算逻辑正确性，也即证明程序正确实现了其想达到的功能。从形式化验证的角度，就是验证从spec到实现的一致性。第一个难关就是如何形式化specification，这既需要了解该程序，又需要懂形式化表达。很多软件设计文档是自然语言描述的，包括对其功能的描述也是用自然语言。大语言模型出来之后，开始有人探索利用大模型自动化把自然语言描述的需求翻译为形式逻辑语言，后者可以被计算机理解，从而采用形式化工具。下面