Resumo Técnico: VASO – Habilidades Autoevolutivas Formalmente Verificáveis para Agentes de IA Física

Declaração do Problema

Habilidades robóticas reutilizáveis servem como a interface entre modelos de fundação e o controle físico, permitindo que agentes incorporados executem tarefas de longo horizonte sob restrições de segurança. Embora os modelos de fundação tenham reduzido o custo de geração dessas habilidades a partir de linguagem natural, eles não resolveram o problema da garantia de habilidade. Os métodos de autoevolução existentes dependem de sinais de feedback "suaves" — como resultados de execução, testes unitários, recompensas do ambiente ou autocrítica de LLMs. Esses sinais fornecem apenas evidência de nível de traço, demonstrando que uma habilidade funcionou em execuções amostradas, mas falhando em garantir que os planos induzidos pela habilidade satisfaçam contratos de segurança temporal sob condições não testadas. Na robótica, uma única violação de segurança rara, mas severa (ex: um robô terrestre movendo-se após detectar uma pessoa), é inaceitável, embora o feedback suave muitas vezes falhe em detectar esses casos extremos.

O desafio central é fechar o loop entre a verificação formal e a evolução da habilidade sem apenas filtrar planos inseguros ou ajustar os pesos do modelo. Há uma necessidade de uma representação onde contraexemplos formais possam atualizar diretamente os contratos de habilidades reutilizáveis, garantindo que as melhorias sejam inspecionáveis, reutilizáveis e verificáveis.

Metodologia: Estrutura VASO

Os autores propõem o VASO (Verification-Guided Automated Skill Optimization), uma estrutura de ciclo fechado para a autoevolução de contratos de habilidades de robôs gerados por LLM. O VASO opera tratando as habilidades como contratos semânticos que acoplam uma interface formal a uma interface voltada ao planejador.

1. Representação de Habilidade Verificável

Uma habilidade $sk$ é definida como uma tupla $(G, \psi_{sk}, C_{sk})$:

• $G$ (Especificações Globais): Um conjunto de fórmulas LTL que representam restrições de segurança que devem sempre ser mantidas.
• $\psi_{sk}$ (Regra Local): Uma fórmula LTL que define a intenção ou o objetivo específico da habilidade.
• $C_{sk}$ (Contrato Semântico): O componente central consistindo de:
  • $L_{sk}$ (Função de Rotulagem Alinhada a Proposições): Uma função que mapeia estados de baixo nível do robô, observações e comandos de controle para proposições lógicas atômicas. Isso faz a ponte entre a execução física e a verificação de modelos simbólica.
  • $C^p_{sk}$ (Template de Plano Baseado em Texto): Um prior comportamental que guia o planejador na geração de comandos executáveis (ex: chamadas de API ou trajetórias).

2. Ciclo de Verificação de Dois Níveis

O VASO emprega um processo de verificação hierárquica para refinar habilidades:

• Verificação de Nível de Habilidade (Checagem de Viabilidade): Antes de amostrar planos, a estrutura verifica se a regra local $\psi_{sk}$ é logicamente consistente com as especificações globais $G$. Um sistema de transição universal é construído para verificar a satisfatibilidade. Se a regra local contradiz a segurança global (ex: uma regra comandando movimento quando uma pessoa é observada), a habilidade é rejeitada e o modelo de fundação é consultado para refinar a regra local.
• Verificação de Nível de Plano (Checagem Comportamental): Uma vez obtida uma habilidade viável, um planejador gera um plano executável $\pi$. Este plano é compilado em um sistema de transição simbólico (autômato) usando a função de rotulagem $L_{sk}$. Um verificador de modelos (NuSMV) verifica o plano contra $G \land \psi_{sk}$.

3. Otimização via Gradientes Textuais

Quando a verificação falha, o verificador de modelos retorna um traço de contraexemplo. O VASO converte esse traço em um gradiente textual (ex: "violar especificação: $G(\text{pessoa\_observada} \to X \text{ parar})$"). Esse feedback textual é alimentado de volta no modelo de fundação para atualizar o contrato semântico $C_{sk}$ e a regra local $\psi_{sk}$.

