在人工智能日益承担起编写高安全要求代码（如自动驾驶、核电站控制）的背景下，如何确保AI生成代码的绝对可靠性成为关键挑战。当前主流AI系统依赖人类编写的测试用例进行验证，但该方法存在两大根本缺陷：一是测试用例数量随代码复杂度呈指数增长，难以全面覆盖所有执行路径；二是无法发现深层逻辑漏洞，尤其在复杂系统中风险极高。针对这一问题，上海人工智能实验室青年科学家付杰团队（Veri-Code Team）提出“Re：Form”框架，通过结合强化学习与形式化验证语言Dafny，显著降低对人类先验知识的依赖，实现可扩展的代码正确性验证。 该研究的核心在于将AI训练过程从依赖人工标注的“思维链”（CoT）和主观评判，转向基于数学逻辑的客观验证信号。团队采用Dafny这一形式化语言，其代码与规范可被逻辑引擎自动验证，生成的“无错误声明”具备数学定理级别的可靠性。研究团队构建了从Python代码自动翻译为Dafny代码的数据管道，并设计了名为DafnyComp的基准测试集，用于评估模型的组合泛化能力。在训练中，他们对Qwen2.5-coder模型进行监督微调以掌握语法，随后引入强化学习，奖励机制不仅基于验证通过与否，更创新性地引入“规范优越率”（SSR），衡量生成规范是否比原始规范更精确或约束更弱，从而防止模型通过简单语句“奖励劫持”。 实验表明，Re：Form在14B规模模型上，于pass@1指标上全面超越GPT-4o和Claude4等闭源模型，且在多个基准测试中表现优异。更重要的是，该方法无需依赖人类提供的CoT或结果反馈，实现了从“模仿人类推理”到“自主生成可验证代码”的范式转变。付杰指出，这不仅是技术突破，更是“制造安全AI”的关键路径——通过数学宇宙假说的启发，将真实世界问题映射为形式化空间中的可证命题，从而建立稳定、可扩展、不受人类认知局限影响的AI训练体系。 业内专家评价，该研究为AI安全验证提供了极具前瞻性的解决方案。形式化验证与强化学习的结合，有望成为下一代可信AI系统的基础架构。尤其在医疗、金融、操作系统等高风险领域，此类技术可大幅降低因代码漏洞引发的系统性风险。团队已开源代码、模型与数据，推动社区共建可信AI生态。未来，团队计划拓展至更长代码（上万行）与自学习CoT能力，迈向通用人工智能的可验证路径。