FormalJudge：用于代理监督的神经符号范式
人工智能
2026-02-13 v2
摘要
随着基于 LLM 的代理在具有真实后果的高风险领域中不断运作，确保其行为的安全性变得至关重要。当前主流的监督范式 LLM-as-a-Judge 面临着一个根本性困境：概率系统如何可靠地监督其他概率系统而不继承其失效模式？我们认为形式化验证提供了原则性的解决方案，但其采纳一直受到一个关键瓶颈的制约：从自然语言需求到形式化规范的翻译。本文通过提出一种神经符号框架，构建了一种双向的 Formal-of-Thought 架构：LLMs 作为规范编译器，自上而下分解高层人类意图为原子、可验证约束，然后自下而上使用 Dafny 规范和 Z3 满足模理论求解进行合规性证明，从而产生数学保证而非概率得分。我们在三个基准测试上进行了验证，涵盖行为安全、跨域约束遵从性和代理上层欺骗检测。7 个 agent 模型的实验表明，FormalJudge 在 LLM-as-a-Judge baseline 上实现了平均 16.6% 的提升，实现了弱到强的泛化，其中 7B judge 能以超过 90% 的准确率检测来自 72B agent 的欺骗行为，并通过迭代细化实现近乎线性的安全性提升。
引用
@article{arxiv.2602.11136,
title = {FormalJudge: A Neuro-Symbolic Paradigm for Agentic Oversight},
author = {Jiayi Zhou and Yang Sheng and Hantao Lou and Yaodong Yang and Jie Fu},
journal= {arXiv preprint arXiv:2602.11136},
year = {2026}
}
备注
27 pages