Resumo Técnico: U-Define: Projetando Fluxos de Trabalho do Usuário para Restrições Rígidas e Flexíveis em Planejamento Baseado em LLM

1. Declaração do Problema

Embora os Modelos de Linguagem de Grande Escala (LLMs) tenham reduzido a barreira para o planejamento de tarefas por usuários finais, sua natureza de "caixa preta" introduz problemas significativos de confiabilidade. LLMs frequentemente produzem planos inconsistentes, falham em impor requisitos estritos e geram saídas com raciocínio confiante, porém errôneo. Abordagens de verificação existentes, como críticos externos ou verificação formal, frequentemente dependem de modelos rígidos pré-engenhariados ou especificações específicas de domínio que limitam a flexibilidade. Por outro lado, abordagens puramente de restrições flexíveis (por exemplo, pesos numéricos ou preferências flexíveis) são frequentemente difíceis de interpretar pelos usuários e falham em garantir regras críticas de segurança ou lógica.

O desafio central abordado por este trabalho é projetar um fluxo de trabalho de interação que permita aos usuários expressar e equilibrar de forma confiável restrições rígidas (regras que nunca devem ser violadas) e restrições flexíveis (preferências que refletem flexibilidade) dentro do planejamento baseado em LLM, sem exigir que os usuários aprendam linguagens de especificação formal ou dependam de modelos rígidos.

2. Metodologia e Design do Sistema

Os autores propõem o U-Define, um sistema que operacionaliza um fluxo de trabalho onde os usuários definem restrições em linguagem natural, categorizam-nas por rigor e recebem resultados de verificação adaptados a cada tipo de restrição. O sistema estende trabalhos anteriores (VeriPlan) removendo dependências de modelos e introduzindo uma arquitetura de verificação híbrida.

Arquitetura do Sistema

O U-Define estrutura o processo de planejamento em três etapas:

1. Etapa de Definição:

   • Entrada: Os usuários inserem restrições em linguagem natural e as categorizam como Rígidas ou Flexíveis.
   • Tradutor de Regras: Um agente LLM especializado (ajustado no LLaMA 7B usando o conjunto de dados NL2LTL) traduz restrições rígidas definidas pelo usuário em propriedades de Lógica Temporal Linear (LTL).
   • Conversão PRISM: As propriedades LTL são posteriormente traduzidas para a linguagem de modelagem PRISM, um formato necessário para verificação de modelos probabilísticos.
   • Validação: O sistema converte as regras formais de volta para linguagem natural para verificação do usuário antes de prosseguir.

2. Etapa de Verificação:

   • Geração de Plano: Um Planejador LLM gera planos candidatos com base no prompt da tarefa do usuário e nas restrições.
   • Verificação de Restrições Rígidas: O plano gerado é convertido para o formato PRISM. Um Verificador de Modelo formal (usando PRISM e Stormpy) explora exaustivamente o espaço de estados do plano para verificar a adesão às regras LTL. Retorna um resultado binário de validade e uma lista de regras específicas violadas.
   • Verificação de Restrições Flexíveis: Um agente LLM-como-Juiz avalia o plano contra restrições flexíveis. Fornece uma classificação de 1 a 5 estrelas e uma explicação em linguagem natural sobre o grau de alinhamento com as preferências do usuário.

3. Etapa de Feedback:

   • Os usuários revisam os planos classificados (priorizados por violações de restrições rígidas) e as saídas de verificação.
   • Os usuários podem refinar iterativamente as restrições, ajustar o rigor das regras ou modificar o prompt. O sistema regenera o plano e o re-verifica, criando um ciclo de feedback fechado.

Implementação Técnica

• Agentes LLM: A maioria dos agentes usa GPT-4. O Tradutor de Regras usa um modelo LLaMA 7B ajustado.
• Verificação Formal: Utiliza PRISM e Stormpy para verificação de modelos.
• Avaliação: O sistema foi avaliado através de uma avaliação técnica em nível de componente (medindo a precisão da tradução) e dois estudos com usuários.

3. Contribuições Principais

Contribuições Técnicas

