上海AI实验室重磅发布：让机器自己学会编程验证，告别人工标注的时代

这项由上海人工智能实验室Veri-Code团队主导的突破性研究发表于2025年7月22日，论文题为"Re:Form — Reducing Human Priors in Scalable Formal Software Verification with RL in LLMs: A Preliminary Study on Dafny"。感兴趣的读者可以通过arXiv:2507.16331v1访问完整论文，相关代码和模型已在GitHub（https://github.com/Veri-Code/ReForm）和Hugging Face（https://huggingface.co/Veri-Code）开源。

想象一下这样的场景：你写了一段代码，但担心其中可能存在bug。传统的做法是人工检查或编写测试用例，但这就像在茫茫大海中寻找可能存在的漏洞一样困难。现在，上海AI实验室的研究团队开发出了一种全新的方法，让人工智能模型能够像一个经验丰富的程序员一样，自动为代码生成严格的数学证明，确保代码的正确性。

这项研究的核心思想非常巧妙：传统的大语言模型训练需要大量人工标注的数据，就像教小孩学习需要老师一步步指导一样。但在编程验证这个领域，人工标注的成本极其昂贵——为50个入门级程序标注正式规范就需要两名计算机科学家花费220小时，而像SeL4这样的复杂系统验证更是需要20人年的工作量。研究团队认为，如果能让AI系统自己学会这些技能，而不依赖于如此庞大的人工指导，那将是一个巨大的突破。

研究团队选择了Dafny这种特殊的编程语言作为实验平台。Dafny的特别之处在于，它不仅能编写程序，还能为程序添加数学上严格的规范说明。这就像为每道菜谱不仅写出制作步骤，还要精确描述每个步骤的预期效果和最终成果的质量标准。更重要的是，Dafny有一个自动验证器，能够数学证明代码是否真的符合这些规范，这为强化学习提供了可靠的反馈信号。

团队的创新之处在于构建了一个几乎不依赖人工先验知识的训练流水线。他们完全摒弃了传统的自然语言思维链提示，转而让模型直接在形式化语言空间中工作。这种做法的好处是避免了自然语言推理中常见的不可靠性和冗长性问题。同时，他们设计了一套巧妙的奖励机制，不仅要求生成的规范能通过验证器检查，还要求这些规范在逻辑上比参考答案更强。

在数据构建方面，研究团队开发了两条并行的自动化流水线。第一条流水线从公开的Dafny代码库中收集和清理现有代码，但由于Dafny代码的稀缺性，最终只收集到约1200个样本。第二条流水线更加创新：它从Python代码开始，通过模板提取、自动翻译和迭代调试的方式，将Python程序转换为带有完整规范的Dafny程序。这个过程完全自动化，无需人工介入每个样本的处理。

为了全面评估模型的能力，团队还构建了DafnyComp基准测试集。这个测试集的特殊之处在于包含了需要多函数协作的复杂程序，这些程序的规范需要考虑函数间的全局约束和交互，比单函数问题更具挑战性。测试集分为域内和域外两部分，前者用于评估模型在训练数据分布内的表现，后者则测试模型的泛化能力。

在模型训练过程中，团队采用了两阶段策略。监督微调阶段使用相对少量的数据让模型掌握Dafny的基本语法和语义。令人惊讶的是，即使是0.5B这样的小模型在经过监督微调后，也能生成语法正确且可验证的Dafny代码，表现超过了包括GPT-4o在内的大型专有模型。

强化学习阶段是整个方法的核心创新。团队设计了三种类型的奖励：语法奖励确保生成的代码能够编译通过，验证奖励确保代码与给定实现一致，而子集奖励则确保生成的规范在逻辑上至少与参考规范一样强。这个子集奖励特别巧妙，它利用了形式化规范之间天然存在的偏序关系，通过两个逻辑蕴含检查来验证生成规范的优越性：前置条件应该更宽松（允许更多输入），后置条件应该更严格（提供更强保证）。

