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

FormalJudge: A Neuro-Symbolic Paradigm for Agentic Oversight

대규모 언어 모델(LLM) 기반 에이전트가 실제 세계의 중요한 영역에서 점점 더 많이 사용됨에 따라, 에이전트의 안전한 행동을 보장하는 것이 매우 중요해지고 있습니다. 현재 주류인 'LLM-as-a-Judge' 방식은 근본적인 딜레마에 직면합니다. 확률적 시스템이 다른 확률적 시스템을 어떻게 신뢰성 있게 감독할 수 있을까요? 그렇지 않으면, 원 시스템의 오류 모드를 그대로 답습하게 될 위험이 있습니다. 본 논문에서는 형식적 검증이 이러한 딜레마에서 벗어날 수 있는 원칙적인 방법을 제공한다고 주장하지만, 자연어 요구 사항을 형식적 명세로 변환하는 중요한 기술적 장벽으로 인해 그 활용이 제한되어 왔습니다. 본 논문은 'FormalJudge'라는 신경-기호 통합 프레임워크를 제안하여 이러한 격차를 해소합니다. FormalJudge는 양방향 'Formal-of-Thought' 아키텍처를 활용합니다. LLM은 고수준의 인간 의도를 원자적이고 검증 가능한 제약 조건으로 분해하는 명세 컴파일러 역할을 하며, Dafny 명세와 Z3 SAT 솔버를 사용하여 하향식으로 준수 여부를 증명합니다. 이를 통해 확률적 점수 대신 수학적 보장을 제공합니다. 본 논문에서는 행동 안전, 다중 영역 제약 조건 준수, 에이전트의 기만 행위 탐지와 관련된 세 가지 벤치마크를 통해 FormalJudge의 성능을 검증했습니다. 7가지 에이전트 모델에 대한 실험 결과, FormalJudge는 기존의 'LLM-as-a-Judge' 방식에 비해 평균 16.6%의 성능 향상을 보였으며, 70억 파라미터의 판단 모델이 720억 파라미터의 에이전트의 기만 행위를 90% 이상의 정확도로 탐지하는 일반화 능력을 보여주었습니다. 또한, 반복적인 개선을 통해 거의 선형적인 안전성 향상을 달성할 수 있었습니다.

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.