Can LLM Aid in Solving Constraints with Inductive Definitions?

Este artigo propõe uma abordagem neuro-simbólica que integra Grandes Modelos de Linguagem (LLMs) com solucionadores de restrições para gerar lemas auxiliares e verificar conjecturas, demonstrando uma melhoria de cerca de 25% na resolução de tarefas de prova envolvendo definições indutivas em comparação com os solucionadores de última geração.

O essencial

Imagine que você está tentando provar que uma receita de bolo é perfeita. Você tem as regras básicas (os ingredientes e o modo de fazer) e quer garantir que, não importa quantas vezes você repita o processo, o bolo sempre saia igual.

No mundo da computação, isso se chama verificação de programas. Mas, quando os programas têm regras que se repetem infinitamente (chamadas de "definições indutivas" ou recursivas), os computadores tradicionais (os "robôs matemáticos" chamados SMT solvers) muitas vezes travam. Eles sabem as regras, mas não conseguem "adivinhar" o passo intermediário mágico que falta para fechar o raciocínio. É como se eles soubessem como misturar a massa, mas não soubessem que precisam preaquecer o forno antes.

Este artigo apresenta uma solução criativa: colocar um "cérebro humano" (uma Inteligência Artificial generativa) para trabalhar junto com o "robô matemático".

Aqui está a explicação simplificada do que eles fizeram:

1. O Problema: O Robô Cego

Os computadores tradicionais são ótimos em lógica pura, mas péssimos em criatividade. Quando precisam provar algo complexo, eles tentam seguir um caminho rígido. Se o caminho exige um "atalho" (um lema auxiliar) que não está óbvio, eles ficam presos.

• Analogia: É como tentar abrir um cofre com uma chave mestra que só funciona se você girar a maçaneta de um jeito específico. O robô tenta girar em todas as direções, mas nunca acerta o ângulo certo porque não tem intuição.

2. A Solução: O Duplo Dinâmico (Neuro-Simbólico)

Os autores criaram uma equipe de dois:

• O Artista (LLM - Grande Modelo de Linguagem): É como um escritor criativo ou um matemático sonhador. Ele olha para o problema e diz: "E se a gente tentasse provar isso de outro jeito? Talvez precisemos de uma regra extra aqui." Ele gera conjecturas (palpites inteligentes).
• O Juiz (Solver Tradicional): É o rigoroso, o cético. Ele pega os palpites do Artista e diz: "Isso é verdade? Isso ajuda a provar o objetivo? Se não, descarto."

3. Como Funciona a Dança (O Fluxo de Trabalho)

O sistema funciona em três etapas, como um processo de seleção de talentos:

• Etapa 1: O Pedido Criativo (Prompting)
  Em vez de apenas pedir "me dê uma resposta", eles ensinaram o Artista a pensar como um humano.

  • Estratégia 1: "Vamos fazer passo a passo, como se estivéssemos desmontando um brinquedo." (Raciocínio equacional).
  • Estratégia 2: "Vamos simplificar o problema, tirando as partes difíceis e vendo se conseguimos encontrar um padrão." (Generalização).
    Isso evita que o Artista alucine ou dê respostas sem sentido.

• Etapa 2: O Filtro Rápido (Filter)
  O Artista pode gerar 100 ideias, mas 90 podem ser bobagens ou erros. Antes de gastar tempo verificando tudo, o sistema usa o Juiz para fazer uma triagem rápida. Se a ideia for obviamente errada ou inútil, ela é descartada na hora.

  • Analogia: É como um editor de jornal que joga fora os rascunhos mal escritos antes de mandar para o revisor principal.

• Etapa 3: A Validação Final (Validate)
  As ideias que passaram no filtro são testadas de verdade. O Juiz verifica se a ideia ajuda a provar o objetivo final. Se sim, o sistema usa essa nova regra para tentar provar o problema original. Se a nova regra também for difícil, o sistema chama o Artista de novo para ajudar a provar essa nova regra (recursão).

4. O Resultado: O Time Venceu

Eles testaram essa equipe em 706 problemas difíceis de lógica.

• Os robôs sozinhos (os melhores do mundo) resolveram cerca de 293 problemas.
• A equipe (Artista + Juiz) resolveu 525 problemas.
• Conclusão: Eles conseguiram provar cerca de 25% a mais de problemas do que a tecnologia atual consegue sozinha.

Resumo em uma frase

O papel mostra que, quando você combina a criatividade desenfreada de uma Inteligência Artificial (que sabe "adivinhar" o próximo passo lógico) com a rigorosa precisão de um verificador matemático (que garante que a resposta está certa), você consegue resolver quebra-cabeças lógicos que eram impossíveis para qualquer um dos dois sozinho.

É como ter um arquiteto visionário desenhando a ponte e um engenheiro civil calculando se ela vai cair: juntos, eles constroem algo que nenhum dos dois conseguiria fazer isoladamente.

Resumo técnico

Aqui está um resumo técnico detalhado do artigo "Can LLM Aid in Solving Constraints with Inductive Definitions?", apresentado em português:

1. O Problema

A resolução de restrições envolvendo definições indutivas (também conhecidas como definições recursivas) é um desafio significativo na verificação de programas. Essas definições aparecem frequentemente sob duas formas:

• Tipos de Dados Algébricos (ADTs): Como números naturais ou listas.
• Funções Recursivamente Definidas (RDFs): Funções que chamam a si mesmas em entradas menores.

