FormalJudge: A Neuro-Symbolic Paradigm for Agentic Oversight

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.

This paper studies how to check whether AI agents behave safely and honestly after they complete a task. Today, many systems use another large language model as a judge, but this can be unreliable because both the agent and the judge may make similar mistakes or be persuaded by convincing but false explanations. We propose FormalJudge, a method that breaks a task into simple yes-or-no checks and then uses formal logic software to combine those checks into a final decision. This makes the judging process more transparent and easier to inspect when something goes wrong. Across several agent safety and deception benchmarks, FormalJudge detects unsafe or deceptive behavior more accurately than standard language-model judges, especially when weaker judges need to evaluate stronger agents.