SEVerA：自演化智能体的可验证合成 SEVerA: Verified Synthesis of Self-Evolving Agents

完整流程在 Algorithm 2 中给出，输入是 $I = (F, A, L, D, \Phi, \Psi, \mathcal{I})$，其中 $F = F_c \cup F_p$ 是非参数库函数与参数化模型的集合，$A$ 是库函数的一阶逻辑公理（如 $pow$ 的单调性、$noDiff$ 的自反性），$L$ 是任务损失，$D$ 是训练集，$(\Phi, \Psi)$ 是行为规约，$\mathcal{I}$ 是给规划 LLM 的任务文字描述。 (1) **Search 阶段**：规划 LLM $L_p$ 先按 Eq.15 的语法定义若干 FGGM $G = \{G_1, ..., G_m\}$，每个 FGGM 给出提示程序 $f_p$（把输入构造成 LLM prompt）和回退程序 $f_d$；然后在 Dafny 受限子集中采样参数化候选程序 $P\{\Theta\}$，其中参数集 $\{\Theta\}$ 是 $F_p$ 中所有可优化参数。 (2) **Verify 阶段**：SEVerA 用 `validateFGGM` 检查每个 FGGM 的良构性：$f_p$、$f_d$ 必须类型正确且终止，$f_d$ 必须被 $VC[\Phi_l, \Psi_l]$ 验证通过。检查通过后，将 $G$ 及其局部契约 $(\Phi_{l,i}, \Psi_{l,i})$ 注入验证上下文 $C' = (G_D, F \cup G, A \cup A_G)$，再用 `validateProgram` 走一遍 $PC$（语法）、$TC$（终止性）、$VC[\Phi, \Psi]$（行为规约）三道关。任一失败则把错误信息回送给 $L_p$ 进入 CEGIS 循环下一轮（预算 $\delta$ 轮内）。验证成功则由 Theorem 5.3 保证 $P\{\Theta\}$ 在所有参数取值下都满足 $(\Phi, \Psi)$。 (3) **Learn 阶段**：把已验证的 $P\{\Theta\}$ 用 Dafny 自带 transpiler 转成 Python，对底层生成模型做无约束梯度优化。损失函数为 Eq.21：全局任务损失 $\sum_{(x,y) \in D} L(x, y, P(x)) + \lambda \sum_{i \in k} L^{\Phi_l, \Psi_l}_i(\theta_i)$，其中第二项是 FGGM 局部契约合规损失（Eq.20：$L^{\Phi_l, \Psi_l}(\theta) = \frac{1}{|P|} \sum_{p \in P} E_{y \sim L_\theta(p)}[1 - \mathbb{I}(c_{\Phi_l, \Psi_l}(x, y))]$，即采样不通过判定器的期望比例）。对 LLM 这种大模型，作者用各 FGGM 之间参数独立的事实（局部合规损失只依赖该 FGGM 的输入输出）做模块化近似（Eq.22），并用 GRPO 训练：奖励 $R(p, y_l) = 1 - sigmoid(L(x, \_, y)\cdot \mathbb{I}(y=y_l) + \lambda (1 - \mathbb{I}(c(p, y_l))))$，把'任务错'与'契约违'都打成低分。闭源模型跳过 Learn，只靠 $f_p$ 改进。 (4) **外层循环与候选池**：把调好的 $P^*\{\Theta\}$ 加进池 $P$，并用其对 $D$ 的执行轨迹构造反馈 $\mathcal{I}'$（附录P）送给规划 LLM，让它在'前序版本哪里跑挂了'的提示下提议新候选。预算 $\Delta$ 用尽后从池中挑任务损失最低的作为最终 $f^*$。Theorem 5.4 给出全局正确性：$f^* \neq \perp \Rightarrow \forall x. \Phi(x) \Rightarrow \Psi(x, f^*(x))$。Theorem 5.5 进一步证明：在 $L$ 对违约输出更敏感、$\Psi$ 无量词、存在非参回退 $f_d$ 三个温和条件下，搜索空间里一定存在一个 $f$ 满足硬约束且任务损失不高于任何带初始参数的裸生成模型。

在概念层面，本文首次把'形式化行为规约'和'自演化智能体训练'用一个通用、可验证、可训练的中间层 FGGM 衔接起来，这一组合在先前任何工作中都没有出现过。与约束解码相比，FGGM 不改模型解码器、可以套在闭源 LLM 上、契约可用一阶逻辑而非 CFG；与运行时监控（Agent-C）相比，FGGM 在合成时一次性证明对所有输入和参数都安全，而非只能检查已观测到的执行轨迹；与传统演绎式程序合成相比，SEVerA 允许程序内嵌可训练的 LLM，并通过 FGGM 把'合成的程序必须确定性正确'放宽为'可训练组件在 verified fallback 守护下参数独立正确'。在工程层面，'违反率 0% + 任务性能反而提升'这一组合本身也是反直觉的——传统认知是'加约束 = 牺牲性能'，本文用 Theorem 5.5 给出理论解释（约束把低质量候选剪掉，引导搜索聚焦高质量候选），再用四个任务的实验数据佐证。Theoretical soundness（Theorem 5.3/5.4）和 sufficient success condition（Theorem 5.5）也共同构成了'为什么能 work'的完整论证链。