Embora os solvers de SMT (Satisfiability Modulo Theories) e provadores de lógica de primeira ordem de última geração (como cvc5 e Vampire) ofereçam suporte limitado para indução, eles frequentemente falham em provar objetivos complexos que exigem lemas auxiliares. Métodos tradicionais de geração de lemas (exploração de teoria, generalização e métodos baseados em Cláusulas de Horn Constrainidas - CHCs) sofrem de limitações de escalabilidade, expressividade e dependência de heurísticas fixas, muitas vezes incapazes de descobrir lemas complexos necessários para completar a prova.

2. Metodologia Proposta

Os autores propõem uma abordagem neuro-simbólica que integra sinergicamente Grandes Modelos de Linguagem (LLMs) com solvers de restrições tradicionais. O objetivo é usar o LLM para gerar conjecturas (lemas candidatos) e o solver simbólico para verificar sua validade e utilidade.

O fluxo de trabalho consiste em três etapas principais:

A. Estratégia de Consulta (Prompting)

Para superar a aleatoriedade e as alucinações dos LLMs, foram desenhadas duas estratégias de prompt sofisticadas:

1. Raciocínio Equacional: Guia o LLM a realizar um raciocínio passo a passo, similar ao humano, usando reescrita de termos. O LLM identifica o caso base e o caso indutivo, transformando o lado esquerdo da equação usando axiomas e hipóteses indutivas. Quando um passo não pode ser derivado diretamente, o LLM gera uma conjectura para preencher a lacuna.
2. Reescrita de Termos e Generalização: Em vez de seguir passos rígidos, esta estratégia incentiva o LLM a identificar termos comuns no objetivo de prova, substituí-los por variáveis frescas para simplificar o problema, ou gerar lemas de "ponte" que conectam formas simplificadas ao objetivo original.

B. Filtragem (Filter)

Esta etapa visa eliminar rapidamente conjecturas incorretas ou inúteis antes de um custo computacional elevado. Um conjectura é filtrada (rejeitada) se:

• Contiver erros sintáticos.
• For idêntica ao objetivo de prova (o que não ajuda).
• For inconsistente com os axiomas (verificado via solver SMT com um timeout curto).

C. Validação (Validate)

As conjecturas que passam pela filtragem são submetidas a uma verificação rigorosa:

1. Utilidade: O solver verifica se a adição das conjecturas ao conjunto de axiomas permite provar o objetivo original.
2. Validade (Recursiva): Se úteis, as conjecturas tornam-se novos sub-objetivos. O sistema recursivamente tenta provar que cada conjectura é um teorema válido derivado dos axiomas originais. Se todos os sub-objetivos forem provados, a prova original é concluída.

3. Principais Contribuições

• Abordagem Neuro-Simbólica: Integração iterativa de LLMs (para geração criativa de lemas) e solvers SMT (para verificação rigorosa), superando as limitações de métodos puramente lógicos.
• Estratégias de Prompting Específicas: Desenvolvimento de técnicas de prompting que imitam o raciocínio indutivo humano e a generalização, direcionando o LLM para gerar lemas estruturalmente úteis.
• Pipeline de Filtragem e Validação: Um mecanismo robusto para lidar com a incerteza dos LLMs, garantindo que apenas conjecturas válidas e úteis sejam usadas na prova final.
• Ferramenta LLM4Ind: Implementação de uma ferramenta de código aberto que automatiza esse processo.

4. Resultados Experimentais

Os autores avaliaram a abordagem em um conjunto de benchmarks diversificado (706 tarefas), incluindo conjuntos como StandardDT, StandardDTLIA, AutoProof e IndBen, comparando com solvers de última geração (cvc5, Vampire, Racer).

• Desempenho Superior: O LLM4Ind resolveu significativamente mais tarefas do que os solvers base. Em média, houve um aumento de cerca de 25% no número de tarefas de prova resolvidas em comparação com o estado da arte.
  • Exemplo: No conjunto StandardDT, o LLM4Ind resolveu 212 tarefas contra 150 do cvc5.
• Robustez: O sistema demonstrou ser robusto a diferentes modelos de LLM (DeepSeek, Qwen, Gemini, GPT-5) e a diferentes temperaturas de amostragem, mantendo uma baixa variância nos resultados.
• Eficiência de Custo: Estudos de ablação mostraram que as estratégias de prompt e o mecanismo de filtragem são cruciais. Sem a filtragem, o tempo de resolução aumentava devido a conjecturas inúteis, e o consumo de tokens era maior.
• Tempo de Execução: Embora o tempo médio de resolução seja maior (aprox. 100s) do que em solvers tradicionais (que levam segundos), o tempo é considerado aceitável para tarefas de verificação onde a correção é prioritária.

5. Significado e Impacto

Este trabalho representa um avanço significativo na automação da verificação de programas, especialmente em cenários que envolvem tipos de dados complexos e funções recursivas.

• Superação de Limitações Lógicas: Demonstra que os LLMs podem aprender a "pensar" indutivamente e gerar lemas que os solvers puramente simbólicos não conseguem descobrir sozinhos.
• Paradigma Híbrido: Estabelece um novo paradigma onde a criatividade dos modelos de linguagem é contida e validada pela precisão matemática dos solvers formais, mitigando o risco de alucinações.
• Aplicabilidade Prática: A ferramenta LLM4Ind oferece uma solução prática para problemas de verificação que anteriormente exigiam intervenção manual extensiva de especialistas, potencialmente acelerando o desenvolvimento de software seguro e confiável.

Em resumo, o artigo prova que LLMs, quando adequadamente guiados e integrados a ferramentas formais, podem expandir drasticamente as fronteiras do que é possível provar automaticamente em lógica indutiva.