FormalJudge: 一种用于代理监管的神经符号范式
FormalJudge: A Neuro-Symbolic Paradigm for Agentic Oversight
AI总结：
FormalJudge通过神经符号框架结合形式验证，提升代理行为安全性和欺骗检测能力，实现数学保证而非概率评分。
摘要：
随着基于大语言模型（LLM）的代理在高风险领域中日益广泛地应用于现实世界，确保其行为安全变得至关重要。主流的监管范式，即LLM-as-a-Judge，面临一个根本性的困境：如何让概率系统可靠地监管其他概率系统而不继承其失败模式？我们主张形式验证提供了一种原理性的解决方案，但其采用受到一个关键瓶颈的阻碍：自然语言要求到形式规范的翻译。本文通过提出，一种神经符号框架，采用双向的Formal-of-Thought架构：LLM作为规范编译器，自上而下地将高层次的人类意图分解为可验证的原子约束，然后自下而上地使用Dafny规范和Z3可满足性模理论求解器证明合规性，从而产生数学保证而非概率分数。我们通过三个涵盖行为安全、多领域约束遵守和代理向上欺骗检测的基准测试进行了验证。在7个代理模型上的实验表明，实现了相对于LLM-as-a-Judge基线的平均提升16.6%，实现了弱到强的泛化，其中7B的判官在检测72B代理的欺骗时达到90%以上的准确率，并通过迭代优化提供近线性的安全提升。
英文摘要：
As LLM-based agents increasingly operate in high-stakes domains with real-world consequences, ensuring their behavioral safety becomes paramount. The dominant oversight paradigm, LLM-as-a-Judge, faces a fundamental dilemma: how can probabilistic systems reliably supervise other probabilistic systems without inheriting their failure modes? We argue that formal verification offers a principled escape from this dilemma, yet its adoption has been hindered by a critical bottleneck: the translation from natural language requirements to formal specifications. This paper bridges this gap by proposing , a neuro-symbolic framework that employs a bidirectional Formal-of-Thought architecture: LLMs serve as specification compilers that top-down decompose high-level human intent into atomic, verifiable constraints, then bottom-up prove compliance using Dafny specifications and Z3 Satisfiability modulo theories solving, which produces mathematical guarantees rather than probabilistic scores. We validate across three benchmarks spanning behavioral safety, multi-domain constraint adherence, and agentic upward deception detection. Experiments on 7 agent models demonstrate that achieves an average improvement of 16.6% over LLM-as-a-Judge baselines, enables weak-to-strong generalization where a 7B judge achieves over 90% accuracy detecting deception from 72B agents, and provides near-linear safety improvement through iterative refinement.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
