VERGE: 검증 가능한 LLM 추론을 위한 형식적 정제 및 안내 엔진

VERGE: Formal Refinement and Guidance Engine for Verifiable LLM Reasoning

대규모 언어 모델(LLM)은 문법적으로 유창하지만, 고위험 영역에서 그 논리적 정확성을 보장하는 것은 여전히 근본적인 과제입니다. 본 논문에서는 LLM과 SMT 솔버를 결합하여 반복적인 정제를 통해 검증 기반 답변을 생성하는 신경-기호 프레임워크를 제시합니다. 저희의 접근 방식은 LLM의 출력을 원자적 주张으로 분해하고, 이를 1차 논리로 자동 형식화한 다음, 자동 정리 증명을 사용하여 그 논리적 일관성을 검증합니다. 저희는 다음 세 가지 주요 혁신을 소개합니다: (1) 형식적 의미 동등성 검사를 통한 다중 모델 합의를 통해 후보 간의 논리 수준 정렬을 보장하고, 표면 형식 메트릭의 문법적 편향을 제거합니다. (2) 의미적 라우팅을 통해 다양한 유형의 주张을 적절한 검증 전략으로 안내합니다. 즉, 논리적 주张에는 기호 솔버를 사용하고, 상식 추론에는 LLM 앙상블을 사용합니다. (3) 최소 수정 집합(MCS)을 통해 정확한 논리적 오류 위치를 파악하고, 이분법적인 실패 신호를 실행 가능한 피드백으로 변환합니다. 저희의 프레임워크는 주张을 그 논리적 상태에 따라 분류하고, 여러 검증 신호를 통합하여 분산 기반의 패널티를 적용한 통합 점수를 산출합니다. 시스템은 수용 기준이 충족되거나 수렴될 때까지 구조화된 피드백을 사용하여 답변을 반복적으로 개선합니다. 이 하이브리드 접근 방식은 가능한 경우 형식적인 보장을 제공하고, 그렇지 않은 경우에는 합의 기반 검증을 통해 신뢰할 수 있는 AI를 발전시킵니다. 저희는 GPT-OSS-120B 모델을 사용하여 VERGE가 추론 벤치마크 세트에서 단일 패스 접근 방식에 비해 평균 18.7%의 성능 향상을 달성함을 보여주었습니다.

Despite the syntactic fluency of Large Language Models (LLMs), ensuring their logical correctness in high-stakes domains remains a fundamental challenge. We present a neurosymbolic framework that combines LLMs with SMT solvers to produce verification-guided answers through iterative refinement. Our approach decomposes LLM outputs into atomic claims, autoformalizes them into first-order logic, and verifies their logical consistency using automated theorem proving. We introduce three key innovations: (1) multi-model consensus via formal semantic equivalence checking to ensure logic-level alignment between candidates, eliminating the syntactic bias of surface-form metrics, (2) semantic routing that directs different claim types to appropriate verification strategies: symbolic solvers for logical claims and LLM ensembles for commonsense reasoning, and (3) precise logical error localization via Minimal Correction Subsets (MCS), which pinpoint the exact subset of claims to revise, transforming binary failure signals into actionable feedback. Our framework classifies claims by their logical status and aggregates multiple verification signals into a unified score with variance-based penalty. The system iteratively refines answers using structured feedback until acceptance criteria are met or convergence is achieved. This hybrid approach delivers formal guarantees where possible and consensus verification elsewhere, advancing trustworthy AI. With the GPT-OSS-120B model, VERGE demonstrates an average performance uplift of 18.7% at convergence across a set of reasoning benchmarks compared to single-pass approaches.