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

1、ML-SummitML-Summitwww.cpp-www.ml-summit.orgwww.gosim.orgwww.pm-summit.orgML-SummitML-SummitML-SummitML-SummitML-SummitML-Summit卢卢帅帅 微微软软亚亚洲洲研研究究院院研研究究员员微软亚洲研究院研究员，2021年毕业于北京大学。研究领域为代码智能和自然语言处理，致力于用大模型技术实现软件开发自动化，赋能程序开发者。主要研究方向是代码生成、代码大模型，程序自动化验证等，研究成果发表于NeurIPS,ICLR,ACL,ICSE,FSE等学术会议，谷歌学术引用量5000余次。演

2、演讲讲主主题题：自自动动形形式式化化验验证证与与可可信信代代码码生生成成ML-SummitML-Summit2 20 02 25 5 全球机器学习技术大会自自动动形形式式化化验验证证与与可可信信代代码码生生成成卢帅微软亚洲研究院ML-SummitML-Summit目目录录可信代码生成形式化验证的优势与挑战自动形式化验证模型的自我进化ML-SummitML-SummitML-SummitML-Summit代码生成大模型（GPT-4o）ML-SummitML-Summit可信代码生成输出概率分布期待只返回一个输出矛矛盾盾！解决方案（模型角度）提高模型输出正确答案的概率 通过后验证，拒绝错误输出ML

3、-SummitML-Summit可信代码生成 模型优化 更多高质量数据 训练本身就是提高正确答案的概率的过程 长思维链 引导大模型学会思考和反思 强化学习 进一步提升模型能力只只能能减减少少模模型型犯犯错错的的概概率率，无无法法达达到到真真正正的的可可信信ML-SummitML-Summit可信代码生成 后验证用可信赖的工具自动验证模型输出 测试 形式化验证让模型自动验证？自动写测试用例 自动写形式化证明繁琐！耗时！解放人力！ML-SummitML-Summit可信代码生成 后验证用户意图生成的代码自动后验证反馈代码执行器/定理证明器大模型大模型测试用例/形式化规范ML-SummitML-Su

4、mmit可信代码生成 自动测试验证Chen,Bei,et al.CodeT:Code Generation with Generated Tests.ICLR.2023.Huang,Baizhou,et al.Enhancing Large Language Models in Coding Through Multi-Perspective Self-Consistency.“ACL 2024让大模型同时从多个角度进行输出，再通过代码执行的方式互相验证多组输出间的一致性，找出最合理的代码。缺陷：生成的测试用例不能保证正确程序测试本身不能保证代码绝对可信ML-SummitML-SummitML

5、-SummitML-Summit形式化验证在不执行代码的条件下，用数学证明的方式验证代码满足特定的性质二分搜索需要满足的性质（specification）：输入的性质vector是有序的value存在于vector里输出的性质返回值下标在vector对应的数等于valueML-SummitML-Summit形式化验证使用形式化证明工具（定理证明器）验证代码满足性质 常见形式化验证语言：Fstar,Coq,Isabelle,Verus,Dafny,.需需要要形形式式化化证证明明（proof）！ML-SummitML-Summit形式化验证证明包括：循环不变量、断言、。成功证明代码满足二分搜索的性

6、质 理论上的绝对正确 写证明的时间甚至超过写代码的时间ML-SummitML-Summit自动形式化验证用户意图生成的代码形式化证明反馈定理证明器大模型大模型形式化规范大模型证明反馈ML-SummitML-Summit自动形式化验证的挑战 当前大模型对形式化验证知识的不足 标注数据极其稀缺 大模型与定理证明器的交互能力不足预训练数据微调数据Debugging数据ML-SummitML-SummitML-SummitML-Summit解决数据不足的难点数数据据不不足足的的三三个个方方面面 缺少已经得到证明的代码code+specification+proo