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.

翻译：随着基于大语言模型的智能体日益在具有现实世界影响的高风险领域运行，确保其行为安全性变得至关重要。当前主流的监督范式"LLM-as-a-Judge"面临一个根本性困境：概率系统如何能可靠地监督其他概率系统，而不继承其失效模式？我们认为形式化验证为这一困境提供了原则性解决方案，但其应用一直受制于一个关键瓶颈：从自然语言需求到形式化规约的转换。本文通过提出FormalJudge来弥合这一鸿沟，该神经符号框架采用双向形式化思维架构：大语言模型作为规约编译器，自上而下地将高层人类意图分解为原子化、可验证的约束，随后自下而上地利用Dafny规约和Z3可满足性模理论求解器证明合规性，从而产生数学保证而非概率评分。我们在涵盖行为安全、多领域约束遵循和智能体上行欺骗检测的三个基准测试中验证FormalJudge。对7种智能体模型的实验表明，相较于LLM-as-a-Judge基线，FormalJudge平均提升16.6%的性能，实现了弱到强泛化（7B参数的裁判模型检测72B智能体欺骗行为的准确率超过90%），并通过迭代优化提供接近线性的安全性提升。