Lean4Agent: Formal Modeling and Verification for Agent Workflow and Trajectory

Com base no texto fornecido, aqui está um resumo técnico detalhado do artigo "Lean4Agent: Formal Modeling and Verification for Agent Workflow and Trajectory":

Visão Geral

O artigo apresenta o Lean4Agent, o primeiro framework que utiliza o Lean4, uma linguagem formal de tipos dependentes (FL), para modelar, verificar e refinar de forma uniforme fluxos de trabalho (workflows) e trajetórias de execução de agentes de Large Language Models (LLM). Os autores abordam o desafio crítico de garantir a confiabilidade em sistemas de agentes de múltiplas etapas, onde a ambiguidade da linguagem natural frequentemente leva a alucinações, inconsistências lógicas e falhas de execução. Ao emprestar paradigos da prova de teoremas formal, o Lean4Agent fornece garantias matematicamente comprováveis para o comportamento do agente.

Contribuições Principais

O framework consiste em dois componentes primários:

1. FormalAgentLib: Uma biblioteca extensível em Lean4 para modelar e verificar formalmente fluxos de trabalho de agentes.
2. LeanEvolve: Um método de refinamento em tempo de execução que utiliza resultados de verificação para melhorar automaticamente os fluxos de trabalho.

Metodologia: O Sistema de Verificação de Três Camadas

O FormalAgentLib opera em três camadas distintas de correção:

Camada 1: Verificação Estrutural

• Objetivo: Verificar a conformidade sintática e estrutural do fluxo de trabalho, análogo a verificações de compilador.
• Mecanismo: Define um sistema de tipos para variáveis, nós de execução e transições de grafo. Ele verifica:
  • Alcançabilidade de nós.
  • Validade de arestas (sequencial, ramificação, loop).
  • Consistência de Leitura/Escrita: Garante que os nós leiam apenas variáveis que são ou parâmetros iniciais ou produzidos por nós predecessores alcançáveis.
• Resultado: Detecta erros estruturais como "leituras não resolvidas", onde uma etapa tenta acessar dados não gerados em seu escopo.

Camada 2: Verificação Semântica Estática

• Objetivo: Verificar a autossuficiência semântica sob suposições explícitas (especificamente, a suposição LLMExec: se uma etapa de LLM começa em um estado que satisfaz os pré-requisitos, ela produz um estado que satisfaz os pós-requisitos).
• Mecanismo:
  • Sistema de Predicados: Traduz instruções ambíguas de linguagem natural em predicados concretos e decidíveis (ex: isValidJson, matchesJsonSchema, nameExists).
  • Lógica Estilo Hoare: Modela cada etapa do agente como um par de pré-condição/pós-condição.
  • Grafo de Fluxo de Trabalho Semântico: Propaga esses contratos através do grafo do fluxo de trabalho para garantir que a saída de uma etapa satisfaça os requisitos de entrada da próxima.
  • Variáveis Implícitas: Rastreia o fluxo de informações e o gerenciamento de contexto para detectar erros que humanos poderiam perder (ex: isolamento de contexto em ramos paralelos).
• Resultado: Identifica fluxos de trabalho que são semanticamente autossuficientes antes da execução.

Camada 3: Verificação de Trajetória de Execução

• Objetivo: Validar a suposição LLMExec em execuções reais e localizar falhas.
• Mecanismo:
  • Utiliza o Lean para avaliar predicados decidíveis.
  • Utiliza ferramentas externas (ex: validadores Python) para verificações em tempo de execução (ex: conectividade de URL).
  • Utiliza LLM-as-a-Judge para propriedades não decidíveis, aproveitando o feedback do ambiente (ex: erros de casos de teste).
• Resultado: Aponta exatamente a etapa onde uma trajetória desvia dos pós-requisitos esperados, permitindo a depuração direcionada.

LeanEvolve: Refinamento Guiado por Formalismo

Quando um fluxo de trabalho passa na verificação estática, mas falha durante a execução, o LeanEvolve é empregado para refiná-lo:

• Modo Guiado por Formalismo: Utiliza diagnósticos da Camada 3 para identificar o predicado específico violado e a etapa que falhou. Um LLM é então instruído a revisar a especificação do fluxo de trabalho com base nesta localização precisa do erro.
• Modo Pure-LLM: Um fallback/adicional que realiza exploração ampla e revisões de tentativa e erro sem orientação formal, útil para tarefas onde o feedback formal é escasso.
• Resultado: O sistema evolui iterativamente o fluxo de trabalho até que a tarefa seja resolvida.

Resultados Experimentais

Os autores avaliaram o Lean4Agent em dois benchmarks desafiadores através de cinco LLMs líderes (incluindo GPT-5.2, GLM-5, Kimi-K2.5, etc.):

1. SWE-Bench-Verified (Subconjunto Hard): Tarefas reais de engenharia de software envolvendo geração de código e depuração.
2. ELAIP-Bench: Tarefas de compreensão de artigos de IA que exigem raciocínio complexo e recuperação de evidências.

Principais Descobertas:

• Impacto da Verificação: Fluxos de trabalho que passaram na verificação da Camada 2 superaram aqueles que falharam em uma média de 11,94% (14,80% no SWE e 9,07% no ELAIP). Isso demonstra que a verificação formal filtra efetivamente fluxos de trabalho defeituosos.
• Impacto do Refinamento: Usando o LeanEvolve, os fluxos de trabalho verificados alcançaram uma melhoria adicional média de 7,47% na tarefa SWE.
• Formal vs. Pure LLM: A evolução guiada por formalismo superou a evolução de LLM puro em 7,00% em média ao corrigir casos inicialmente falhos, provando que a localização precisa de erros é superior à tentativa e erro cega.
• Sensibilidade do Modelo: Modelos menores mostraram maior sensibilidade à qualidade do fluxo de trabalho, ganhando mais com a verificação do que modelos maiores.

Conclusão

O Lean4Agent estabelece um novo paradigma para a IA verificável. Ao aplicar linguagens formais de tipos dependentes a sistemas de agentes, ele vai além da avaliação heurística para fornecer garantias matematicamente fundamentadas. O framework não apenas melhora o desempenho das tarefas, mas também oferece uma base para o desenvolvimento de agentes autônomos autossuficientes e confiáveis em domínios de alto risco. Os autores planejam abrir o código para fomentar mais pesquisas nesta área.