ConformalNL2LTL: Translating Natural Language Instructions into Temporal Logic Formulas with Conformal Correctness Guarantees

Resumo Técnico: ConformalNL2LTL

1. O Problema

A Lógica Temporal Linear (LTL) é uma linguagem formal amplamente utilizada para especificar missões complexas para sistemas autônomos (como vigilância, cobertura e coleta de dados), oferecendo garantias de correção e otimalidade aos planejadores de tarefas. No entanto, a especificação manual de missões em LTL exige um esforço significativo e expertise de domínio.

Para mitigar isso, métodos recentes tentam traduzir Instruções em Linguagem Natural (NL) diretamente para fórmulas LTL usando Grandes Modelos de Linguagem (LLMs). A limitação crítica dessas abordagens existentes é a falta de garantias de correção. Os LLMs podem gerar fórmulas LTL que não refletem com precisão a intenção original do usuário, e como esses modelos frequentemente operam sem quantificação de incerteza, erros podem passar despercebidos, resultando em planos robóticos falhos.

O objetivo do trabalho é desenvolver um algoritmo de tradução probabilisticamente correto que converta instruções NL em fórmulas LTL semanticamente equivalentes com uma taxa de sucesso definida pelo usuário (ex: 99%), minimizando a necessidade de intervenção humana.

2. Metodologia: ConformalNL2LTL

O método proposto, ConformalNL2LTL, utiliza uma combinação de LLMs e Predição Conformal (Conformal Prediction - CP) para garantir taxas de sucesso controladas. A abordagem baseia-se nos seguintes pilares:

• Tradução Iterativa como QA: O problema de tradução não é tratado como uma geração única, mas como uma sequência de tarefas interdependentes de Perguntas e Respostas (QA). Em cada passo $k$, o sistema pergunta ao LLM qual operador temporal/lógico ou proposição atômica (AP) deve ser adicionado para estender a fórmula LTL parcial construída até o momento.
• Arquitetura de Dois Modelos:
  • Modelo Primário ($\psi_p$): Responde às perguntas de QA.
  • Modelo Auxiliar ($\psi_{aux}$): Atua como um "segundo par de olhos" quando o modelo primário está incerto.
• Quantificação de Incerteza via CP:
  • Em vez de confiar na resposta mais provável do LLM, o sistema consulta o modelo múltiplas vezes ($m$ vezes) para obter uma distribuição de respostas.
  • A frequência das respostas é usada como uma métrica de confiança grosseira.
  • Predição Conformal: O sistema constrói um "conjunto de predição" (prediction set) para cada passo de QA. Este conjunto contém a resposta correta com uma probabilidade garantida definida pelo usuário ($1-\alpha$).
  • Se o conjunto de predição for um único elemento (singleton), a tradução prossegue automaticamente.
  • Se o conjunto tiver múltiplos elementos (indicando alta incerteza), o sistema solicita ajuda ao Modelo Auxiliar.
  • Se a interseção dos conjuntos de predição dos dois modelos ainda for ambígua, a intervenção de um usuário humano é solicitada para escolher a opção correta.
• Agregação Semântica: O método inclui um mecanismo para agrupar respostas semanticamente similares (ex: "carro" e "veículo") antes de calcular frequências, evitando que variações textuais inflacionem a incerteza artificialmente.

3. Contribuições Principais

1. Primeiro Algoritmo com Garantias de Sucesso: O ConformalNL2LTL é o primeiro método de tradução NL-to-LTL capaz de garantir taxas de sucesso definidas pelo usuário em instruções nunca vistas antes, sob suposições de distribuição i.i.d.
2. Aplicação de CP em LLMs Colaborativos: É a primeira aplicação de Predição Conformal em um cenário onde dois LLMs (abertos ou fechados) colaboram para resolver tarefas de QA interdependentes. O uso do modelo auxiliar reduz drasticamente a necessidade de intervenção humana.
3. Garantias Teóricas e Empíricas: O artigo fornece provas teóricas de que o método atinge a taxa de sucesso desejada ($1-\alpha$) e demonstra empiricamente que isso é alcançado com taxas de ajuda humana extremamente baixas.
4. Implementação e Dados: Os autores liberaram o código, datasets de calibração e teste, e demonstrações em robôs reais integrados a planejadores LTL.

4. Resultados Experimentais

Os experimentos foram realizados em tarefas de entrega e transporte de robôs móveis, com cenários classificados como fáceis, médios e difíceis.

• Taxa de Sucesso vs. Intervenção Humana:
  • Para uma taxa de sucesso alvo de 99%, o sistema alcançou uma taxa de sucesso empírica de 99,24%.
  • A taxa de ajuda humana (porcentagem de passos que exigiram intervenção) foi de apenas 0,378%.
  • A frequência de cenários que exigiram ajuda humana pelo menos uma vez foi de apenas 4%.
• Impacto do Modelo Auxiliar:
  • Ao remover o modelo auxiliar, a taxa de ajuda humana saltou de 0,378% para 7,43% (para 99% de sucesso), e a frequência de cenários com intervenção subiu de 4% para 36,5%. Isso demonstra que o modelo auxiliar resolve a maioria das ambiguidades antes que o humano precise intervir.
• Comparação com Baselines:
  • O método superou abordagens existentes (como Lang2LTL, nl2spec e variantes sem CP) em taxas de sucesso de tradução.
  • Baselines sem garantias de incerteza (UA-NL2LTL) tiveram taxas de sucesso de ~87%, enquanto o ConformalNL2LTL atingiu >99% com controle rigoroso.
• Robustez (Out-of-Distribution):
  • Em cenários fora da distribuição de treinamento (OOD), as garantias teóricas não se mantêm estritamente, mas o sistema ainda apresentou desempenho razoável (84,5% de sucesso para alvo de 99%), superando a intuição de falha total.

5. Significado e Impacto

O trabalho representa um avanço significativo na interseção entre Métodos Formais e Inteligência Artificial Generativa na robótica.

• Segurança e Confiabilidade: Ao fornecer garantias probabilísticas de que a especificação formal (LTL) corresponde à intenção do usuário, o método mitiga o risco de falhas catastróficas em sistemas autônomos críticos.
• Viabilidade de Implantação: A redução drástica na necessidade de intervenção humana (de ~36% para <1% ao usar o modelo auxiliar) torna a tradução automática de NL para LTL viável para implantação em ambientes do mundo real, onde a supervisão humana constante é impraticável.
• Modularidade: A abordagem de tradução separada do planejamento permite que o sistema seja integrado a qualquer planejador LTL existente, oferecendo rastreabilidade e facilidade de depuração de erros (separando erros de tradução de erros de planejamento).

Em resumo, o ConformalNL2LTL estabelece um novo padrão para a especificação de missões robóticas, combinando a flexibilidade da linguagem natural com a rigidez matemática das garantias de correção formal.