Resumo Técnico: MANTRA – Sintetizando Benchmarks de Conformidade Validados por SMT

Declaração do Problema

Agentes de Grandes Modelos de Linguagem (LLM) que utilizam ferramentas estão cada vez mais implantados em domínios críticos, como operações empresariais, saúde e reservas de viagens, onde seu comportamento deve aderir a manuais procedimentais estritos. Um desafio fundamental na avaliação desses agentes é o "descompasso" entre a entrada e a saída: as regras procedimentais são tipicamente escritas em linguagem natural não estruturada para interpretação humana, enquanto o comportamento do agente se manifesta como uma sequência de chamadas de ferramentas (rastros de execução).

Os métodos de avaliação existentes sofrem de limitações significativas:

• Construção Manual: Criar benchmarks manualmente é de alta qualidade, mas não escala para manuais grandes e complexos ou novos domínios.
• Juízes Baseados em LLM: Embora mais fáceis de implantar, esses juízes lutam para impor de forma confiável restrições temporais estritas, pré-condições e ações proibidas ao longo de rastros de execução longos, levando a avaliações pouco confiáveis.
• Avaliação Apenas de Resultado: Muitos benchmarks verificam apenas o estado final, falhando em detectar se um agente chegou ao resultado correto por meio de um caminho procedimental não conforme.

Falta um método escalável e reproduzível para gerar automaticamente benchmarks de conformidade em nível de trilha a partir de manuais em linguagem natural que forneçam correção determinística e verificável por máquina.

Metodologia: O Framework MANTRA

O MANTRA (MANual-to-Test-tRAnslation) é um framework projetado para sintetizar automaticamente benchmarks de conformidade a partir de documentos procedimentais em linguagem natural e esquemas de ferramentas. Ele opera através de um pipeline de três estágios que combina geração por LLM com verificação formal:

1. Ingestão de Documentos e Geração de Cenários

• Construção de Grafo de Dependência: O sistema ingere um manual procedimental ($D$) e constrói um grafo de dependência ($G_D$) onde os nós representam fragmentos de conteúdo (por exemplo, parágrafos) e as arestas representam relações hierárquicas e de referência.
• Amostragem Orientada por Cobertura: Para controlar a complexidade da tarefa e garantir ampla cobertura, o MANTRA amostra subgrafos ($G_{DS}$) de $G_D$. Subgrafos pequenos e densos geram cenários simples; subgrafos maiores ou pouco conectados induzem cenários complexos envolvendo múltiplas regras.
• Relevância de Ferramentas e Síntese de Cenários: Para cada amostra, um LLM identifica as ferramentas relevantes ($T_S$) e gera cenários concretos ($\lambda$). Cada cenário inclui um prompt em linguagem natural ($p_\lambda$) e uma valoração de variáveis, incluindo variáveis de estado interno (por exemplo, "solicitação está pendente") que são tornadas explícitas no prompt para guiar o agente.

2. Geração de Verificações e Criação do Modelo de Mundo

Para avaliar a conformidade de forma determinística, o MANTRA gera dois artefatos independentes para cada cenário:

• Verificações em Nível de Trilha ($C_\lambda$): Um LLM gera um conjunto de verificações booleanas especificando chamadas de ferramentas obrigatórias, chamadas proibidas e ordenação temporal (por exemplo, check_inventory deve preceder assign_warehouse_picker). Essas verificações são fundamentadas com valores de argumentos concretos.
• Modelo de Mundo Simbólico ($W_S$): Independentemente, um LLM gera um modelo de mundo representando as regras procedimentais como um sistema de transição de estados. Este modelo é expresso em uma Linguagem Específica de Domínio (DSL) tipada, definindo variáveis de estado, pré-condições de ferramentas e pós-condições. Esta abstração permite uma representação compacta de lógica procedimental complexa.

3. Validação Cruzada via Resolução SMT

A inovação central do MANTRA é o uso de solucionadores de Satisfiability Modulo Theories (SMT) (especificamente Z3) para validar cruzadamente as verificações geradas e o modelo de mundo.

• Verificação de Modelo Limitado: Tanto $C_\lambda$ quanto $W_S$ são compilados em codificações SMT limitadas ($b\Phi_h$) sobre um horizonte de trilha $h$.
• Busca por Conflitos: O sistema busca dois tipos de inconsistências:
  1. Conflito Forward: Rastros que satisfazem as verificações, mas violam o modelo de mundo (indicando que as verificações são muito fracas ou o modelo é muito restritivo).
  2. Conflito Backward: Rastros que satisfazem o modelo de mundo, mas violam uma verificação específica (indicando que a verificação é muito restritiva).
