SEVerA: Верифицированный синтез саморазвивающихся агентов

SEVerA: Verified Synthesis of Self-Evolving Agents

March 26, 2026

Авторы: Debangshu Banerjee, Changming Xu, Gagandeep Singh

cs.AI

Аннотация

Последние достижения продемонстрировали эффективность саморазвивающихся агентов на основе больших языковых моделей (LLM) для таких задач, как исправление программ и научные открытия. В этой парадигме LLM-планировщик синтезирует программу агента, которая вызывает параметрические модели, включая LLM, которые затем настраиваются для каждой задачи для повышения производительности. Однако существующие фреймворки саморазвивающихся агентов не предоставляют формальных гарантий безопасности или корректности. Поскольку такие программы часто выполняются автономно на непредвиденных входных данных, это отсутствие гарантий вызывает обеспокоенность в отношении надежности и безопасности. Мы формулируем задачу генерации агентского кода как проблему обучения с ограничениями, сочетая жесткие формальные спецификации с мягкими целевыми функциями, отражающими полезность задачи. Мы представляем Формально Защищенные Генеративные Модели (FGGM), которые позволяют LLM-планировщику задавать формальный контракт на выходные данные для каждого вызова генеративной модели с использованием логики первого порядка. Каждый вызов FGGM оборачивает базовую модель в rejection sampler с верифицированным резервным вариантом, гарантируя, что каждое возвращаемое выходное значение удовлетворяет контракту для любого входного данных и настройки параметров. На основе FGGM мы представляем SEVerA (Self-Evolving Verified Agents) — трехэтапный фреймворк: Поиск синтезирует кандидатные параметрические программы, содержащие вызовы FGGM; Верификация доказывает корректность относительно жестких ограничений для всех значений параметров, сводя задачу к обучению без ограничений; и Обучение применяет масштабируемую градиентную оптимизацию, включая тонкую настройку в стиле GRPO, для улучшения мягкой целевой функции при сохранении корректности. Мы оцениваем SEVerA на задачах верификации программ на Dafny, синтеза символьных математических выражений и использования агентских инструментов с соблюдением политик (τ²-bench). Во всех задачах SEVerA демонстрирует нулевое количество нарушений ограничений при одновременном улучшении производительности по сравнению с незащищенными и современными базовыми методами, показывая, что формальные ограничения на поведение не только гарантируют корректность, но и направляют синтез в сторону агентов более высокого качества.

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.