SEVerA: Verified Synthesis of Self-Evolving Agents

Motivation

• Known: LLM 에이전트 합성의 핵심 도전은 자율적으로 실행되는 프로그램의 안전성 보장이다. 기존 제약 유도 프로그램 합성(deductive program synthesis)은 형식적 보장을 제공하지만 작업 성능 최적화가 약하고, 자가 진화 프레임워크는 성능은 우수하지만 형식적 보장이 부족하다는 상충관계가 알려져 있다.
• Gap: 기존 작업은 제약 감소(constrained decoding) 기법으로 구문 제약만 강제할 수 있으며, 의미론적 제약의 지원이 제한적이고 모델의 복호화 절차 수정을 요구하여 개방형 모델 적용성이 낮으며, 제약 만족도 출력 분포를 왜곡하여 성능을 저하시킨다는 근본적인 한계가 있다.
• Why: LLM 에이전트의 프로그램 수정, 정책 위반, 보안 우회 등의 실패 사례가 보고되고 있으며, 자율 실행 환경에서 형식적 안전 보장과 동시에 작업 성능을 개선하는 방법론이 실무적으로 필수적이기 때문이다.
• Approach: • FGGM: first-order logic으로 표현된 형식 계약(formal contract)을 통해 각 생성 모델 호출에 지역적 제약을 정의하고, rejection sampler와 검증된 폴백(verified fallback)으로 자동 포장하여 모든 입력과 파라미터 설정에서 계약 만족을 보장\n• SEVerA: (a) Search—Dafny 같은 검증 가능 언어로 프로그램 샘플링, (b) Verify—내장 검증기로 모든 파라미터에 대한 정확성 증명, (c) Learn—검증된 프로그램을 제약 없는 최적화로 환원하여 GRPO 스타일 미세조정 적용

Achievement

Fig. 2. Auto-synthesized guarded GM with

0 제약 위반 달성\n- HumanEvalDafny: 97.0% 검증 성공률 (최고 기준 86.9% 대비)\n- GSM-Symbolic: 66.0% 정확도 (최고 constrained-decoding 44.7% 대비)\n- τ2-bench 항공사 도메인: 52.6% 통과율 (Qwen3-8B 기준, Claude Sonnet 4.5 기반 Agent-C도 초과)\n형식 정확성 증명: Theorem 5.4—반환 에이전트는 모든 입력과 파라미터에서 행동 명세 만족\n성능 개선: Theorem 5.5—제약 없는 모델 대비 작업 손실 없음 보장, 미준수 시 엄격한 개선 증명

How

Fig. 1. Overview of SEVerA, which operates in three key steps. (1) Search: Given the task information, library

• first-order logic 계약을 LLM 출력 문자열에만 적용하여 개방형/폐쇄형 모델 모두 지원\n• 검증기(verifier)의 형식 증명과 그래디언트 기반 최적화의 분리로 기존 GRPO, 미세조정 도구 재사용 가능\n• 형식적 제약이 프로그램 탐색 공간을 정제(prune)하여 더 높은 품질 에이전트로 안내하는 긍정적 부작용 활용

Originality

• FGGM의 novel 개념: 생성 모델 호출 수준에서 first-order logic 기반 형식 계약 도입으로 기존 constrained decoding의 구문-중심 제약을 의미론적 수준으로 확장\n• 형식 검증과 미분 가능 학습의 명시적 분리 설계: Verify 단계가 모든 파라미터에 대한 정확성을 보장하므로 Learn에서 제약 없는 최적화로 환원 가능\n• 자가 진화 에이전트에 형식 보장을 처음으로 부여한 종합 프레임워크

Limitation & Further Study

이론적 한계: Theorem 5.5의 "충분 조건"이 실제 적용 가능성이 제한적일 수 있으며, 어떤 상황에서 이 조건이 만족되는지에 대한 실증적 분석이 부족\n실험 범위: 기존 program repair, code generation 같은 광범위한 LLM 에이전트 작업에 대한 평가 부재, 계산 비용(형식 검증 오버헤드) 분석 미흡\n생성 모델 제약: FGGM의 rejection sampler는 계약 만족 샘플이 매우 희귀한 경우 샘플링 비효율 가능성\n후속 연구: (1) 더 광범위한 agent 도메인 평가, (2) 복합 형식 명세에 대한 검증 확장성 분석, (3) 제약-성능 트레이드오프 메커니즘의 이론적 심화

Evaluation

총평: 본 논문은 자가 진화 LLM 에이전트의 형식적 안전성이라는 긴급한 문제를 처음으로 체계적으로 다루며, FGGM과 SEVerA는 기술적으로 건전하고 실제 성능에서도 우수한 결과를 보인다. 다만 이론적 충분 조건의 실용성 명확화와 평가 도메인 확대가 필요하다.