FormalJudge: a neuro-symbolic paradigm for agent supervision

Researchers propose FormalJudge, a neuro-symbolic framework that uses formal verification to supervise the behavior of LLM agents, replacing the probabilistic scoring of LLM-as-a-Judge with mathematical guarantees. The framework adopts a bidirectional Formal-of-Thought architecture: the LLM first decomposes high-level human intent top-down into atomic verifiable constraints, then bottom-up proves compliance using Dafny specifications and Z3 SMT solving. Experiments on 7 agent models across three benchmarks covering behavioral safety, multi-domain constraint adherence, and detection of upward deception by agents show that FormalJudge improves by an average of 16.6% over the LLM-as-a-Judge baseline; a 7B discriminator model detects deception by a 72B agent with over 90% accuracy, showing weak-to-strong generalization; iterative refinement yields near-linear safety improvements.