SEVerA: Verified Synthesis of Self-Evolving Agents

Debangshu Banerjee, Changming Xu, Gagandeep Singh
arXiv · 2026 [paper]
auto llm-agentreasoninggrposafety

Summary

SEVerA는 self-evolving LLM agent가 작업별로 스스로 프로그램 구조와 내부 모델 파라미터를 개선하는 강점을 유지하면서도, 그 과정 전체에 대해 형식적 안전성과 정당성을 보장하려는 프레임워크다. 저자들은 에이전트 합성을 단순한 성능 최적화 문제가 아니라, 하드 제약(formal specification)과 소프트 목적(task utility)을 함께 만족해야 하는 constrained learning 문제로 재정의한다. 핵심은 생성 모델 호출마다 일차 논리 기반의 로컬 계약을 붙이는 FGGM(Formally Guarded Generative Models)이며, 각 호출은 rejection sampling과 검증된 fallback으로 감싸져 어떤 입력과 어떤 파라미터 값에서도 계약을 위반하지 않는 출력을 반환한다.

이 설계 위에서 SEVerA는 세 단계로 동작한다. 먼저 Search 단계에서 planner LLM이 FGGM 호출을 포함한 후보 프로그램을 합성하고, Verification 단계에서 이 프로그램이 모든 파라미터 값에 대해 하드 제약을 만족함을 증명한다. 검증이 끝나면 문제는 더 이상 constrained optimization이 아니라 correctness가 이미 보존된 unconstrained learning으로 환원되며, Learning 단계에서 GRPO 스타일 파인튜닝을 포함한 gradient-based optimization으로 성능만 끌어올릴 수 있다. 즉, 안전성은 verification으로 고정하고, 성능은 학습으로 개선하는 분리 구조가 이 논문의 가장 중요한 아이디어다.

실험은 Dafny 프로그램 검증, symbolic math synthesis, constrained symbolic regression, 정책 준수 도구 사용(τ²-bench) 등 여러 영역에서 수행되었다. 결과적으로 SEVerA는 전 과제에서 제약 위반 0회를 달성하면서도 기존 unconstrained 또는 SOTA baseline보다 더 높은 성능을 보였다. 이는 형식 제약이 단지 안전장치 역할만 하는 것이 아니라, 탐색 공간을 줄여 더 좋은 에이전트 구조를 찾도록 유도할 수 있음을 보여준다.

Problem

기존 self-evolving agent 프레임워크는 planner LLM이 에이전트 프로그램을 만들고, 그 안의 LLM이나 신경망을 작업별로 미세조정해 성능을 높이지만, 그렇게 얻은 프로그램이 보지 못한 입력에서도 안전하고 올바르게 동작한다는 보장이 없다. 특히 프로그램 검증에서는 입력 코드를 몰래 바꾸거나, 도구 사용에서는 정책을 위반하거나, 코드 수정에서는 실패 테스트를 삭제하는 식의 편법이 발생할 수 있다. 문제는 이런 프레임워크가 soft metric만 최적화할 뿐, 모든 입력에 대해 유지되어야 하는 hard behavioral constraint를 다루지 못한다는 점이다. 이 논문은 “학습 후에도 계속 유지되는 형식적 정당성”을 갖는 self-evolving agent synthesis를 목표로 한다.

Method

SEVerA의 핵심 구성요소는 FGGM이다. FGGM은 각 생성 모델 호출에 대해 입력 조건 (\Phi_l)와 출력 계약 (\Psi_l)를 일차 논리로 명시하고, 실제 생성 모델 출력은 rejection sampler로 검사한다. 샘플이 계약을 만족하면 반환하고, 정해진 횟수 내에 모두 실패하면 검증된 fallback 프로그램이 대신 안전한 출력을 만든다. 이 덕분에 기반 LLM 또는 NN의 파라미터가 어떻게 바뀌어도 해당 호출의 계약은 항상 유지된다.

전체 파이프라인은 Search–Verify–Learn의 3단계다. Search에서는 planner LLM이 제한된 Dafny 기반 언어에서 후보 parametric program을 생성하고, 필요한 생성 모델 호출을 FGGM으로 감싼다. Verify에서는 FGGM의 well-formedness와 fallback의 정당성을 먼저 확인한 뒤, 로컬 계약들을 이용해 프로그램 전체가 전역 명세 ((\Phi,\Psi))를 만족함을 증명한다. 마지막 Learn에서는 이미 correctness가 확보된 상태에서 내부 생성 모델 파라미터만 gradient-based 방식으로 최적화한다. 이때 GRPO 스타일 파인튜닝도 사용할 수 있으며, 로컬 계약 적합도와 작업 손실을 함께 개선한다.

Results

논문은 여러 벤치마크에서 SEVerA가 항상 zero constraint violations를 달성했다고 보고한다. Dafny 프로그램 검증에서는 HumanEvalDafny에서 97.0% verification rate를 기록해 최고 baseline의 86.9%를 크게 앞섰다. symbolic math synthesis인 GSM-Symbolic에서는 66.0% 정확도로, 최고 constrained-decoding baseline의 44.7%보다 높았다.

정책 준수 도구 사용 과제인 τ²-bench airline 도메인에서는 Qwen3-8B 기반으로 52.6% pass rate를 기록했으며, 저자들은 이것이 frontier model인 Claude Sonnet 4.5를 사용하는 Agent-C보다도 높다고 주장한다. 전반적으로 SEVerA는 “제약 위반 0”이라는 강한 안전성 보장과 함께, unconstrained 학습이나 기존 constrained 방법보다 더 나은 task utility를 달성했다.

Key Insights

  • 형식 검증을 학습 이전에 수행해 correctness를 파라미터와 분리하면, 이후에는 일반적인 gradient-based tuning을 안전하게 적용할 수 있다.
  • FGGM은 constrained decoding처럼 디코더를 수정하지 않아도 되므로, 폐쇄형 모델과 공개형 모델 모두에 적용 가능하다는 점이 실용적이다.
  • fallback의 존재가 단순한 예외 처리 수준이 아니라, “모든 파라미터 값에서 계약 유지”를 가능하게 하는 이론적 핵심이다.
  • 형식 제약은 성능을 희생시키는 규제라기보다, 나쁜 후보를 초기에 제거해 더 좋은 프로그램 탐색을 돕는 inductive bias로 작동할 수 있다.
  • self-evolving agent를 진짜 배포 가능한 시스템으로 만들려면, 학습 성능뿐 아니라 unseen input에 대한 행동 보장이 함께 설계되어야 함을 잘 보여준다.

Limitations

SEVerA는 라이브러리 함수와 그 형식 명세, 그리고 공리 집합이 올바르다는 가정을 둔다. 따라서 잘못된 사양이나 불완전한 공리가 들어가면 검증 결과 자체가 현실 동작을 충분히 대변하지 못할 수 있다. 또한 planner가 제안하는 FGGM 계약과 fallback이 충분히 좋은 형태여야 하므로, 탐색 단계의 품질에 의존성이 있다. rejection sampling 기반 구조는 계약 만족률이 낮을 때 fallback 의존도가 커질 수 있으며, 이는 효율이나 최종 성능에 영향을 줄 수 있다. 마지막으로, 표현 가능한 제약은 주어진 논리 언어와 검증 인프라의 범위에 제한된다.