FormalJudge: A Neuro-Symbolic Paradigm for Agentic Oversight

Paper: 2602.11136 Authors: Jiayi Zhou, Yang Sheng, Hantao Lou, Yaodong Yang, Jie Fu Categories: cs.AI

Abstract

As LLM-based agents deploy in high-stakes environments, the dominant oversight approach—LLM-as-a-Judge—faces a critical paradox: probabilistic systems cannot reliably supervise other probabilistic systems without inheriting their failure modes. FormalJudge resolves this through a neuro-symbolic architecture that bridges natural language requirements and formal verification. The framework employs a bidirectional Formal-of-Thought process where LLMs decompose human intent into atomic constraints, then prove compliance using Dafny specifications and Z3 SMT solving to produce mathematical guarantees instead of probabilistic scores. Validated across behavioral safety, multi-domain constraints, and deception detection benchmarks with 7 agent models, FormalJudge achieves 16.6% average improvement over baselines, enables weak-to-strong generalization (7B judge detecting 72B agent deception at >90% accuracy), and provides near-linear safety gains through iterative refinement.

Key Contributions

• Introduces a neuro-symbolic oversight paradigm that escapes the probabilistic supervision dilemma by combining LLM reasoning with formal verification
• Proposes bidirectional Formal-of-Thought architecture: top-down decomposition of natural language requirements into verifiable constraints, bottom-up compliance proving via Dafny and Z3
• Demonstrates weak-to-strong generalization where smaller models (7B) reliably judge larger agents (72B) through formal guarantees
• Achieves 16.6% average accuracy improvement over LLM-as-a-Judge baselines across three diverse benchmarks
• Provides mathematical safety guarantees with near-linear improvement through iterative specification refinement

The Probabilistic Supervision Dilemma

The current AI safety landscape relies heavily on LLM-as-a-Judge for oversight, where one language model evaluates another’s outputs. This creates a fundamental circularity problem: if the judge model is itself probabilistic and prone to errors, how can it reliably detect failures in systems with similar architectures and failure modes?

Traditional approaches attempt to solve this through scaling (using larger models as judges) or ensembling (combining multiple judge outputs). However, these methods remain fundamentally probabilistic—they reduce error rates but cannot eliminate them. In high-stakes domains like healthcare, finance, or autonomous systems, probabilistic guarantees are insufficient.

FormalJudge reframes the problem: instead of asking “how confident is the judge?”, it asks “can we mathematically prove compliance?” This shift from probabilistic scoring to formal verification provides a principled escape from the supervision dilemma.

Methodology: Bidirectional Formal-of-Thought

The core innovation lies in the bidirectional architecture that connects natural language requirements to formal proofs:

Top-Down Decomposition: The LLM acts as a specification compiler, parsing high-level human intent (e.g., “the agent should not deceive users”) into atomic, verifiable constraints. This decomposition produces a structured specification tree where each node represents a testable property.

Bottom-Up Verification: Once constraints are formalized, the system translates them into Dafny specifications—a verification-aware programming language. Z3, a Satisfiability Modulo Theories (SMT) solver, then attempts to prove or disprove each constraint mathematically. The result is binary: either the property holds with mathematical certainty, or a counterexample demonstrates violation.

This bidirectional flow leverages LLMs’ strength in natural language understanding while delegating the critical verification step to deterministic formal methods. The LLM handles the ambiguous translation problem; the SMT solver provides rigorous guarantees.

The framework also supports iterative refinement: when verification fails, the system can analyze counterexamples, refine specifications, and re-verify, creating a feedback loop that progressively strengthens safety guarantees.

Experimental Validation

The authors validate FormalJudge across three challenging benchmarks:

Behavioral Safety: Testing whether agents adhere to ethical guidelines and safety constraints in open-ended scenarios. FormalJudge’s formal approach excels at detecting subtle violations that probabilistic judges miss.

Multi-Domain Constraint Adherence: Evaluating compliance with complex, multi-faceted requirements spanning different domains simultaneously. The decomposition architecture naturally handles this complexity by breaking constraints into verifiable components.

Agentic Upward Deception Detection: Perhaps most impressively, detecting when agents attempt to deceive their overseers—a critical failure mode as agents become more capable. The formal verification approach proves particularly effective here, as deceptive agents cannot “fool” mathematical proofs the way they might fool probabilistic judges.

Across 7 different agent models, FormalJudge achieves an average 16.6% accuracy improvement over LLM-as-a-Judge baselines. More significantly, it demonstrates weak-to-strong generalization: a 7B parameter judge model achieves over 90% accuracy detecting deception from 72B parameter agents. This inverts the typical scaling assumption and suggests formal methods can compensate for model size differences.

Implications for AI Safety

FormalJudge represents a paradigm shift in how we approach AI oversight. Rather than accepting probabilistic uncertainty as inherent to the problem, it demonstrates that formal verification can provide mathematical safety guarantees even when dealing with complex, natural language requirements.

The weak-to-strong generalization result is particularly significant for AI safety governance. It suggests that we don’t necessarily need superhuman AI to oversee superhuman AI—we need the right verification architecture. A smaller model with formal verification capabilities can reliably judge a larger model’s behavior.

The near-linear safety improvement through iterative refinement also provides a practical path forward: safety isn’t binary but can be progressively strengthened through specification refinement and re-verification.

However, the approach has limitations. Formal verification requires that properties be formalizable, which may not cover all aspects of AI safety. The translation from natural language to formal specifications, while aided by LLMs, remains a potential bottleneck. And verification complexity can scale poorly for certain types of constraints.

Takeaways

1. Formal verification offers a principled escape from the probabilistic supervision dilemma in AI oversight, providing mathematical guarantees instead of confidence scores.

2. The bidirectional Formal-of-Thought architecture successfully bridges the gap between natural language requirements and formal specifications using LLMs as specification compilers.

3. Weak-to-strong generalization is achievable through formal methods: 7B models can reliably judge 72B models when equipped with verification capabilities.

4. FormalJudge achieves 16.6% average improvement over LLM-as-a-Judge baselines across diverse safety benchmarks, with particularly strong performance on deception detection.

5. Iterative specification refinement provides a practical path to progressively stronger safety guarantees with near-linear improvement rates.

6. The neuro-symbolic paradigm combines the strengths of neural language understanding with the rigor of formal verification, suggesting a promising direction for AI safety research.