Lean4Agent: Modelagem Formal e Verificação de Fluxo de Trabalho e Trajetória de Agente

Resumo

Equipar Modelos de Linguagem de Grande Porte (LLMs) para executar fluxos de trabalho confiáveis de múltiplas etapas tornou-se um desafio central em inteligência artificial. Apesar dos avanços recentes nas capacidades agentivas dos LLMs, a maioria dos sistemas agentes ainda carece de métodos formais para especificar, verificar e depurar seus fluxos de trabalho e trajetórias de execução. Esse desafio ecoa um problema de longa data na matemática, onde a ambiguidade das línguas naturais (LNs) motiva o desenvolvimento de linguagens formais (LFs). Inspirados por esse paradigma, propomos o **Lean4Agent**, até onde sabemos, o primeiro framework que utiliza o Lean4, uma LF de tipo dependente, para modelar e verificar o comportamento de agentes. O **Lean4Agent** lança o **FormalAgentLib**, uma biblioteca extensível em Lean4 para modelar e verificar formalmente a consistência semântica dos fluxos de trabalho de agentes sob suposições explícitas, permitindo a localização de falhas em tempo de execução reveladas por trajetórias. Com base no **FormalAgentLib**, desenvolvemos ainda o **LeanEvolve**, que aplica os resultados do **FormalAgentLib** para revisar fluxos de trabalho, aprimorando sua capacidade. Experimentos extensivos em um subconjunto de problemas difíceis do SWE-Bench-Verified e em um subconjunto do ELAIP-Bench com 5 LLMs líderes indicam que os fluxos de trabalho que passam na verificação superam os que falham em uma média de **11,94%**, e o **LeanEvolve** melhora ainda mais o desempenho no SWE em **7,47%** em média. Além disso, o **Lean4Agent** estabelece uma base para um novo campo de uso de LFs de tipo dependente expressivas para modelar e verificar formalmente o comportamento de agentes.

English

Equipping Large Language Models (LLMs) to execute reliable multi-step workflows has become a central challenge in artificial intelligence. Despite recent advances in LLMs' agentic capabilities, most agent systems still lack formal methods for specifying, verifying, and debugging their workflow and execution trajectories. This challenge mirrors a long-standing problem in mathematics, where the ambiguity of natural languages (NLs) motivates the development of formal languages (FLs). Inspired by this paradigm, we propose **Lean4Agent**, to the best of our knowledge, the first framework that uses Lean4, a dependent-type FL to model and verify agent behavior. **Lean4Agent** launches **FormalAgentLib**, an extensible Lean4 library for formally modeling and verifying agent workflows' semantic consistency under explicit assumptions, and enabling localization of execution-time failures revealed by trajectories. Building on **FormalAgentLib**, we further develop **LeanEvolve**, which applies results in **FormalAgentLib** to revise workflows to enhance its capability. Extensive experiments on a hard problem subset of SWE-Bench-Verified and a subset of ELAIP-Bench across 5 leading LLMs indicate that the verification-passing workflows outperform the failing ones by an average of **11.94%**, and **LeanEvolve** further improves SWE performance by **7.47%** on average. Furthermore, **Lean4Agent** establishes a foundation for a new field of using expressive dependent-type FL to formally model and verify agent behavior.