FormalJudge: 에이전트 감독을 위한 신경-기호적 패러다임

FormalJudge: A Neuro-Symbolic Paradigm for Agentic Oversight

LLM 기반 에이전트가 실제 세계에 영향을 미치는 고위험 영역에서 점차 더 많이 활용됨에 따라, 이들의 행동 안전성을 보장하는 것이 무엇보다 중요해지고 있습니다. 지배적인 감독 패러다임인 '심판으로서의 LLM(LLM-as-a-Judge)'은 근본적인 딜레마에 직면해 있습니다. 즉, 확률적 시스템이 어떻게 자신의 오류 가능성을 답습하지 않으면서 다른 확률적 시스템을 신뢰성 있게 감독할 수 있는가 하는 문제입니다. 우리는 정형 검증(formal verification)이 이러한 딜레마에서 벗어날 수 있는 원칙적인 해결책을 제공한다고 주장하지만, 자연어 요구사항을 정형 명세로 변환하는 과정의 결정적인 병목 현상으로 인해 그 도입이 지연되어 왔습니다. 본 논문은 양방향 'Formal-of-Thought' 아키텍처를 사용하는 신경-기호적 프레임워크인 FormalJudge를 제안하여 이러한 격차를 해소합니다. LLM은 명세 컴파일러 역할을 하여 하향식으로 고차원적인 인간의 의도를 검증 가능한 원자 단위의 제약 조건으로 분해한 다음, Dafny 명세와 Z3 SMT(Satisfiability Modulo Theories) 솔버를 사용하여 상향식으로 준수 여부를 증명함으로써 확률적 점수 대신 수학적 보증을 산출합니다. 우리는 행동 안전성, 다중 도메인 제약 조건 준수, 에이전트의 상향 기만 탐지를 아우르는 세 가지 벤치마크를 통해 FormalJudge를 검증합니다. 7개의 에이전트 모델에 대한 실험 결과, FormalJudge는 LLM-as-a-Judge 베이스라인 대비 평균 16.6%의 성능 향상을 달성했습니다. 또한 7B 파라미터의 심판 모델이 72B 에이전트의 기만을 90% 이상의 정확도로 탐지하는 '약에서 강으로의 일반화(weak-to-strong generalization)'를 가능하게 하며, 반복적인 개선을 통해 거의 선형적인 안전성 향상을 제공함을 입증했습니다.

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.