在人工智能日益承担起编写核电站控制程序、自动驾驶系统等关键软件的今天，如何确保其生成代码的绝对可靠性，已成为亟待破解的安全难题。当前主流AI系统依赖人类设计的测试用例进行验证，但这种方法面临两大根本性瓶颈：其一，随着代码复杂度上升，测试用例数量呈指数增长，难以覆盖所有执行路径；其二，测试无法发现深层逻辑缺陷，尤其在复杂系统中漏洞可能长期潜伏。 针对这一挑战，上海人工智能实验室青年科学家付杰团队（Veri-Code Team）提出了一种新范式——通过强化学习驱动大模型直接生成可形式化验证的代码，从而大幅降低对人类先验知识的依赖。相关研究成果以《Re：Form——减少可扩展形式化软件验证中的人类先验知识：在 Dafny 中的初步研究》为题发表于 arXiv，并已开源数据、代码与模型。 该团队的核心思路是：利用形式化验证工具（如 Dafny）提供的数学级可靠性反馈，构建一个客观、无歧义的训练信号环境。Dafny 作为一门支持程序行为精确规范的语言，能将代码逻辑转化为可验证的数学命题，其验证结果不依赖人类判断，具有“定理级”可信度。这为AI训练提供了理想的“奖励环境”。 传统方法依赖人工标注的思维链（CoT）和结果评判，不仅成本高昂——为50个初级程序编写规范需220小时，验证SeL4操作系统耗时20人年——且易受主观偏差影响。更关键的是，当AI能力超越人类时，人类提供的监督信号本身可能包含错误，形成认知瓶颈。付杰团队由此提出：与其让AI模仿人类不完美的推理过程，不如引导其在形式化空间中自主探索。 他们设计了名为 Re：Form 的训练框架，摒弃人工CoT与主观奖励机制，转而采用“验证通过”与否的0/1信号，并引入“规范优越率”（SSR）作为更精细的奖励指标。该指标衡量生成的代码规范是否比基准更严格或更通用，有效防止模型通过“奖励破解”（如输出空语句）获取虚假高分。 为获取训练数据，团队构建了代码翻译流水线，将Python代码自动转换为可验证的Dafny代码，并创建了名为 DafnyComp 的基准测试集，用于评估模型的组合泛化能力。在对 Qwen2.5-coder 进行语法微调后，团队在0.5B至14B规模模型上实施强化学习训练，结果表明，Re：Form 模型在验证通过率与SSR指标上均超越 GPT-4o 和 Claude4 等闭源模型。 值得注意的是，该方法在保持高验证率的同时，实现了对形式化语言的高效学习。Dafny 的代码结构天然适合渐进式训练：代码行数与复杂度呈线性关系，便于设计课程学习路径；其模块化要求也使模型组合能力成为可测量的智能指标，为迈向通用人工智能提供关键路径。 展望未来，团队计划探索让模型自主学习CoT的能力，并推动系统支持万行级代码的验证。这一研究不仅回应了“如何制造安全AI”的核心命题，更标志着AI开发正从“事后修补”转向“从源头保障”的范式跃迁。在可验证、可扩展、可信赖的软件系统构建道路上，形式化验证正成为不可或缺的基石。