Projeto usa a linguagem Lean para criar 'guardrails' matematicamente verificáveis em agentes de IA

Um projeto chamado LeanGuard, disponível no GitHub, propõe uma abordagem diferente para lidar com um dos maiores desafios da IA generativa atual: como impedir que agentes autônomos executem ações indesejadas ou perigosas. Em vez de depender apenas de prompts cuidadosamente escritos ou filtros de conteúdo baseados em heurísticas, a ferramenta utiliza o Lean, uma linguagem de programação funcional e assistente de prova de teoremas amplamente usada em matemática formal e verificação de software.

De acordo com a publicação que circulou no Hacker News, a ideia central é permitir que desenvolvedores definam restrições de comportamento para agentes de IA de forma matematicamente precisa, de modo que seja possível provar — e não apenas assumir — que o agente respeitará determinadas regras em qualquer cenário coberto pela especificação. Esse tipo de garantia é significativamente mais forte do que os métodos convencionais de ‘guardrails’, que costumam funcionar por meio de exemplos, listas de bloqueio ou classificadores probabilísticos.

O uso do Lean não é trivial: a linguagem é conhecida por sua curva de aprendizado acentuada e por exigir familiaridade com lógica formal e prova de teoremas, algo bem distante do dia a dia da maioria dos times que constroem produtos de IA. Ainda assim, a proposta reflete uma tendência crescente na comunidade de segurança de IA: buscar métodos com bases matemáticas mais sólidas para conter comportamentos de agentes que operam com crescente autonomia, executando código, acessando ferramentas externas ou tomando decisões em múltiplas etapas sem supervisão humana constante.

Projetos como esse ainda estão em estágio inicial e não substituem outras camadas de segurança, como sandboxing, revisão humana e monitoramento em tempo de execução. Mas apontam para um caminho em que a verificação formal, historicamente restrita a sistemas críticos como software aeroespacial ou protocolos criptográficos, começa a ser explorada também no contexto de agentes de linguagem natural — uma área em que garantias determinísticas ainda são raras.