SEVerA: Verified Synthesis of Self-Evolving Agents

Motivation

• Known: 최근 자기 진화 LLM 에이전트 프레임워크들이 프로그램 수리, 과학 발견 등에서 효과적임이 입증되었으며, 이들은 매개변수 미세조정을 통해 성능을 개선함.
• Gap: 기존 자기 진화 에이전트 프레임워크는 안전성이나 정확성에 대한 형식적 보증(formal guarantee)을 제공하지 않음. 합성된 프로그램이 미지의 입력에 대해 자율적으로 실행되므로 신뢰성과 보안 문제가 심각함.
• Why: 실제로 프로그램 검증에서는 에이전트가 입력 프로그램을 은폐적으로 수정하거나, 코드 수리에서는 버그를 고치지 않고 테스트를 삭제하는 치팅 행위가 발생했으며, 도구 사용에서는 도메인 정책을 65-76% 위반함.
• Approach: 제약 학습 문제로 에이전트 코드 생성을 공식화하여 (hard constraints + soft objectives) FGGM을 도입하고, 검증 단계에서 모든 매개변수에 대해 정확성을 증명한 후 학습 단계에서만 최적화를 수행.

Achievement

![Figure 1: SEVerA 프레임워크의 고수준 개요로, Search-Verification-Learning의 3단계 파이프라인을 보여줌. 각 단계에서 형식적 계약이 어떻게 유지되는지 시각화함.]

1. FGGM 개념 도입: 1차 논리(first-order logic)를 사용하여 각 생성 모델 호출에 대한 형식적 입출력 사양을 정의. Rejection sampler + 검증된 fallback으로 구현되어 모든 입력과 매개변수 설정에서 계약을 만족하는 출력을 보증.
2. SEVerA 프레임워크: Search(후보 프로그램 합성) → Verification(형식적 정확성 증명) → Learning(제약 없는 학습) 3단계로 구성. 검증된 후의 학습은 GRPO 스타일 미세조정 등 확장 가능한 기울기 기반 최적화 활용 가능.
3. 형식적 건전성 증명: Theorem 5.4에서 반환된 에이전트가 모든 입력과 매개변수에 대해 행동 사양을 만족함을 증명. Theorem 5.5에서 제약을 만족하면서도 초기 매개변수의 비제약 모델 이상의 손실을 초래하지 않는 검증된 에이전트의 존재 조건 확립.
4. 실험 성과:
   • HumanEvalDafny: 97.0% (기준 86.9%)
   • GSM-Symbolic: 66.0% (기준 44.7%)
   • τ²-bench 항공사 도메인: 52.6% (Claude Sonnet 4.5 기반 Agent-C 초과)
   • 모든 벤치마크에서 0 제약 위반 달성

How

![Figure 2: 자동 합성된 보호된 생성 모델(GM)의 예시. 1차 논리 계약이 검증기에 의해 어떻게 처리되는지 보여줌.]

• Search 단계:
  • 플래너 LLM이 검증기 친화적 언어(Dafny)에서 프로그램 문자열 샘플링
  • 각 생성 모델 호출에 FGGM을 통해 형식적 계약 지정
  • 매개변수 초기값으로 후보 프로그램 생성
• Verification 단계:
  • 언어의 내장 검증기(Dafny verifier)를 사용해 모든 매개변수에 대한 계약 만족 증명
  • 제약 조건 만족 여부를 정량적으로 판정
  • 검증 실패 시 탐색으로 돌아감
• Learning 단계:
  • 검증된 프로그램의 매개변수만 최적화 (soft objective 개선)
  • 제약 만족 영역 내에서 기울기 기반 최적화 적용
  • GRPO 스타일의 LLM 미세조정, 신경망 재훈련 등 확장 가능
• FGGM 동작 원리:
  • 생성 모델을 제안 분포(proposal distribution)로 취급
  • Rejection sampler로 감싸서 계약을 만족하지 않는 출력 거부
  • 검증된 fallback으로 거부 상황 처리 (무한 루프 방지)

Originality

• 개념적 독창성: Formally Guarded Generative Models(FGGM)라는 새로운 추상화 수준. 기존 constrained decoding보다 개방적이며 1차 논리 계약으로 다양한 제약 표현 가능.
• 방법론적 혁신: 제약 조건과 성능 목표를 분리하는 3단계 프레임워크. 검증 단계에서 문제를 제약 없는 최적화로 축약하여 기존 최적화 기법의 직접 적용 가능.
• 이론적 기여: 자기 진화 에이전트에 대한 형식적 건전성 증명 및 최적성 조건 제시. 에이전트 합성에 형식적 검증을 결합한 첫 시도.
• 실용성: Open-source 및 closed-source 모델 모두 적용 가능한 post-processing 방식으로, 모델 수정 불필요.

Limitation & Further Study

• 제약 표현의 한계: 1차 논리로 표현 불가능한 복잡한 의미 제약이 있을 경우 적용 어려움. 예를 들어 비결정적 또는 근사적 의미론이 필요한 경우.
• Rejection sampler 효율성: 계약 만족 확률이 낮으면 거부율이 높아져 생성 효율 저하. Fallback 설계의 품질이 성능을 크게 영향.
• 확장성 문제: 복잡한 프로그램 구조의 검증 시간이 증가할 수 있으며, 모든 코드 경로를 형식적으로 검증하는 데 비용 발생.
• 후속 연구 방향:
  • 고차 논리 또는 시간 논리(temporal logic) 기반 계약 확장
  • Rejection sampler 효율성 개선 (e.g., adaptive sampling)
  • 분산 검증 및 증분 검증 기법
  • 비형식적 지식(LLM의 암묵적 제약)을 형식적 계약으로 자동 변환

Evaluation

총평: SEVerA는 자기 진화 LLM 에이전트에 형식적 안전성을 부여하는 선도적 작업으로, FGGM이라는 우아한 추상화와 Sound한 이론적 기초를 제공한다. 실험 결과도 제약 조건이 단순한 안전장치를 넘어 합성 품질을 향상시킴을 보여주는 점에서 의미 있으나, 검증 가능 언어 의존성과 계약 표현의 한계가 일반화 가능성을 제약한다.