Lean4Agent: формальная верификация рабочих процессов LLM-агентов повысила точность на 11,94%
Надежность многошаговых рабочих процессов, выполняемых агентами на основе больших языковых моделей (LLM), остается одной из ключевых проблем в области искусственного интеллекта. Современные агентные системы, как правило, не имеют формальных методов для спецификации, верификации и отладки своих workflow и траекторий выполнения. Это напоминает давнюю проблему в математике, где неоднозначность естественных языков привела к созданию формальных языков.
Вдохновившись этим подходом, группа исследователей разработала Lean4Agent — первый в своем роде фреймворк, использующий зависимо-типизированный формальный язык Lean4 для моделирования и верификации поведения агентов. Lean4Agent включает библиотеку FormalAgentLib, которая позволяет формально описывать и проверять семантическую согласованность рабочих процессов при явно заданных предположениях, а также локализовать ошибки исполнения, выявленные в траекториях.
На основе FormalAgentLib был создан метод LeanEvolve. Он применяет результаты верификации для автоматического улучшения рабочих процессов, повышая их способность успешно выполнять задачи. Такой подход позволяет не только обнаруживать ошибки, но и исправлять их без ручного вмешательства.
Эффективность Lean4Agent была проверена в экспериментах на сложных наборах задач из SWE-Bench-Verified и ELAIP-Bench с использованием пяти ведущих LLM. Результаты показали, что рабочие процессы, прошедшие верификацию, превосходят те, которые ее не прошли, в среднем на 11,94%. Дополнительное применение LeanEvolve улучшило производительность на задачах по разработке ПО (SWE) еще на 7,47%.
По мнению авторов, Lean4Agent закладывает основу для нового направления — формального моделирования и верификации поведения агентов с помощью выразительных зависимо-типизированных формальных языков. Это может стать важным шагом к созданию более надежных и предсказуемых систем искусственного интеллекта.
