# FormalJudge: A Neuro-Symbolic Paradigm for Agentic Oversight

arXiv: https://arxiv.org/abs/2602.11136 · HTML: https://mlsanity.com/paper/2602.11136/

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- Placed in General LLM agent frameworks and benchmarks, one of 16 directions in LLM agents and tool use.
- Builds on 30 of its 45 references that are in the map.
- First posted on arXiv 11 Feb 2026.

## Placed in

- LLM agents and tool use / [General LLM agent frameworks and benchmarks](https://mlsanity.com/agents/general-llm-agent-frameworks-and-benchmarks/)

## Builds on (most cited first, 30 of 30)

- [GPT-4 Technical Report](https://mlsanity.com/paper/2303.08774/) (2023)
- [Chain-of-Thought Prompting Elicits Reasoning in Large Language Models](https://mlsanity.com/paper/2201.11903/) (2022)
- [Qwen3 Technical Report](https://mlsanity.com/paper/2505.09388/) (2025)
- [ReAct: Synergizing Reasoning and Acting in Language Models](https://mlsanity.com/paper/2210.03629/) (2022)
- [Reflexion: Language Agents with Verbal Reinforcement Learning](https://mlsanity.com/paper/2303.11366/) (2023)
- [On the Opportunities and Risks of Foundation Models](https://mlsanity.com/paper/2108.07258/) (2021)
- [G-Eval: NLG Evaluation using GPT-4 with Better Human Alignment](https://mlsanity.com/paper/2303.16634/) (2023)
- [A Survey on Large Language Model based Autonomous Agents](https://mlsanity.com/paper/2308.11432/) (2023)
- [Survey of Hallucination in Natural Language Generation](https://mlsanity.com/paper/2202.03629/) (2022)
- [SelfCheckGPT: Zero-Resource Black-Box Hallucination Detection for Generative Large Language Models](https://mlsanity.com/paper/2303.08896/) (2023)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [LLMs-as-Judges: A Comprehensive Survey on LLM-based Evaluation Methods](https://mlsanity.com/paper/2412.05579/) (2024)
- [Logic-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning](https://mlsanity.com/paper/2305.12295/) (2023)
- [Self-Diagnosis and Self-Debiasing: A Proposal for Reducing Corpus-Based Bias in NLP](https://mlsanity.com/paper/2103.00453/) (2021)
- [Agent-SafetyBench: Evaluating the Safety of LLM Agents](https://mlsanity.com/paper/2412.14470/) (2024)
- [Safety Verification of Deep Neural Networks](https://mlsanity.com/paper/1610.06940/) (2016)
- [AI Alignment: A Comprehensive Survey](https://mlsanity.com/paper/2310.19852/) (2023)
- [Foundational Challenges in Assuring Alignment and Safety of Large Language Models](https://mlsanity.com/paper/2404.09932/) (2024)
- [Mobile-Agent-v3: Fundamental Agents for GUI Automation](https://mlsanity.com/paper/2508.15144/) (2025)
- [LLM Lies: Hallucinations are not Bugs, but Features as Adversarial Examples](https://mlsanity.com/paper/2310.01469/) (2023)
- [Solving Math Word Problems by Combining Language Models With Symbolic Solvers](https://mlsanity.com/paper/2304.09102/) (2023)
- [Agent RL Scaling Law: Agent RL with Spontaneous Code Execution for Mathematical Problem Solving](https://mlsanity.com/paper/2505.07773/) (2025)
- [Large Language Model Safety: A Holistic Survey](https://mlsanity.com/paper/2412.17686/) (2024)
- [Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification](https://mlsanity.com/paper/2404.00762/) (2024)
- [SpecGen: Automated Generation of Formal Program Specifications via Large Language Models](https://mlsanity.com/paper/2401.08807/) (2024)
- [A Survey on the Safety and Security Threats of Computer-Using Agents: JARVIS or Ultron?](https://mlsanity.com/paper/2505.10924/) (2025)
- [The Fusion of Large Language Models and Formal Methods for Trustworthy AI Agents: A Roadmap](https://mlsanity.com/paper/2412.06512/) (2024)
- [Are Your Agents Upward Deceivers?](https://mlsanity.com/paper/2512.04864/) (2025)
- [HERMES: Towards Efficient and Verifiable Mathematical Reasoning in LLMs](https://mlsanity.com/paper/2511.18760/) (2025)
- [Guiding Enumerative Program Synthesis with Large Language Models](https://mlsanity.com/paper/2403.03997/) (2024)

## Built on by (most cited first, 4 of 4)

- [Securing Agentic AI: From Per-Action Checks to Trajectory Assurance](https://mlsanity.com/paper/2608.01558/) (2026)
- [Agents Catching Agents: Shortcut Cascades and Benchmark Gaming in Clinical Multi-Agent Systems](https://mlsanity.com/paper/2608.03744/) (2026)
- [Not Self-Decidable: LLMs Cannot Draw the Boundary of What an Agent Verifier Can Check](https://mlsanity.com/paper/2610.04699/) (2026)
- [Before Agent Tells The Lie: Has Deception Already Been Represented?](https://mlsanity.com/paper/2610.06576/) (2026)

## Abstract (arXiv)

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.