A Neuro-Symbolic Paradigm for Agentic Oversight
This repository hosts code and reference material for the paper "FormalJudge: A Neuro-Symbolic Paradigm for Agentic Oversight" by Jiayi Zhou, Yang Sheng, Hantao Lou, Yaodong Yang, and Jie Fu. Release coverage differs by benchmark; see the status table below.
FormalJudge is a neuro-symbolic framework that combines formal verification with large language models for robust agent safety evaluation. Unlike traditional LLM-as-a-Judge approaches, FormalJudge leverages formal specifications (Dafny) to provide verifiable safety guarantees.
The following results are reported in the paper; the status table below describes the available code and reference material.
- 16.6% average improvement over LLM-as-a-Judge baselines across 3 benchmarks and 7 agent models
- Weak-to-strong detection: A 7B judge model achieves >90% accuracy detecting deceptive behaviors from 72B agents
- Stable performance across varying attack sophistication levels
- Near-linear safety improvement through iterative refinement: agents improve from 70.7% to 99.8% accuracy over three rounds with Dafny specification feedback
FormalJudge/
├── AgentSafetyBench/ # Behavioral safety benchmark (available now)
│ ├── data/ # Benchmark dataset
│ ├── environments/ # 350+ agent environment simulators
│ ├── evaluation/ # Agent evaluation framework
│ ├── formal_verification/ # Formal verification pipeline
│ ├── iterative_refinement/ # Iterative refinement with feedback
│ └── score/ # Safety scoring module
├── VitaBench/ # Multi-agent, adversarial, and cross-verifier workflows
└── UpwardDeceivers/ # Deception detection benchmark (coming soon)
| Benchmark | Focus | Status |
|---|---|---|
| AgentSafetyBench | Behavioral safety evaluation | Available |
| VitaBench | Multi-domain constraint adherence | Experiment workflows and data examples |
| UpwardDeceivers | Deception detection | Coming soon |
The VitaBench directory provides multi-agent, adversarial, and cross-verifier workflows with shared prompts, data examples, and model/Dafny adapters. See its README for entry points and configurations.
pip install -r AgentSafetyBench/requirements.txtcd AgentSafetyBench/evaluation
bash eval.shcd AgentSafetyBench/formal_verification
bash scripts/run_dafny.shcd AgentSafetyBench/iterative_refinement
bash run_api_refinement.sh claude-opus-4-5 3 8 dafnyThe AgentSafetyBench implementation provides a hierarchical 3-agent pipeline for formal verification:
- Agent #1 (NL Decomposition): Breaks down high-level safety requirements into verifiable sub-properties
- Agent #2 (Formal Translation): Translates requirements into Dafny/Python/NL specifications
- Agent #3 (Trace Abstraction): Extracts concrete values from agent execution traces
- Executor: Compiles and runs formal verification to produce YES/NO verdicts
The VitaBench pipeline uses a hybrid workflow combining formal evidence, semantic assessment, and LLM aggregation.
dafny: Full formal verification with Dafny specificationspython: Python-based verification (without formal proofs)natural_language: Natural language judgmentllm_cot: LLM with chain-of-thought reasoningllm_fewshot: LLM with few-shot examples
FormalJudge supports evaluation of multiple agent models:
API Models: Claude (Opus, Sonnet), GPT-4/5, Gemini, DeepSeek
Local Models: Qwen (7B-72B), Llama 3, GLM-4
Jiayi Zhou, Yang Sheng, Hantao Lou, Yaodong Yang, and Jie Fu. FormalJudge: A Neuro-Symbolic Paradigm for Agentic Oversight. arXiv:2602.11136, 2026.
This project is released under the MIT License. See individual benchmark directories for specific licensing information.