• Loop Estruturado de Reparo: Quando conflitos são encontrados, o MANTRA emprega um loop de reparo:
  • Resolução do Modelo de Mundo: Se múltiplos cenários da mesma amostra compartilharem um conflito, um LLM propõe um reparo compartilhado ao modelo de mundo (por exemplo, adicionar uma pré-condição ausente).
  • Resolução de Verificações: Se os conflitos persistirem, o sistema identifica e repara verificações específicas para cenários individuais.
  • Edições Determinísticas: Os reparos são aplicados via uma linguagem de edição tipada para garantir a boa formação, seguidos de recompilação e revalidação.
• Humano no Loop: Se os reparos automatizados falharem após um número definido de iterações, o sistema sinaliza o cenário para revisão humana estruturada, onde um revisor pode resolver manualmente ambiguidades.

Principais Contribuições

1. Pipeline Automatizado: Um pipeline totalmente automatizado para converter manuais em linguagem natural e esquemas de ferramentas em benchmarks verificáveis por máquina, com dificuldade de tarefa controlável e correção determinística.
2. Formulação de Dois Artefatos: A separação de verificações em nível de trilha e modelos de mundo simbólicos, que são validados cruzadamente via resolução SMT. Isso permite a identificação e reparo automáticos de inconsistências antes que os benchmarks sejam aceitos, minimizando a intervenção humana.
3. Suite de Benchmarks: A criação de uma nova suite de benchmarks contendo 285 tarefas diversas em 6 domínios (Operações, Sneaky Sasquatch, Segurança da Cabine, Varejo, Companhia Aérea, Telecomunicações). Essas tarefas escalonam para manuais procedimentais de até ~16.000 palavras e 148 ferramentas, com esforço humano mínimo.
4. Análise Granular de Falhas: O framework fornece verificações em nível de trilha que permitem a depuração detalhada dos modos de falha do agente, distinguindo entre chamadas ausentes, violações de ordenação e ações proibidas.

Resultados e Avaliação

Os autores avaliaram o framework MANTRA e os benchmarks resultantes usando 6 agentes LLM diferentes.

• Eficiência de Validação: A validação cruzada baseada em SMT validou com sucesso uma parte significativa dos casos de teste gerados automaticamente. Por exemplo, no domínio "Operações", 63 de 66 casos gerados foram validados após rodadas de refinamento forward e backward.
• Desempenho do Agente: A avaliação revelou que os agentes LLM atuais lutam com a conformidade procedimental. As taxas de sucesso variaram significativamente por domínio, com "Varejo" e "Companhia Aérea" (do $\tau$-Bench) provando-se particularmente difíceis devido ao uso complexo de ferramentas, e não ao comprimento do documento.
• Análise de Modo de Falha: A análise de 10.895 verificações falhas mostrou que 76% das falhas foram devidas a "Chamada-Obrigatória-Ausente" (pular uma ferramenta mandatória) ou "Ancoragem-Ausente" (falhar em executar o pré-requisito para uma cláusula de ordenação).
  • Um padrão de falha dominante foi a "escrita prematura", onde agentes chamavam ferramentas do tipo escrita antes de realizar consultas do tipo leitura necessárias.
  • O modelo Qwen3.6:36B demonstrou desempenho superior, particularmente nos domínios de Companhia Aérea e Varejo, mantendo um hábito estrito de "ler antes de escrever", alcançando uma taxa de escrita prematura de 0% nesses domínios.
• Comparação com Benchmarks Existentes: Ao contrário de benchmarks existentes que dependem de construção manual ou juízes LLM, o MANTRA fornece avaliação determinística em nível de trilha que escala para documentos grandes e não estruturados e novos domínios com esforço humano mínimo.

Significado e Alegações

O artigo alega que o MANTRA demonstra a viabilidade de combinar geração automatizada de benchmarks com métodos de validação formalmente fundamentados para criar benchmarks escaláveis e confiáveis para agentes que utilizam ferramentas.

• Confiabilidade: Ao usar solucionadores SMT para validar cruzadamente verificações contra um modelo de mundo, o MANTRA garante que os benchmarks estejam livres de inconsistências lógicas que possam surgir de alucinações de LLM, fornecendo um maior grau de confiança nos resultados da avaliação em comparação com abordagens de LLM-como-juiz.
• Escalabilidade: O framework aborda o gargalo de escalabilidade da criação manual de benchmarks, permitindo a avaliação de agentes contra manuais procedimentais complexos e do mundo real (até 50+ páginas) em domínios arbitrários.
• Capacidade de Depuração: A granularidade das verificações em nível de trilha permite que os pesquisadores vão além de métricas simples de passar/falhar para entender falhas estruturais específicas no raciocínio do agente, como a tendência de pular consultas de pré-requisito.

Os autores posicionam o MANTRA não como uma garantia autônoma de comportamento seguro, mas como um componente crítico para o desenvolvimento de sistemas de IA mais confiáveis em configurações críticas para conformidade, fechando a lacuna entre aprendizado de máquina e verificação formal.