2025全球机器学习技术大会-自动形式化验证与可信代码生成

在2025年全球机器学习技术大会上，关于自动形式化验证与可信代码生成的议题，微软亚洲研究院研究员卢帅发表了深入的研究成果和见解。卢帅研究员拥有北京大学的学术背景，专注于代码智能和自然语言处理领域。他在代码生成、代码大模型以及程序自动化验证方面取得了显著成果，其研究在NeurIPS、ICLR、ACL、ICSE和FSE等顶级会议上发表，受到学术界广泛关注，谷歌学术引用量超过5000次。 卢帅研究员提出，软件开发的自动化是人工智能领域的一个重要分支，尤其在代码生成和自动化验证方面有着极大的潜力。在代码生成方面，大模型技术的发展促使软件开发更加快速、高效，但同时也面临着模型输出正确答案概率的挑战。他提出从模型角度提高输出正确率，并通过后验证拒绝错误输出的策略。 可信代码生成的研究涉及模型优化、后验证和自动测试验证。模型优化包括引入更多高质量数据、利用长思维链和强化学习来提升模型思考和反思的能力。后验证则指利用可信赖的工具自动验证模型输出，通过测试用例的自动编写和形式化证明的生成来减少人力负担。此外，自动测试验证通过从多个角度生成输出并互相验证来找出最合理的代码，但存在生成测试用例正确性无法保证的问题。 形式化验证是确保代码质量的关键技术，它不依赖于执行代码，而是用数学证明来确保代码满足特定性质。形式化验证的工具和语言如Fstar、Coq、Isabelle、Verus、Dafny等，被用于编写形式化证明，如循环不变量、断言等。尽管形式化验证理论上能保证代码的绝对正确，但编写证明的过程可能非常耗时。 自动形式化验证则进一步提升形式化验证的效率，它通过大模型直接生成形式化规范和证明，反馈给定理证明器进行验证。尽管这种方法能够减少人力并加速开发，但它面临着大模型在形式化验证知识上的不足、预训练数据稀缺、以及大模型与定理证明器交互能力不足等挑战。 卢帅研究员的研究不仅推动了软件开发自动化的进程，还指出了可信代码生成和形式化验证在实际应用中需要克服的技术障碍。随着技术的不断进步，这些挑战有望逐步被解决，进一步促进代码生成和自动化验证技术的广泛应用。