实验结果令人印象深刻。在域内测试中，强化学习训练的模型在所有指标上都显著超过了仅使用监督微调的基线。更重要的是，模型展现出了真正的探索能力：约8%的测试样本中，强化学习模型生成了全新的、语义上有意义的后置条件，这些条件在监督微调模型的128次采样中从未出现过。这表明模型不仅仅是在记忆训练数据，而是真正学会了推理和创新。

在域外泛化测试中，14B参数的强化学习模型在具有挑战性的DafnyComp基准上取得了14.0%的验证成功率，相比监督微调模型的8.3%有显著提升，更是远超Claude等专有模型的2.7%。这说明强化学习不仅提升了域内性能，还帮助模型获得了可迁移的推理模式。

研究团队还发现了一些有趣的现象。当模型仅使用验证奖励训练时，容易出现"奖励破解"现象，即生成过于简单的规范来轻松通过验证器。而加入子集奖励后，这个问题得到了有效缓解。此外，熵正则化虽然会导致训练不稳定，但能显著提高模型的探索能力和输出多样性。

从更广阔的视角来看，这项研究代表了AI系统自主学习能力的重要进步。传统的机器学习严重依赖人工标注的数据和预设的推理模式，而这项工作展示了如何让AI系统在最小人工干预下，通过与环境的交互来学习复杂的推理技能。虽然研究仍保留了一些基本的人工先验（如预训练模型、基础数据种子等），但相比传统方法，已经大大减少了对人工知识的依赖。

这种方法的潜在影响是深远的。在软件开发领域，自动化的形式验证能够显著提高关键系统的可靠性，特别是在医疗、金融、自动驾驶等对安全性要求极高的场景中。更重要的是，这种让AI系统自主学习和探索的范式可能适用于其他需要严格推理的领域，为人工智能的进一步发展开辟了新的道路。

当然，这项研究也存在一些局限性。当前的方法主要针对相对简单的编程任务，对于复杂的现实世界软件系统，效果如何还需要进一步验证。同时，完全摒弃自然语言推理链是否适用于所有推理任务，也是一个值得深入探讨的问题。研究团队也坦承，对于一些非常复杂的推理任务，人类语言的引导可能仍然是必要的。

值得注意的是，这项研究的开源特性为整个学术界和工业界提供了宝贵的资源。完整的训练流水线、数据集和模型权重的公开，将大大加速相关研究的进展，也为实际应用奠定了基础。这种开放的研究态度体现了中国AI研究机构在推动全球科技进步方面的责任感。

展望未来，这项研究开启了许多激动人心的可能性。随着方法的不断完善和计算资源的提升，我们可能很快就能看到AI系统在更复杂的推理任务中展现出类似的自主学习能力。这不仅将改变软件开发的方式，更可能为人工智能向真正的通用智能迈进提供重要启示。

说到底，这项研究最重要的贡献不仅是在特定任务上的性能提升，更是展示了一种新的AI训练范式：让机器在最小的人工指导下，通过与环境的交互来学会复杂的推理技能。这种范式的成功应用，为我们理解和构建更加自主、更加智能的AI系统提供了宝贵的经验和启示。

Q&A

Q1：什么是Dafny？为什么要选择它作为研究平台？ A：Dafny是微软研究院开发的一种特殊编程语言，它不仅能编写程序，还能为程序添加数学上严格的规范说明。选择Dafny是因为它有自动验证器，能够数学证明代码是否符合规范，这为强化学习提供了可靠的反馈信号，而传统编程语言缺乏这种自动化的正确性检查机制。

Q2：这个方法会不会完全取代程序员的工作？ A：目前不会。这项研究主要针对相对简单的编程验证任务，距离处理复杂现实世界软件系统还有很大距离。它更像是程序员的智能助手，能够自动生成和验证程序规范，提高开发效率和代码质量，但复杂的系统设计和业务逻辑实现仍需要人类程序员的创造力和判断力。

Q3：这种不依赖人工标注的训练方法有什么优势？ A：最大优势是大幅降低了训练成本和时间。传统方法需要专家花费大量时间进行人工标注，比如为50个程序添加规范需要220小时专家工作。而这种方法让AI系统通过与验证器的交互自主学习，不仅节省了人力成本，还能发现人类专家可能遗漏的新颖规范，展现出真正的探索和创新能力。