可自动检测AI生成程序可靠性？科学家提出减少软件验证对先验知识的依赖

主要观点总结

文章介绍了在人工智能在编程领域的一个关键安全问题，即如何确保AI生成的程序绝对可靠。针对这个问题，上海人工智能实验室青年科学家付杰团队进行了系统性研究，使用形式化语言直接生成可验证的代码，以此来判断代码行为是否符合人类意图。文章还详细描述了他们的研究成果，包括解决AI编程中的验证危机、建立数学定理级别的验证体系、利用形式化定理验证器提供保真的训练信号等。此外，文章还提到了其他研究团队的工作和未来的研究重点。

关键观点总结

关键观点1: AI编程中的关键安全问题及挑战

人工智能在尝试编写核电站控制代码和自动驾驶系统代码时面临的关键安全问题是如何确保AI生成的程序绝对可靠。当前主流AI系统存在根本性隐患，依赖人类编写的测试用例进行验证，但这种方法存在两大致命缺陷。一是测试用例数量随代码复杂度增加呈指数级增长，二是无法穷尽所有代码分支路径，尤其难以发现隐藏的逻辑漏洞。

关键观点2: 形式化语言在解决AI编程安全问题中的应用

付杰团队使用形式化语言（如Dafny）直接生成可验证的代码，以此判断代码行为是否符合人类意图。团队在模型训练过程中使用强化学习，减少大模型对人类先验知识的依赖。这种方法适用于确保医疗、金融、自动驾驶和操作系统等安全关键领域的软件没有漏洞。

关键观点3: 验证危机和AI发展的认知枷锁

当前流行的长思维链（CoT）等非形式化推理方法本质上是模仿人类不完美的思维模式，这将成为制约AI发展的认知枷锁。为了真正解决安全问题，必须从“给AI打安全补丁”转向“设计安全AI”，其中一个有效方法是建立数学定理级别的验证体系。

关键观点4: 形式化定理验证器的优势和应用

形式化定理验证器是打开安全之门的“钥匙”。它以Lean/Dafny为代表的验证框架，通过数学逻辑引擎生成“无错误声明”。这种声明的可靠性达到数学定理级别，其真理性不因AI智能水平而变化。付杰团队希望利用形式化定理验证器提供的保真的训练信号，完全利用强化学习让模型自主学习以生成基于形式化语言的代码，从而实现可扩展性。

关键观点5: 研究的未来展望

付杰团队在研究过程中一直在探索如何找到一条可以拓展训练、减少人类非必要先验对训练的影响的道路。他们意识到软件系统是高度形式化的，可以被精确地建模、用数学逻辑进行严格规范和验证。因此，团队将构建可验证的、高可靠性的软件系统确立为终极目标。此外，他们还关注如何提升生成代码的形式化验证效率、如何评估智能体的组合能力等问题。