SEVerA: 검증된 자체 진화 에이전트 합성

초록

최근 연구에서는 프로그램 수리 및 과학적 발견과 같은 작업에서 자기 진화 LLM 에이전트의 효과성이 입증되었습니다. 이러한 패러다임에서는 플래너 LLM이 LLM을 포함한 파라메트릭 모델을 호출하는 에이전트 프로그램을 합성하며, 이 모델들은 이후 성능 향상을 위해 작업별로 조정됩니다. 그러나 기존 자기 진화 에이전트 프레임워크는 안전성이나 정확성에 대한 형식적 보장을 제공하지 않습니다. 이러한 프로그램들은 종종 보이지 않는 입력에 대해 자율적으로 실행되기 때문에, 이러한 보장의 부재는 신뢰성과 보안 문제를 제기합니다. 우리는 에이전트 코드 생성을 작업 효용성을 포착하는 소프트 목표와 형식적 명세를 결합한 제약 학습 문제로 공식화합니다. 우리는 플래너 LLM이 1차 논리학을 사용하여 각 생성 모델 호출에 대한 형식적 출력 계약을 명시할 수 있게 하는 FGGM(형식적으로 보호되는 생성 모델)을 소개합니다. 각 FGGM 호출은 검증된 폴백 기능을 갖춘 거부 샘플러로 기본 모델을 감싸, 모든 입력 및 매개변수 설정에 대해 반환된 모든 출력이 계약을 만족하도록 보장합니다. FGGM을 기반으로 우리는 세 단계의 프레임워크인 SEVerA(자기 진화 검증 에이전트)를 제시합니다: 탐색 단계는 FGGM 호출을 포함하는 후보 파라메트릭 프로그램을 합성합니다; 검증 단계는 모든 매개변수 값에 대한 하드 제약 조건에 대한 정확성을 증명하여 문제를 비제약 학습 문제로 축소합니다; 학습 단계는 정확성을 보존하면서 소프트 목표를 개선하기 위해 GRPO 방식의 미세 조정을 포함한 확장 가능한 경사 기반 최적화를 적용합니다. 우리는 SEVerA를 Dafny 프로그램 검증, 기호 수학 합성, 그리고 정책 준수 에이전트 도구 사용(τ^2-bench) 작업에서 평가합니다. 다양한 작업에서 SEVerA는 제약 조건 위반을 전혀 발생시키지 않으면서 비제약 및 SOTA 기준선 대비 성능을 향상시켜, 형식적 행동 제약이 정확성만을 보장하는 것이 아니라 더 높은 품질의 에이전트를 향한 합성을 유도함을 보여줍니다.

English

Recent advances have shown the effectiveness of self-evolving LLM agents on tasks such as program repair and scientific discovery. In this paradigm, a planner LLM synthesizes an agent program that invokes parametric models, including LLMs, which are then tuned per task to improve performance. However, existing self-evolving agent frameworks provide no formal guarantees of safety or correctness. Because such programs are often executed autonomously on unseen inputs, this lack of guarantees raises reliability and security concerns. We formulate agentic code generation as a constrained learning problem, combining hard formal specifications with soft objectives capturing task utility. We introduce Formally Guarded Generative Models (FGGM), which allow the planner LLM to specify a formal output contract for each generative model call using first-order logic. Each FGGM call wraps the underlying model in a rejection sampler with a verified fallback, ensuring every returned output satisfies the contract for any input and parameter setting. Building on FGGM, we present SEVerA (Self-Evolving Verified Agents), a three-stage framework: Search synthesizes candidate parametric programs containing FGGM calls; Verification proves correctness with respect to hard constraints for all parameter values, reducing the problem to unconstrained learning; and Learning applies scalable gradient-based optimization, including GRPO-style fine-tuning, to improve the soft objective while preserving correctness. We evaluate SEVerA on Dafny program verification, symbolic math synthesis, and policy-compliant agentic tool use (τ^2-bench). Across tasks, SEVerA achieves zero constraint violations while improving performance over unconstrained and SOTA baselines, showing that formal behavioral constraints not only guarantee correctness but also steer synthesis toward higher-quality agents.

SEVerA: 검증된 자체 진화 에이전트 합성

SEVerA: Verified Synthesis of Self-Evolving Agents

초록

Support