在程序验证领域，将机器学习与形式化验证器结合已成为重要研究方向。与传统软件测试不同，ML 程序验证器的核心任务是让模型学会生成能够通过形式化验证的证明脚本、不变式或注解。这一目标的实现高度依赖于训练配方的设计 —— 从超参数调优到损失函数选择，再到数据集构建策略，每一个环节都直接影响最终验证成功率。本文系统梳理 ML 程序验证器的训练方法论，为工程实践提供可落地的参数建议与监控要点。
任务建模与模型选型
在设计训练流程之前，需要首先明确任务的建模方式。根据输出形式的不同，ML 程序验证器通常采用以下两种主流范式：序列到序列模型与判别式模型。前者以程序源码（含规范说明）为输入，输出证明脚本、循环不变式或类型注解；后者则对给定的候选证明或不变式进行打分，输出被验证器接受的概率。实际系统中，往往以代码模型（如 CodeBERT、CodeLlama 等 Transformer 架构）为基础，外部验证器提供最终的正确性信号，形成 “模型生成 + 验证器裁决” 的协作架构。
模型选型直接影响后续的超参数空间与训练成本。若选择从零训练，需关注隐藏层维度、注意力头数、层数等架构参数；若选择微调已有代码预训练模型，则需重点调整学习率、训练轮次与微调层范围。实践中，从具备代码理解能力的预训练模型出发进行微调，是降低验证器调用成本的有效策略 —— 模型已具备基本的语法与语义理解能力，只需学习验证相关的特定模式。
数据集构建：验证器在环的数据工程
数据集是训练 ML 验证器的核心资产，其质量直接决定模型能否学习到有效的验证推理能力。构建数据集时，需要综合考虑样本多样性、标注质量与分布一致性三个维度。
样本结构设计方面，每个训练样本应包含以下核心字段：源代码（经规范化或格式化处理）、形式化规范（前后条件、断言、合约或类型约束）、标准答案（正确的证明脚本、不变式或注解）以及验证器反馈（成功 / 失败状态、错误信息、反例）。仅包含源代码与标准答案的样本难以让模型理解 “为何正确”，而加入验证器反馈可以帮助模型建立输出与验证结果之间的关联。
负样本策略是提升模型区分能力的关键。正样本是能够通过验证的正确证明，而负样本则需要精心设计以模拟真实场景中的错误。硬负样本指那些几乎正确但因细微差别而失败的候选项，例如常量值错误、循环不变式条件弱化、证明步骤遗漏等；结构负样本则是语法合法但逻辑错误的候选项。引入足够比例的负样本（建议负、正样本比例不低于 1:3 至 1:5），可以显著提升模型在推理阶段的召回率。
数据来源通常包括三类：一是现有的已验证代码库，如 Coq、Isabelle、Viper、Dafny、Frama-C 项目中的真实证明与规范；二是基于模板与随机变异的合成程序与证明；三是通过验证器自动标注的样本 —— 将候选证明输入验证器，根据返回结果自动生成标签。第三类方式可以低成本扩充数据量，但需注意过滤低质量样本以避免噪声干扰。
数据划分必须遵循按程序而非按证明划分的原则。若同一程序的多个证明样本同时出现在训练集和测试集中，模型可能通过 “记住程序” 而非 “学习验证逻辑” 来通过测试，导致评估结果虚高。推荐的划分比例为训练集 70%–80%、验证集 10%–15%、测试集 10%–15%，且测试集应包含分布外样本以评估模型的泛化能力。
损失函数设计：从交叉熵到验证器奖励
损失函数的选择决定了模型优化的直接目标，也影响着模型输出的分布特性与验证通过率。ML 程序验证器的损失函数设计需要在可微分的代理损失与基于验证器的离散奖励之间找到平衡。
Token 级交叉熵是最基础的训练目标。在教师强制模式下，模型基于输入程序与标准答案的 token 序列计算负对数似然，损失为所有目标 token 的平均交叉熵。为缓解不同长度样本之间的不平衡，可以引入长度归一化 —— 将损失除以目标序列长度或进行长度分桶归一化。实践中，建议对特殊 token（如证明分隔符、逻辑连接符）给予略高的权重，因为这些 token 对验证器的判定具有关键影响。
序列级重加权策略可以根据样本质量动态调整权重。将通过验证器的样本标记为高质量，赋予较高权重；将未通过验证器但接近正确的样本适当降权；对于噪声较大的样本（如自动标注中验证器超时报错的情况），显著降权或直接过滤。这种加权方式可以缓解验证器标注中的噪声问题，但需注意权重不要波动过大导致训练不稳定。
强化学习微调是提升验证成功率的关键阶段。纯监督学习受限于标准答案的唯一性，难以探索多样化的证明路径；而强化学习可以让模型自主探索可能通过验证的证明。一种常见的做法是以验证器作为奖励函数：若生成的证明通过验证，奖励为 1；否则为 0（或负值）。更精细的设计可以采用分级奖励 —— 根据证明义务被满足的比例、验证耗时或部分进展给予部分奖励。训练时通常采用 REINFORCE 或 PPO 算法，在交叉熵预训练模型的基础上进行策略优化。
复合损失在实际训练中更为常见。例如，将交叉熵损失与验证器奖励的期望通过加权系数组合：$\mathcal {L} = \mathcal {L}_{\text {CE}} - \lambda \cdot \mathbb {E}[\text {reward}]$，其中 $\lambda$ 控制稳定性和奖励最大化之间的权衡。此外，加入 KL 散度项以限制策略接近原始预训练模型，可以避免模型 collapse 到退化解（如同义反复的平凡证明）。
判别式任务的损失函数适用于对候选证明打分的场景。二元交叉熵用于区分可通过验证与不可通过的候选；成对排序损失（margin ranking loss）确保对于同一程序，通过验证的候选得分高于未通过的；回归损失（Huber 损失或 MSE）则用于预测软标签，如证明义务满足比例或验证耗时。
超参数调优：成本感知的两阶段策略
由于每次验证器调用都涉及昂贵的形式化证明搜索，超参数调优必须采用成本感知的策略，避免在验证器调用上产生过高的开销。
关键超参数可以分为四类：模型架构类（隐藏维度、层数、注意力头数，若从头训练）；优化器类（学习率及其预热步数与衰减策略、梯度裁剪阈值、权重衰减系数）；任务相关类（输入 / 输出的最大 token 长度、损失权重、RL 阶段每样本采样的候选数、验证器超时时间）；训练调度类（批量大小、梯度累积步数、训练轮次、早停阈值）。
两阶段调优策略被证明是成本与效果之间的良好折中。第一阶段为离线 cheap 阶段：在固定的子集上使用离线指标（如 token 级准确率、验证集困惑度）进行超参数搜索，不调用验证器。此阶段可以使用随机搜索或贝叶斯优化，在较大的超参数空间内快速筛选。推荐的搜索范围包括学习率（1e-5 至 1e-3）、批量大小（8 至 64）、权重_decay（0.01 至 0.1）、dropout（0.1 至 0.3）。第二阶段为在线 expensive 阶段：选取 top-k（通常 3–5 个）配置，在完整的验证集上评估基于验证器的指标（如验证成功率、平均验证时间），选取综合表现最优的配置。
早停机制对控制成本至关重要。建议同时监控验证集损失（离线指标）与验证成功率（在线指标），若离线指标连续 N 个 checkpoint（如 5–10）无改善则触发早停；若计算资源允许，同时监控在线指标可以更直接地反映最终性能。实践中，训练初期（epoch 1–3）离线指标下降快但在线指标波动大，此时以离线指标为主；中后期（epoch 4+）两者趋于一致，可增加在线指标的权重。
缓存与分层验证是进一步降低成本的有效手段。对相同或等价的候选证明进行结果缓存，避免重复调用验证器；采用分层验证策略 —— 先用轻量级的静态检查或快速 SMT 查询过滤明显不可行的候选，再对保留下来的候选调用完整的形式化验证器。
训练流程与课程学习
完整的训练流程通常包含三个阶段：预训练微调、监督微调与验证器在环的强化学习。
预训练微调阶段从代码或证明导向的预训练模型（如 CodeLlama、StarCoder、GraphCodeBERT）出发，在验证数据集上进行有监督的交叉熵训练。此阶段的目标是让模型学习验证任务的输入输出分布，建议使用较小的学习率（如 2e-5 至 5e-5）以保留预训练知识，训练 3–10 个 epoch。
课程学习策略可以提升训练效率与最终性能。从较简单、较短的程序开始训练，随着训练的推进逐步引入更复杂、证明更长的样本。简单的程序往往有更直观的不变式与更短的证明路径，模型在此阶段建立基础推理模式后再面对复杂任务，成功率更高。可以按程序规模（代码行数）、证明复杂度（证明步数）或验证耗时对样本排序，形成由易到难的训练队列。
验证器在环的强化学习阶段是提升验证成功率的核心。在此阶段，模型周期性生成一批候选证明，运行验证器获取奖励或新标签，然后基于这些反馈更新模型参数。实践中需要注意：保持一个经验回放缓冲区，存储历史 epoch 中验证成功的样本，以稳定训练分布； RL 训练轮数通常不宜过长（10–50 步即可），以避免策略过度拟合特定验证器的行为模式；加入多样性惩罚，鼓励模型生成结构不同的证明，避免仅探索少数几条 “捷径”。
评估指标与训练稳定性监控
评估 ML 验证器需要同时关注模型自身指标与验证器相关指标两类。
模型中心指标包括 token 级准确率、验证集困惑度、BLEU 分数（与标准证明的相似度）以及编辑距离。这些指标反映模型的拟合能力，但不直接代表验证成功率。
验证器中心指标才是最终关注点：验证成功率（生成的证明通过验证的比例）、单程序平均尝试次数（获得首个成功证明所需的生成次数）以及平均验证耗时。Robustness 测试在分布外基准（如不同语言、不同验证器项目）上进行，以评估泛化能力。
训练稳定性方面，需要监控梯度范数（防止梯度爆炸）、token 级损失与序列级奖励的方差（过大说明训练不稳定）、验证成功率曲线（若出现大幅波动需调整学习率或奖励设计）。建议每 500–1000 步记录一次这些指标，形成训练仪表盘以便及时发现异常。
常见陷阱与应对策略
数据泄露是首要避免的问题。确保训练集与测试集中的程序在逻辑上独立，避免因变量重命名、格式化差异导致的隐性泄露。可以在数据预处理阶段使用代码指纹或语义哈希检测重复或近似重复的程序。
过拟合验证器特有行为是另一个常见问题。不同验证器对证明格式、注解风格可能有细微偏好，模型可能学会 “迎合特定验证器” 而非 “生成正确证明”。应对策略包括使用多个验证器变体进行交叉训练、定期人工抽检模型输出、加入证明可读性或语义正确性的辅助约束。
奖励稀疏问题在验证任务中尤为突出 —— 大多数随机生成的候选证明都会失败，导致模型难以获得学习信号。解决思路包括：设计奖励塑形（reward shaping），为接近成功的部分进展提供中间奖励；使用蒙特卡洛树搜索或束搜索引导候选生成，提升初始样本质量；或借助课程学习，先在较简单的验证任务上训练再迁移到复杂任务。
实践参数参考
综合现有经验，以下参数范围可作为工程实践的起点：学习率 1e-5 至 3e-5，批量大小 8 至 32（配合梯度累积），权重衰减 0.01 至 0.1，dropout 0.1 至 0.2，最大输入长度 1024–2048 token，最大输出长度 512–1024 token，验证器超时 5–30 秒 / 样本，RL 阶段每样本候选数 4–16，早停耐心 5–10 个 checkpoint。实际部署时需根据具体验证器性能、硬件资源与目标验证成功率进行微调。
资料来源：RiSE MSR Blog（https://risemsr.github.io）