演讲主题

自动形式化验证与可信代码生成

近年来，大语言模型已经展示出卓越的代码生成能力。然而，大模型并不能保证生成代码的准确性，尤其是对于较为复杂的算法实现或是工程代码，通常很难在一次尝试中生成正确的程序。为了解决这一问题，报告将介绍如何在大模型时代下引入软件工程领域的程序测试和形式化验证等方式，借助大模型强大的生成能力，一方面，让大模型自我验证，从而提高代码生成的可信度。另一方面，报告将着重关注如何利用大模型将复杂的形式化验证过程自动化，从理论证明的角度验证代码可靠性。 1. 以往工作通过引入测试与验证，利用模型的多角度自洽性提高代码生成可信度 2. 形式化验证对于可信代码生成的优势与挑战 3. 利用数据合成实现大语言模型在自动形式化验证上的自我进化