卢帅-自动形式化验证与可信代码生成_2025 4月全球机器学习技术大会-上海站-CSDN在线视频培训

分会场-D

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

课时介绍

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

课程介绍

自1936年阿兰· 图灵提出「图灵机」以及机器具备「思维」的可能性以来，以机器学习为代表的人工智能经过飞速发展，深刻地改变着我们的世界。CSDN & Boolan 秉承“全球专家，卓越智慧”的宗旨，特邀近50位技术领袖和行业应用专家，与1000+来自电商、金融、汽车、智能制造、通信、工业互联网、医疗、教育等众多行业的精英参会听众，共同探讨人工智能领域的前沿发展和行业最佳实践。