上海人工智能实验室青年科学家付杰团队提出一种新方法，旨在减少人工智能在生成软件代码时对人类先验知识的依赖，实现可自动验证的高可靠性代码生成。当前主流AI编程系统依赖人工编写的测试用例来验证代码，但这种方法在复杂场景下面临两大瓶颈：测试用例数量随代码复杂度呈指数增长，且难以覆盖所有执行路径，尤其难以发现深层逻辑漏洞。 为突破这一困境，付杰团队提出“Re：Form”框架，利用形式化语言Dafny直接生成可数学验证的代码与规范。该方法通过强化学习训练大模型，使其在无需人类标注思维链（CoT）或主观评判的情况下，自主生成符合用户意图、且可通过形式化验证器检验的代码。其核心优势在于：Dafny提供的验证信号是客观、精确的数学命题，不受人类认知偏差影响，从而构建出可扩展、稳定可靠的训练闭环。 研究团队发现，完全摒弃CoT也能有效训练模型，尤其在中等复杂度任务中表现良好。他们构建了名为DafnyComp的基准测试集，用于评估模型在模块组合与泛化能力方面的表现。为提升训练质量，团队引入“规范优越率”（SSR）作为奖励信号，衡量生成规范是否比原始规范更优（如约束更松、描述更严），有效防止模型“奖励劫持”（reward hacking）。 实验结果显示，经强化学习训练的Re：Form模型（0.5B至14B参数规模）在验证通过率和SSR指标上均超越GPT-4o、Claude4等闭源模型，尤其在长代码和复杂任务中展现出更强的可验证能力。此外，Dafny相比其他形式化工具（如Lean）具有更小的搜索空间和线性可度量的复杂度，适合渐进式训练，为通向通用人工智能的关键能力——组合泛化——提供了理想实验平台。 该研究强调，未来目标是让模型自主学习CoT，并扩展至上万行代码的系统级验证。这一路径标志着从“给AI打补丁”向“设计安全AI”的范式转变，为医疗、金融、自动驾驶、操作系统等安全关键领域提供数学级可靠软件保障。相关论文已发表于arXiv，代码与数据已开源，推动AI安全验证进入新阶段。