Reliable Reasoning with Large Language Models via Preference-Based Maximum Satisfiability

Resumo Técnico: Raciocínio Confiável com Modelos de Linguagem de Grande Escala via Satisfatibilidade Máxima Baseada em Preferências

Declaração do Problema

Os Modelos de Linguagem de Grande Escala (LLMs) demonstram capacidades robustas na compreensão de linguagem natural e geração de código, mas exibem confiabilidade significativa quando encarregados de problemas complexos de otimização envolvendo múltiplas restrições e preferências definidas pelo usuário. Em domínios como robótica e logística, onde a correção e a optimalidade comprovável são críticas, os LLMs frequentemente falham em satisfazer restrições rígidas ou minimizar funções objetivo ao dependerem exclusivamente do raciocínio interno (por exemplo, Cadeia de Pensamento) ou da geração direta de respostas. Essas falhas decorrem da natureza combinatória da otimização e da incapacidade do LLM de realizar raciocínio exato, levando a soluções inviáveis ou subótimas que são difíceis de verificar. Além disso, os métodos formais existentes, como a Satisfatibilidade Máxima (MaxSAT), exigem que os usuários expressem preferências em linguagens especializadas e rígidas (por exemplo, PDDL), criando uma barreira de entrada para não especialistas.

Metodologia

O artigo propõe uma abordagem neuro-simbólica híbrida que externaliza o raciocínio do LLM para um solucionador formal. O paradigma central, denominado "vibe coding", envolve o LLM traduzindo descrições de problemas em linguagem natural em código Python executável, que é então resolvido por um solucionador exato de MaxSAT.

O pipeline proposto consiste nas seguintes etapas:

1. Planejamento Intermediário: Antes de gerar o código, o LLM é instruído a produzir uma descrição simbólica e estruturada das variáveis de decisão, restrições rígidas e preferências suaves. Esta etapa visa melhorar a precisão da modelagem ao forçar uma decomposição sistemática do problema.
2. Geração de Código: O LLM gera código Python usando a API PySAT para codificar o problema como uma instância de MaxSAT parcial ponderada. As restrições rígidas são codificadas como cláusulas rígidas, enquanto as preferências do usuário são codificadas como cláusulas suaves ponderadas.
3. Resolução MaxSAT: O código gerado é executado para invocar um solucionador MaxSAT (especificamente o RC2 do PySAT). O solucionador garante que a atribuição retornada seja viável (satisfaz todas as cláusulas rígidas) e ótima (minimiza o peso total das cláusulas suaves não satisfeitas) em relação ao problema codificado.
4. Verificação: Para avaliar o sistema sem depender do raciocínio interno do LLM, os autores constroem uma codificação MaxSAT "canônica" para cada instância de problema. Esta codificação canônica serve como verdade fundamental apenas para verificação. A solução produzida pelo código gerado pelo LLM é verificada contra esta codificação canônica para checar:
   • Viabilidade: A solução satisfaz todas as restrições rígidas?
   • Optimalidade: A solução alcança o mesmo valor objetivo que a solução ótima canônica?
   • Nota: Esta verificação permite codificações alternativas e múltiplas soluções ótimas, desde que sejam corretas sob a semântica de referência.
5. Loop de Feedback: Se o código falhar na execução ou produzir um erro, a mensagem de erro é retornada ao LLM para refinamento. Crucialmente, os resultados de verificação canônica (checagens de viabilidade/optimalidade) não são usados como feedback para o modelo durante o processo de geração, a fim de evitar vazamento de dados ou sobreajuste à referência.

Contribuições Principais

