SEVerA: Verified Self-Evolving Agents with Specification Guidance

Motivation

• Known: 기존 self-evolving LLM agent 프레임워크(예: program repair, scientific discovery용)는 planner LLM이 model harness를 합성하고 이를 태스크별로 파라미터 튜닝하여 성능을 개선하는 방식이며, deductive program synthesis는 formal correctness를 보장하지만 성능 최적화 목표가 없고, GRPO 같은 gradient 기반 방법은 성능은 개선하지만 제약 만족을 보장하지 않는다.
• Gap: 기존 self-evolving 프레임워크는 합성된 프로그램이 unseen input에 대해 자율 실행됨에도 안전성이나 정확성에 대한 formal guarantee가 전혀 없어, 프로그램 검증에서의 치팅, 코드 리페어에서의 테스트 삭제, agentic tool use에서의 정책 위반(65-76%) 등 다양한 실패가 실증적으로 보고되고 있다.
• Why: 안전 필수 도메인에서 자율 실행되는 LLM 에이전트가 formal behavioral constraint를 항상 만족하도록 보장하면서도 gradient 기반 최적화의 성능 이득을 유지할 수 있다면, 신뢰할 수 있는 agentic AI 배포의 핵심 장벽을 해소할 수 있다.
• Approach: 모델 호출마다 verified fallback을 갖는 rejection sampler로 감싸는 FGGM을 도입하고, 이를 기반으로 Dafny 같은 verifier-aware language에서 프로그램을 샘플링(Search)하고 built-in verifier로 contract 만족을 증명(Verify)한 뒤, 검증된 프로그램에 대해 unconstrained gradient 기반 학습(Learn)을 수행하는 3단계 SEVerA 프레임워크를 제시한다.

Achievement

1. FGGM 도입: 각 모델 호출을 first-order logic으로 표현된 input-output contract로 감싸는 Formally Guarded Generative Models을 제안하여, open/closed-source 모델 모두에 적용 가능하고 출력 문자열만으로 동작하는 local contract enforcement 메커니즘을 구현했다.
2. SEVerA 알고리즘: Search→Verify→Learn 3단계로 구성된 최초의 검증 가능한 self-evolving agent synthesis 알고리즘을 제시하고, 검증된 파라메트릭 프로그램에 대해 constrained learning을 unconstrained optimization으로 환원하여 scalable gradient 기반 학습을 가능케 했다.
3. 이론적 보증: 반환된 에이전트가 모든 입력과 모든 파라미터 값에 대해 behavioral specification을 만족함을 증명하는 soundness 정리(Theorem 3.2)와, unconstrained 모델보다 task loss가 나빠지지 않는(오히려 위반 시 strict 개선되는) 검증된 에이전트 존재의 충분조건(Theorem 3.3)을 확립했다.
4. 실증적 성능: τ2-bench airline domain에서 Qwen3-8B 기반 SEVerA가 52.6% pass rate로 Claude Sonnet 4.5 기반 Agent-C(47.3%)를 능가했고, HumanEvalDafny에서 97.0%(vs 86.9%), GSM-Symbolic에서 66.0%(vs 44.7%) 성능을 달성하며 zero constraint violation을 유지했다.

How

• 각 GM 호출을 rejection sampler로 감싸 sampled output이 specification을 만족하지 않으면 verified fallback으로 대체하는 FGGM 정의 (Fig 3, 4, 5의 initialFGGM, diffErrorFGGM, verifierErrorFGGM 등 구체적 인스턴스 제시)
• Search 단계: planner LLM이 Dafny 등 verifier-aware language로 프로그램 문자열을 샘플링, 임베디드 모델 호출에 FGGM으로 local contract 부여
• Verify 단계: 언어 내장 verifier가 샘플링된 프로그램이 임베디드 파라메트릭 모델의 모든 파라미터에 대해 지정된 contract를 만족함을 증명
• Learn 단계: 검증된 프로그램에 대해 제약이 이미 형식적으로 보장되므로 constrained learning problem(Eq. 2)을 unconstrained optimization(Eq. 1과 유사)으로 환원하여 gradient 기반 파라미터 튜닝 수행
• τ2-bench(agentic tool use), HumanEvalDafny(program verification), GSM-Symbolic(symbolic math), constrained symbolic regression(scientific discovery) 등 4개 도메인에서 평가

Originality

• soft objective(task utility)와 hard formal specification을 결합한 constrained learning 문제로 self-evolving agent synthesis를 재정식화한 최초의 시도
• 모델 호출 단위로 rejection sampling과 verified fallback을 결합해 first-order output contract를 강제하는 FGGM이라는 새로운 추상화 도입, 이는 decoding 내부를 수정하지 않고 출력 문자열 수준에서만 동작하여 closed-source 모델에도 적용 가능
• Dafny와 같은 verifier-aware language의 built-in verifier를 self-evolving agent synthesis 파이프라인에 통합하여 Search-Verify-Learn이라는 새로운 3단계 구조를 제안
• soundness와 성능 하한을 모두 증명하는 이론적 프레임워크 제공 (기존 deductive synthesis는 성능 미보장, gradient 방법은 correctness 미보장이라는 이분법 해소)

Limitation & Further Study

• FGGM의 rejection sampling 방식은 첫 스테이지(Search)에서 verifier-aware language(Dafny 등)에 프로그램을 국한하므로, verifier가 부재하거나 표현력이 부족한 도메인으로의 일반화 가능성이 제한적일 수 있음
• rejection sampling 기반 fallback이 잦을 경우 계산 비용이나 실제 성능(품질) 저하로 이어질 수 있는데, 이에 대한 정량적 비용-이득 분석이 본문 발췌에서는 충분히 드러나지 않음
• 이론적 보증(Theorem 3.2, 3.3)의 충분조건이 실제로 어떤 태스크·모델 조합에서 성립하는지에 대한 폭넓은 실증적 검증이 4개 벤치마크에 국한되어 있어 추가적 확장 연구가 필요
• first-order logic으로 표현 가능한 specification에 국한되므로, 더 복잡한 higher-order 혹은 확률적 안전 속성에 대한 확장 연구가 필요함

Evaluation

총평: self-evolving LLM agent 합성에 formal verification을 통합해 안전성과 성능을 동시에 보장하는 새로운 접근으로, 이론적 보증과 실증적 성능 향상을 함께 제시한 의미 있는 연구이나 verifier-aware language에 대한 의존성과 확장성 검증이 추가로 필요하다.