**（1）回退程序的可用性瓶颈**。当前 $f_d$ 必须由规划 LLM 写出且通过验证——这等于把'契约'翻译成'显式程序'的负担压回 LLM。对于'退款金额不得超过原始票价'这类数值约束，LLM 写出 min/max 类的 $f_d$ 容易；但对于'对话策略中'已'至少提示过用户确认'这种状态约束，$f_d$ 可能写不出来或写出来任务能力退化严重。改进方向：让 SEVerA 内置一组常用'安全壳'库（如常见业务规则模板），由用户在配置里直接挂载而不是每题让 LLM 写。**（2）拒绝采样预算 $K$ 是固定常数**。$K=5$ 对容易违规的 prompt 来说可能不够——在 5 次内采不到合规样本就回退，可能错失 LLM 偶尔但有价值的合规输出。改进方向：把 $K$ 改为基于 LLM 当前合规率的动态值，或者允许 $K$ 触发多个 FGGM 的级联回退。**（3）FGGM 间的参数不共享**。同一 LLM 在程序中不同位置被调用，作者目前给每个位置一个独立 $\theta$，重复了参数空间。改进方向：引入位置感知的参数绑定（同一 GM 在不同位置共享 backbone，只在 adapter 层不同），并把这一约束也编码进 $\Psi$。**（4）GRPO 训练在多轮工具调用上没扩展**。$\tau^2$-bench 跳过 Learn 限制了真正的'self-evolving'在长程任务上的体现。改进方向：分层 GRPO，先对每个 FGGM 单独做局部 GRPO，再在端到端任务奖励上做 PPO-style 精调。**（5）搜索终止条件过于硬性**。当搜索预算 $\delta$ 用尽时直接抛弃当前候选，浪费了已收集的执行反馈。改进方向：把'部分验证 + 局部契约'的候选也暂存到池里，在 Learn 阶段通过修改 $\Phi, \Psi$ 重新评估。**（6）verification 的墙钟开销**。在 DafnyBench 上 2.5× 时间放大主要来自 SMT 求解超时；对工业级程序可能更糟。改进方向：把'快速路径'（如基于类型系统的 lightweight 静态检查）放在 $VC$ 之前做初筛。

**作者明确点出的方向**：(1) 把资源预算（token 数、调用次数、墙钟时间）作为额外硬约束嵌入 FGGM，让 SEVerA 变成 resource-aware 的合成框架；(2) 引入 FGGM 调用间的参数共享与调用次数上限，降低学习成本。**可延伸的方向**：(3) 把 SEVerA 推广到除 Dafny 之外的验证感知语言（如 F*、Coq、Lean），让行为规约的表达力与生态进一步扩展；(4) 把 FGGM 的局部契约从'一阶逻辑'升级为'时序逻辑'（LTL/CTL），直接表达多步交互规约，对应 $\tau^2$-bench 等需要长程策略合规的任务；(5) 用 LLM 自动发现库函数公理 $A$（目前需用户手写），减少人工 setup 成本；(6) 把 SEVerA 框架中的'约束分解'思想（local+global loss 联合）独立抽出，研究其在多任务 RLHF 中的通用性；(7) 探索在 SEVerA 验证失败时如何把 SMT 反例直接转成自然语言反馈给规划 LLM，进一步降低 CEGIS 循环的轮数。

**代码与数据**：作者声明代码开源在 GitHub（具体链接论文给出）。**算力**：所有实验在 NVIDIA A100 40GB GPU 上跑——对 LLM 微调来说是中等消费级配置，学术实验室可承担。**实现依赖**：依赖 Dafny 编译器/验证器、Python transpiler、Z3-style SMT solver（如 CVC5）、PyTorch、GRPO/LoRA 训练栈（作者用 Qwen3-8B）、Agent-C 的 LTL 策略编码器。**复现难度**：中等偏上。**优势**：(a) 任务基准（HumanEvalDafny、DafnyBench、GSM-Symbolic、$\tau^2$-bench、SymReg）都是公开数据集；(b) 框架输入接口 $I = (F, A, L, D, \Phi, \Psi, \mathcal{I})$ 形式化清晰；(c) 规划 LLM 提示模板、$\mathcal{I}'$ 反馈构造规则都在附录 Q、P 中给出。**门槛**：(a) 用户必须为每个新任务手写公理 $A$（如 $pow$ 的单调性），这是显著的人力开销；(b) FGGM 内的 $f_d$ 需要规划 LLM 自写且能被 Dafny 验证，'什么算合格的回退'对新手不直观；(c) Dafny 转 Python 的 transpiler 仅对受限子集可靠，扩展到完整 Dafny 后正确性未经验证；(d) 复现 Table 5/6 的符号回归结果需要 35 个 ground-truth 函数 + 两档噪声的 600 训练 + 400 测试集，配置成本不低。**复现建议**：先在 $\tau^2$-bench 复现，因为只用 Qwen3-8B 推理、不需要学习阶段，门槛最低；再在 GSM-Symbolic 上跑通 GRPO 微调；Dafny 和 SymReg 留作后续。