FormalJudge：面向Agentic监督的神经符号范式

摘要

随着基于 LLM 的智能体日益在具有现实后果的高风险领域运行，确保其行为安全变得至关重要。主导性的监督范式 LLM-as-a-Judge 面临一个根本困境：概率系统如何能在不继承其失败模式的前提下可靠地监督其他概率系统？我们主张，形式化验证为摆脱这一困境提供了有原则的出路，但其采用一直受制于一个关键瓶颈：从自然语言需求到形式化规约的转换。本文通过提出 FormalJudge 来弥合这一缺口——一个神经符号框架，采用双向的 Formal-of-Thought 架构：LLM 充当规约编译器，自顶向下将高层人类意图分解为原子化、可验证的约束，再自底向上使用 Dafny 规约和 Z3 可满足性模理论（Satisfiability Modulo Theories，SMT）求解来证明合规性，从而产生数学保证而非概率分数。我们在涵盖行为安全、多领域约束遵循和智能体向上欺骗检测的三个基准上进行验证。在 7 个智能体模型上的实验表明，FormalJudge 相比 LLM-as-a-Judge 基线平均提升 16.6%，实现弱到强泛化——7B 判别模型检测 72B 智能体欺骗的准确率超过 90%，并通过迭代细化提供近线性的安全提升。

FormalJudge：面向Agentic监督的神经符号范式 — 图1：引子：LLM 智能体面临可扩展监督（scalable oversight）挑战：难以确定一个可靠的监督智能体。LLM-as-a-Judge 基线依赖概率性的思维链（Chain-of-Thought）推理，而我们提出了一种 Formal-of-Thought 架构，将 LLM 用作规范编译器（specification compiler）。它将智能体轨迹分解为由 SMT 求解器验证的原子事实，从而提供数学意义上的正确性证明而非主观评分。通过将神经语义抽取与确定性逻辑验证分离，该系统确保监督不受说服性操纵的影响。