• Framework Neuro-Simbólico: Os autores apresentam um método onde os LLMs atuam como interfaces de linguagem natural para solucionadores de MaxSAT parcial ponderada, traduzindo a intenção do usuário em formulações formais de MaxSAT via geração de código.
• Verificação Independente: O estudo introduz um protocolo de avaliação que verifica soluções geradas por LLMs contra uma codificação canônica tanto para viabilidade quanto para optimalidade, desacoplando a validade da solução da correção do raciocínio interno do LLM.
• Análise Empírica de Preferências: O artigo analisa como diferentes configurações de preferências definidas pelo usuário impactam o desempenho do raciocínio do LLM em vários problemas de otimização com restrições.
• Avaliação do Planejamento Intermediário: O trabalho investiga a eficácia de uma etapa de planejamento intermediário, constatando que ela melhora o desempenho para modelos mais fortes, mas pode introduzir propagação de erros para modelos mais fracos.

Resultados Experimentais

A abordagem foi avaliada em três famílias de tarefas de raciocínio baseadas em preferências: Conjunto Independente Máximo (MIS), Agendamento e Cobertura de Conjuntos. O conjunto de dados compreendeu 300 instâncias (25 por família × 4 variantes de preferência) testadas em quatro LLMs (GEMINI-3.1-PRO, GPT-5.5, LLAMA3.3 e QWEN3-CODER).

• Desempenho de Linha de Base: As linhas de base de resposta direta e Cadeia de Pensamento (CoT) apresentaram desempenho pobre, frequentemente alcançando taxas de aceitação de 0% nas tarefas MIS e Agendamento. As linhas de base de Programa de Pensamento (PoT) mostraram ligeiras melhorias, mas permaneceram significativamente inferiores à abordagem baseada em MaxSAT.
• Desempenho do Pipeline MaxSAT: O pipeline baseado em MaxSAT proposto alcançou taxas de aceitação substancialmente mais altas. Para modelos fortes como GEMINI-3.1-PRO e GPT-5.5, as taxas de aceitação excederam 80% nas tarefas de Cobertura de Conjuntos e atingiram aproximadamente 56–59% nas tarefas de Agendamento e MIS quando o planejamento intermediário foi utilizado.
• Impacto do Planejamento: O planejamento intermediário melhorou consistentemente o desempenho para os modelos mais fortes (por exemplo, o GEMINI-3.1-PRO melhorou de 36% para 56% no MIS). No entanto, para modelos mais fracos (LLAMA3.3, QWEN3-CODER), o planejamento às vezes degradou o desempenho, sugerindo que a propagação de erros pode ocorrer se o modelo não puder traduzir fielmente o plano em código executável.
• Sensibilidade às Preferências: Embora as preferências do usuário geralmente tenham reduzido as taxas de aceitação em comparação com a configuração "sem preferência", a abordagem baseada em MaxSAT permaneceu mais robusta que as linhas de base em todas as variantes de preferência.

Significado e Alegações

O artigo alega que sua contribuição primária não é uma nova arquitetura de solucionador, mas uma demonstração empírica e metodológica do uso de LLMs como interfaces para solucionadores formais para otimização consciente de preferências. Os autores afirmam que:

1. A Externalização é Fundamental: Os LLMs não devem ser confiados para realizar raciocínio de otimização internamente; em vez disso, são altamente eficazes na tradução de restrições em linguagem natural para código executável.
2. Confiabilidade via Solucionadores: Ao delegar a otimização e a verificação para solucionadores MaxSAT sólidos e completos, o sistema alcança garantias formais de viabilidade e optimalidade que o raciocínio puro de LLM não pode fornecer.
3. Robustez: A combinação de interpretação semântica impulsionada por LLM e resolução MaxSAT permite tomada de decisão robusta e verificável que acomoda preferências do usuário sem exigir linguagens de domínio especializadas.

Os autores concluem que separar a interpretação semântica (LLM) da otimização formal (solucionador MaxSAT) é uma direção promissora para construir sistemas de tomada de decisão confiáveis e voltados para o usuário, particularmente em campos onde a correção é primordial. Eles observam que trabalhos futuros explorarão configurações interativas onde os usuários podem refinar iterativamente as preferências com o suporte deste loop neuro-simbólico.