에이전트 기반 모델 검증 (Agentic Model Checking)

LLM(Large Language Model)이 생성한 시스템 코드를 검증하는 것은 어렵습니다. 버그가 만연해 있고, 형식적 명세(Formal Specifications)가 누락되어 있으며, 안전 계약(Safety Contracts)이 함수 경계에서 강제되기보다는 호출 지점(Call Sites)에서 암묵적으로 인코딩되어 있기 때문입니다. 우리는 에이전트가 제안하고 솔버(Solver)가 검증한다는 원칙 아래, LLM 에이전트를 유계 모델 검증(Bounded Model Checking, BMC) 백엔드와 결합하는 패러다임인 에이전트 기반 모델 검증(Agentic Model Checking)을 제안합니다. 에이전트는 의미론적 판단이 필요한 작업(명세 추론, 검증 선택, 반례 분류, 개선 제안)을 처리하고, BMC는 건전성(Soundness)과 관련된 모든 결정을 수행합니다.

이 패러다임은 세 가지 약속에 기반합니다. 첫째, 명세는 호출자 문맥(Caller Context)으로부터 제한된 DSL(Domain-Specific Language)을 통해 하향식으로 추론되며, 이는 백엔드의 assume/assert 프리미티브(Primitives)로 결정론적으로 변환됩니다. 또한 선택적인 기능적 정확성(Functional-correctness) 절을 통해 검증 범위를 패닉 프리(Panic-freeness) 수준에서 동작 충실도(Behavioural Faithfulness) 수준으로 격상시킵니다. 둘째, 검증은 합성적(Compositional)입니다. 각 함수는 호출 대상(Callees)을 사후 조건(Postcondition)이 제약된 스텁(Stub)으로 대체하여 자신의 명세에 따라 격리된 상태로 검증되므로, 쿼리당 비용은 단일 함수의 상태 공간(State Space)에 따라 확장되며 개선 사항은 호출자에게 자동으로 전파됩니다. 셋째, 반례(Counterexamples)는 단순한 버그 보고서가 아닙니다. 반례는 도달 가능성(Reachability), 호출 대상 타당성(Callee Feasibility), 동적 재현(Dynamic Replay), 현실성 감사(Realism Audit)를 포함하는 검증 파이프라인을 통과하여, 실제 트리 내의 충돌(In-tree Crashes)과 잠재적인 퍼블릭 API 실패를 구분하며, 모델링 아티팩트(Modelling Artifacts)는 억제되는 대신 개선 루프를 주도합니다.

우리는 이 접근 방식을 BMC-Agent로 구현하였으며, 이를 C와 Rust로 작성된 LLM 생성 커널 및 컴파일러 코드와 성숙한 OSS-Fuzz 강화 라이브러리들을 대상으로 평가하였습니다. 이를 통해 실제 결함을 확인하고, 강력하게 퍼징(Fuzzing)된 표면에서도 유계된 클린 검증(Bounded Clean Verifications)을 생성하며, 선택된 알고리즘 함수에서 기능적 동등성(Functional Equivalence)을 확립함을 입증하였습니다.