• Pipeline de Tradução Automatizada: Um pipeline automatizado que traduz restrições rígidas em linguagem natural para artefatos de verificação formal (LTL e PRISM) usando LLMs, eliminando a necessidade de modelos de domínio pré-engenhariados.
• Mecanismo de Verificação Híbrido: Um sistema que aplica métodos de verificação distintos com base no tipo de restrição: verificação de modelo formal para restrições rígidas (garantindo correção) e avaliação LLM-como-juiz para restrições flexíveis (avaliando o alinhamento de preferências).

Contribuições de Sistema

• Interface U-Define: Uma interface de usuário que permite a definição simultânea de restrições rígidas e flexíveis, visualizando-as por meio de um layout de mapa mental e apresentando feedback de verificação diferenciado (listas de violação vs. classificações em estrelas).

Contribuições Empíricas

• Estudos com Usuários: Dois estudos foram conduzidos:
  1. Estudo 1 (Usuários Gerais): Um estudo de ablação intra-sujeitos com 12 participantes em três cenários (férias, casamento, planejamento de receitas).
  2. Estudo 2 (Especialistas de Domínio): Um estudo com 6 especialistas de diversas áreas (educação, construção, finanças) executando tarefas de planejamento profissional.
• Descobertas:
  • Valor Percebido: O sistema completo (C1) superou significativamente as condições de ablação (Apenas Flexível, Apenas Rígido, Nenhum) em utilidade percebida, satisfação e desempenho.
  • Papéis Distintos: Os usuários perceberam restrições rígidas e flexíveis como desempenhando papéis complementares: restrições rígidas forneciam uma base não negociável, enquanto restrições flexíveis permitiam personalização.
  • Rigidez vs. Flexibilidade: Condições apenas rígidas levaram a menos iterações, mas menor satisfação devido à rigidez e latência. Condições apenas flexíveis incentivaram a exploração, mas sofreram com explicações pouco confiáveis e lacunas de verificação.
  • Desafios de Especialistas: Especialistas valorizaram o sistema para gerenciar regras estritas, mas enfrentaram "sobrecarga de contexto" ao lembrar e inserir inúmeras restrições. Eles também notaram que algumas restrições profissionais (limites numéricos, lógica de calendário) excediam a expressividade do LTL.

4. Resultados e Significado

Desempenho Técnico

• Tradução LTL: O LLM ajustado alcançou uma similaridade média de Levenshtein de 83,12% em relação à verdade fundamental gerada por humanos. Os erros foram principalmente no nível de predicado (por exemplo, incompatibilidades de tokens) em vez de erros de operadores lógicos.
• Conversão PRISM: A conversão do plano PRISM alcançou 97,4% de similaridade, com erros também ocorrendo no nível de predicado.

Experiência do Usuário e Implicações de Design

O artigo afirma que o U-Define conecta com sucesso a lacuna entre a confiabilidade da verificação determinística e a flexibilidade da IA generativa. As principais implicações de design derivadas dos resultados incluem:

1. Suporte a Restrições Mistas: Os sistemas devem permitir que os usuários distinguam explicitamente entre restrições rígidas e flexíveis para equilibrar confiabilidade e personalização.
2. Explicações Acionáveis: Explicações para restrições rígidas devem listar explicitamente as regras violadas em vez de fornecer classificações escalares genéricas, que os usuários acharam confusas para restrições flexíveis.
3. Gerenciamento de Contexto: Sistemas futuros devem auxiliar os usuários na redução da sobrecarga cognitiva da entrada de restrições (por exemplo, por meio de modelos, perfis reutilizáveis ou integração com ferramentas externas), uma necessidade crítica identificada por especialistas de domínio.
4. Cobertura de Verificação: Os sistemas devem indicar transparentemente quando uma restrição do usuário não pode ser totalmente verificada pelo motor formal (por exemplo, restrições numéricas) e tratar essas partes como verificações heurísticas.

Significado

O artigo argumenta que o suporte eficaz ao planejamento exige dar aos usuários controle sobre como as restrições são expressas e aplicadas. Ao colocar a autoridade para definir o rigor das restrições nas mãos do usuário e associá-la a mecanismos de verificação apropriados, o U-Define demonstra que é possível criar sistemas de planejamento que são tanto confiáveis (através da verificação formal de regras críticas) quanto adaptáveis (através do gerenciamento flexível de preferências). Esta abordagem aborda as limitações da verificação puramente baseada em modelos e do planejamento puramente generativo, oferecendo um caminho para uma colaboração humano-IA mais confiável em cenários complexos do mundo real.