SEVerA: 자기 진화형 에이전트의 검증된 합성

자기 진화형 LLM 에이전트가 생성한 코드가 안전한지 수학적으로 증명할 수 없었던 기존 한계를 극복했습니다. SEVerA는 정형 검증 기법을 도입하여 에이전트가 생성한 프로그램이 사전에 정의된 안전 및 정확성 규칙을 절대로 위반하지 않음을 보장하며, 동시에 성능 최적화까지 가능하게 합니다.

기존의 LLM 에이전트는 스스로 코드를 수정하고 발전시키는 과정에서 의도치 않게 보안 취약점을 만들거나 논리적 오류를 범할 위험이 크다. 이는 신경망 기반의 생성 모델이 확률적으로 동작하기 때문에 특정 규칙을 반드시 지키도록 강제할 수 없다는 근본적인 한계에서 기인한다. SEVerA는 이 문제를 해결하기 위해 딥러닝의 유연성과 전통적인 정형 검증(Formal Verification)의 엄격함을 결합한다.

핵심 아이디어는 LLM이 생성한 결과물을 그대로 실행하는 대신, '계약(Contract)'이라는 필터를 통과시키는 것이다. 마치 함수가 입력과 출력의 타입을 지켜야 하듯, LLM의 출력이 논리적으로 타당한지 수학적으로 검사한다. 만약 LLM이 생성한 코드가 규칙을 어기면 다시 생성하도록 시도(Rejection Sampling)하고, 끝내 실패하면 미리 준비된 안전한 기본 코드(Fallback)를 실행하여 시스템의 안정성을 100% 보장한다.

이 과정에서 흥미로운 점은 이러한 '제약 조건'이 단순히 안전장치 역할만 하는 것이 아니라, LLM이 탐색해야 할 정답의 범위를 좁혀주는 가이드 역할을 한다는 것이다. 결과적으로 에이전트는 엉뚱한 방향으로 학습되지 않고, 검증된 범위 내에서만 성능을 최적화하게 되어 더 빠르고 정확한 자기 진화가 가능해진다.

SEVerA는 Search, Verification, Learning의 세 단계로 구성된 순환 구조를 가진다. Search 단계에서는 Planner LLM이 FGGM 호출을 포함하는 후보 프로그램을 생성한다. 이때 각 FGGM은 입력 조건(Requires)과 출력 조건(Ensures)이 명시된 논리적 계약을 포함한다.

Verification 단계에서는 Dafny 검증기를 사용하여 생성된 프로그램이 모든 입력값과 모델 파라미터 설정에 대해 정형 사양을 만족하는지 수학적으로 증명한다. 이 과정은 [프로그램 코드와 논리 사양 입력 → SMT Solver를 통한 논리적 모순 여부 판별 → 증명 성공 시 통과] 순으로 진행되어, 파라미터가 어떻게 변하더라도 안전성이 유지됨을 보장한다.

Learning 단계에서는 검증된 프로그램의 성능을 높이기 위해 경량화된 최적화 기법을 적용한다. 특히 LLM의 경우 GRPO(Group Relative Policy Optimization) 스타일의 파인튜닝을 사용하여, [입력 프롬프트에 대해 여러 샘플 생성 → 각 샘플의 작업 손실(Loss)과 계약 준수 여부 계산 → 보상 함수(Reward) 산출 → 가중치 업데이트] 과정을 거쳐 모델이 계약을 더 잘 준수하면서도 정답에 가까운 결과를 내도록 학습시킨다.

HumanEvalDafny 벤치마크에서 SEVerA는 97.0%의 검증 성공률을 기록하여 기존 최고 수치인 86.9%를 크게 상회했다. 특히 기존 모델들이 검증 통과를 위해 원본 코드를 임의로 수정하는 '치팅'을 범하는 것과 달리, SEVerA는 AST 기반의 차분 검사(Diff check)를 제약 조건으로 걸어 이러한 위반을 0%로 차단했다.

기호 수학 합성(GSM-Symbolic) 과제에서는 Qwen3-8B 모델을 사용하여 66.0%의 정확도를 달성했다. 이는 제약 조건 없이 학습된 기본 모델(38.3%)이나 기존의 제약 조건 디코딩 기법인 CRANE(44.7%)보다 월등히 높은 수치이다. 또한 에이전트 도구 사용(tau-bench) 테스트에서도 Claude 4.5와 같은 거대 모델을 사용한 기존 에이전트보다 더 높은 성공률을 보이며 소형 모델로도 안전하고 효율적인 에이전트 구축이 가능함을 입증했다.

SEVerA의 핵심은 FGGM(Formally Guarded Generative Models) 아키텍처이다. FGGM은 확률적 생성 모델을 결정론적인 정형 계약으로 감싸는 래퍼(Wrapper) 역할을 한다. 이는 모델의 내부 가중치에 접근할 수 없는 폐쇄형 모델(Closed-source)에도 적용 가능한 모델-애그노스틱(Model-agnostic)한 방식이다.

수학적으로 SEVerA는 제약 조건이 있는 학습 문제(Constrained Learning Problem)를 해결한다. 목적 함수는 작업 손실(Task Loss)과 계약 위반 손실(Conformance Loss)의 합으로 정의된다. [샘플링된 출력 y가 계약을 위반할 확률 계산 → 위반 시 높은 페널티 부여 → Sigmoid 변환을 통한 부드러운 보상 지형 형성] 과정을 통해 경사 하강법(Gradient Descent)이 모델을 안전한 영역으로 유도하도록 설계되었다.

구현 측면에서 SEVerA는 Dafny 언어를 호스트 언어로 채택하여 강력한 타입 시스템과 내장 검증기를 활용한다. 합성된 프로그램은 Python으로 트랜스파일되어 실제 실행 및 학습에 사용된다. 이러한 구조는 추론 시점에만 제약을 거는 기존의 Constrained Decoding과 달리, 학습 시점부터 제약 조건을 내재화하여 추론 속도 저하 없이 높은 성능을 유지하게 한다.

현재 SEVerA는 기능적 정확성에 초점을 맞추고 있어, LLM 호출 횟수나 토큰 사용량, 실행 시간과 같은 자원 제약(Resource-aware constraints)은 고려하지 않는다. 또한 Planner LLM이 초기 탐색 단계에서 적절한 후보 프로그램을 제안하지 못할 경우 최적의 솔루션을 찾지 못할 가능성이 있다.