BEAVER: 효율적인 결정론적 LLM 검증기

초록

대규모 언어 모델(LLM)이 연구용 프로토타입에서 실제 운영 시스템으로 전환됨에 따라, 실무자들은 모델 출력이 요구되는 제약 조건을 만족하는지 검증할 신뢰할 수 있는 방법이 필요합니다. 표본 추출 기반 추정치는 모델 동작에 대한 직관을 제공하지만, 엄밀한 보장을 제공하지는 않습니다. 본 논문에서는 LLM의 제약 조건 만족에 대한 결정론적이고 엄밀한 확률적 경계를 계산하는 최초의 실용적 프레임워크인 BEAVER를 제시합니다. 접두사-폐쇄적 의미론적 제약 조건이 주어지면, BEAVER는 새로운 토큰 트라이(trie) 및 프론티어 데이터 구조를 활용하여 생성 공간을 체계적으로 탐색하며 매 반복마다 이론적으로 엄밀하게 보장된 경계를 유지합니다. 우리는 검증 문제를 공식화하고 접근법의 엄밀성을 증명하며, 최신 LLM들을 대상으로 정확성 검증, 개인정보 보호 검증 및 안전한 코드 생성 과제에 대해 BEAVER를 평가합니다. 동일한 계산 예산 하에서 BEAVER는 기준 방법 대비 6~8배 좁은 확률 경계를 달성하고 3~4배 많은 고위험 사례를 식별하여, 느슨한 경계나 경험적 평가로는 제공할 수 없는 정밀한 특성 분석 및 위험 평가를 가능하게 합니다.

English

As large language models (LLMs) transition from research prototypes to production systems, practitioners often need reliable methods to verify that model outputs satisfy required constraints. While sampling-based estimates provide an intuition of model behavior, they offer no sound guarantees. We present BEAVER, the first practical framework for computing deterministic, sound probability bounds on LLM constraint satisfaction. Given any prefix-closed semantic constraint, BEAVER systematically explores the generation space using novel token trie and frontier data structures, maintaining provably sound bounds at every iteration. We formalize the verification problem, prove soundness of our approach, and evaluate BEAVER on correctness verification, privacy verification and secure code generation tasks across multiple state of the art LLMs. BEAVER achieves 6 to 8 times tighter probability bounds and identifies 3 to 4 times more high risk instances compared to baseline methods under identical computational budgets, enabling precise characterization and risk assessment that loose bounds or empirical evaluation cannot provide.

BEAVER: 효율적인 결정론적 LLM 검증기

BEAVER: An Efficient Deterministic LLM Verifier

초록

Support