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

초록

대규모 언어 모델(LLM)의 구문적 유창성에도 불구하고, 높은 위험을 수반하는 영역에서 논리적 정확성을 보장하는 것은 근본적인 과제로 남아 있습니다. 본 연구에서는 LLM과 SMT Solver를 결합하여 반복적 정제를 통해 검증 기반 답변을 생성하는 신경-기호론적(neurosymbolic) 프레임워크를 제시합니다. 우리의 접근법은 LLM 출력을 원자적 주장으로 분해하고, 이를 1차 술어 논리로 자동 형식화하며, 자동 정리 증명을 사용하여 논리적 일관성을 검증합니다. 본 연구는 세 가지 핵심 혁신을 도입합니다: (1) 후보 답변 간 논리 수준 정렬을 보장하기 위한 형식적 의미 동등성 검증을 통한 다중 모델 합의로, 표층 형태 지표의 구문적 편향을 제거합니다. (2) 논리적 주장에는 기호론적 Solver를, 상식 추론에는 LLM 앙상블을 활용하는 적절한 검증 전략으로 주장 유형을 안내하는 의미 기반 라우팅입니다. (3) 최소 수정 부분집합(MCS)을 통한 정밀한 논리 오류 지역화로, 수정이 필요한 정확한 주장 하위 집합을 특정하여 이분법적 실패 신호를 실행 가능한 피드백으로 전환합니다. 우리의 프레임워크는 주장을 논리적 상태에 따라 분류하고 여러 검증 신호를 분산 기반 패널티와 함께 통합 점수로 집계합니다. 이 시스템은 구조화된 피드백을 사용하여 수용 기준이 충족되거나 수렴에 도달할 때까지 답변을 반복적으로 정제합니다. 이러한 하이브리드 접근법은 가능한 경우 형식적 보장을 제공하고 그 외에는 합의 검증을 수행하여 신뢰할 수 있는 AI를 발전시킵니다. GPT-OSS-120B 모델을 사용한 VERGE는 단일 패스 접근법 대비 일련의 추론 벤치마크에서 수렴 시 평균 18.7%의 성능 향상을 보여줍니다.

English

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.

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

VERGE: Formal Refinement and Guidance Engine for Verifiable LLM Reasoning

초록

Support