• Restrição Chave: Os pesos do modelo de fundação permanecem congelados. A otimização ocorre inteiramente no nível do prompt/contrato, refinando o artefato de habilidade reutilizável em vez de ajustar os parâmetros do modelo ou um único prompt de tarefa.
• Processo: O loop alterna entre geração direta (Contrato $\to$ Plano $\to$ Autômato) e refinamento reverso (Autômato $\to$ Gradiente Textual $\to$ Contrato Atualizado).

Principais Contribuições

1. Representação de Habilidade Autoevolutiva Verificável: O artigo introduz uma estrutura de habilidade que conecta explicitamente especificações de lógica temporal, semântica de robô alinhada a proposições e templates voltados ao planejador. Isso permite que habilidades geradas por LLM sejam usadas para planejamento enquanto permanecem expostas à verificação formal.
2. Contraexemplos Formais como Feedback de Otimização: Os autores desenvolvem um ciclo de verificação de dois níveis onde traços de contraexemplo são convertidos em gradientes textuais. Isso permite o refinamento do próprio contrato de habilidade reutilizável, em vez de apenas rejeitar um plano específico ou ajustar um prompt.
3. Validação de Agente Físico: A estrutura é validada em plataformas robóticas reais (Clearpath Jackal e quadricóptero PX4), demonstrando que habilidades otimizadas podem alcançar alta conformidade de especificação formal sem o ajuste fino (fine-tuning) do modelo de fundação subjacente.

Resultados Empíricos

A estrutura foi avaliada em 11 especificações de lógica temporal através de 400 planos gerados em duas plataformas robóticas.

• Conformidade: O VASO alcançou 97,2% de conformidade com a especificação formal utilizando menos de 100 amostras de otimização (menos de 20 minutos por habilidade).
• Comparação: Superou baselines zero-shot, métodos de otimização de prompt (como LAD-VF) e abordagens baseadas em ajuste fino (como RLVF). Notavelmente, o VASO atingiu pontuações de segurança mais altas que os métodos de ajuste fino, exigindo apenas uma fração do custo e tempo de treinamento.
• Generalização: Habilidades otimizadas demonstraram forte generalização para prompts de tarefas não vistas dentro da mesma família de tarefas, mantendo altas taxas de segurança e conclusão de tarefas sem refinamento adicional.
• Alinhamento Automático: O estudo mostrou que funções de rotulagem geradas automaticamente e alinhadas a proposições tiveram desempenho equivalente a mapeamentos feitos à mão, eliminando a necessidade de expertise de domínio manual para definir abstrações simbólicas.

Significância e Alegações

O artigo afirma ser a primeira estrutura a fechar o loop entre verificação formal e habilidades autoevolutivas geradas por LLM para agentes de IA física.

• Mudança de Paradigma: Ao contrário dos pipelines padrão de planejamento verificado que usam a verificação meramente como um filtro de passagem/falha para planos pontuais, o VASO usa a razão para a rejeição (o contraexemplo) para melhorar a fonte do plano (a habilidade reutilizável).
• Eficiência e Segurança: Ao otimizar o contrato da habilidade em vez dos pesos do modelo, o VASO fornece um mecanismo para gerar comportamentos mais seguros e confiáveis que são inspecionáveis e reutilizáveis em diferentes tarefas, abordando o gargalo crítico da garantia de habilidade na IA física.
• Limitações: Os autores reconhecem que as garantias formais são condicionais à correção da função de rotulagem alinhada a proposições gerada por IA. Erros no mapeamento de dinâmicas de baixo nível para proposições simbólicas podem levar a resultados de verificação espúrios, embora dados empíricos sugiram que isso ocorre infrequentemente (<1% de degradação nos escores de segurança). A estrutura atual também assume execução sequencial, não concorrente.