LLM2SMT: Building an SMT Solver with Zero Human-Written Code

O artigo apresenta o LLM2SMT, um estudo de caso em que um agente de codificação baseado em LLM construiu, sem nenhuma intervenção humana, um solver SMT completo e competitivo para a lógica QF_UF, implementando o algoritmo de fechamento de congruência de Nieuwenhuis-Oliveras e emitindo provas em Lean.

O essencial

Imagine que você pediu a um chef de cozinha robótico (uma Inteligência Artificial avançada) para criar um prato complexo do zero. O desafio? Você não pode escrever nenhuma receita, não pode cortar nenhum legume e nem pode tocar no fogão. Você só pode dar instruções verbais.

O que o robô faria? Ele tentaria, erraria, queimaria a comida, aprenderia com os erros e, eventualmente, criaria um prato delicioso?

É exatamente isso que os autores deste artigo fizeram, mas em vez de comida, eles pediram para a IA criar um cérebro matemático chamado SMT Solver.

Aqui está a história simplificada do que aconteceu:

1. O Desafio: Criar um "Detetive Lógico"

Um "SMT Solver" é um programa que responde a perguntas do tipo: "É possível organizar estas peças de um quebra-cabeça de forma que todas as regras sejam obedecidas ao mesmo tempo?"

• Se a resposta for Sim, ele mostra como montar.
• Se for Não, ele prova matematicamente que é impossível.

Os pesquisadores queriam ver se uma IA (especificamente um agente de codificação chamado Claude) conseguiria escrever o código desse "detetive" do zero, sem que um único humano tivesse digitado uma linha de código.

2. O Processo: O Aprendiz e o Mestre

A IA começou a trabalhar. No começo, foi um pouco caótico, como um estagiário muito inteligente, mas inexperiente:

• O Erro Inicial: A IA esqueceu de ensinar ao programa como lidar com a lógica básica (como "E", "OU" e "NÃO"). Foi como tentar construir um carro sem rodas.
• A Correção: Os pesquisadores apontaram o erro e a IA corrigiu.
• A Surpresa: A IA tentou criar seu próprio motor de busca (o "motor" do carro), mas era muito lento. Os pesquisadores disseram: "Não, use o motor que já existe e é rápido (CaDiCaL)". A IA obedeceu imediatamente e integrou a peça perfeita.

3. O Grande Obstáculo: O "Círculo de Espelhos"

Havia um tipo de problema matemático muito difícil, chamado "Problema do Diamante Equacional". Imagine que você tem várias pistas que parecem formar um círculo infinito, e o detetive precisa perceber que, no fundo, todas as pistas levam a uma contradição.

• A IA, sozinha, ficava girando em círculos tentando resolver isso.
• Os pesquisadores deram uma dica simples: "Olhe para o padrão e simplifique antes de começar a resolver".
• O Resultado: A IA criou uma técnica de "pré-processamento" genial. Ela aprendeu a olhar para o problema, simplificar as pistas óbvias e resolver o quebra-cabeça instantaneamente. Foi como se ela tivesse aprendido a ver o "macete" do jogo.

4. A Prova Final: O Advogado de Defesa

Para garantir que o detetive não estava mentindo, os pesquisadores pediram que a IA escrevesse um certificado de prova em uma linguagem chamada Lean (que é como um advogado escrevendo um argumento jurídico impecável para um juiz).

• Isso foi a parte mais difícil. A IA às vezes escrevia argumentos confusos ou que o "juiz" (o verificador de Lean) não entendia.
• Os pesquisadores tiveram que dar exemplos de como um argumento perfeito deveria parecer.
• No final, a IA conseguiu escrever provas que o juiz aceitou, confirmando que o detetive estava certo.

5. O Resultado: Um Campeão Inesperado

Quando testaram esse "robô detetive" criado por outro robô:

• Ele resolveu quase tantos problemas quanto os melhores programas do mundo (como o Z3 e o cvc5), que foram criados por décadas de trabalho de humanos brilhantes.
• Ele foi rápido e eficiente.
• O Pulo do Gato: A IA conseguiu até criar uma versão que era mais rápida em alguns casos porque ela não fazia passos desnecessários que os humanos costumam incluir por hábito.

O Que Aprendemos? (A Lição da História)

1. A IA é um gênio, mas precisa de supervisão: Ela consegue escrever código complexo e aprender com erros, mas se você não der limites claros (como "não fique girando em círculos" ou "use este motor"), ela pode se perder.
2. A "Inteligência Irregular": Às vezes, a IA resolve um problema super difícil, mas falha em algo bobo (como simplificar "A = A"). É como um pianista que toca uma sinfonia complexa, mas erra uma nota simples.
3. O Futuro: Isso prova que podemos usar IAs para criar ferramentas que ajudam a pensar e a provar verdades matemáticas. Não é que a IA vai substituir os humanos amanhã, mas ela pode ser um parceiro incrível que escreve o código enquanto nós focamos na lógica e na direção.

Em resumo: Os pesquisadores pediram a uma IA para construir um "cérebro matemático" do zero. A IA tropeçou, aprendeu, criou truques inteligentes e entregou um produto final que compete com os melhores do mundo. Tudo isso sem que um humano tenha digitado uma única linha de código. É como se você tivesse ensinado um aluno a escrever um livro de física, e ele tivesse escrito um best-seller, apenas com suas dicas.

Resumo técnico

Aqui está um resumo técnico detalhado do artigo "LLM2SMT: Building an SMT Solver with Zero Human-Written Code", apresentado em português.

1. O Problema

A questão central investigada pelo artigo é: Agentes de LLM (Large Language Models) são capazes de desenvolver ferramentas de raciocínio automatizado?
Embora haja um debate sobre a capacidade de LLMs escreverem software ou raciocinarem, a capacidade de um LLM criar um software que por si só realiza raciocínio lógico complexo (como um solucionador SMT) é um território inexplorado. O desafio reside na necessidade de correção absoluta; pequenos erros na implementação de lógica formal podem levar a falhas sutis e difíceis de detectar, comprometendo a confiabilidade do sistema. O objetivo foi construir um solucionador SMT completo para a teoria de funções não interpretadas sem quantificadores (QF_UF) sem que uma única linha de código fosse escrita manualmente por humanos.

2. Metodologia

O estudo foi conduzido utilizando o agente de codificação Claude Code com o modelo Sonnet 4.6. A abordagem seguiu os seguintes pilares:

• Especificação e Arquitetura: O projeto foi iniciado com uma descrição mínima, solicitando a implementação de um solucionador SMT estilo DPLL(T) em C++20. O agente foi instruído a usar:
  • ANTLR para análise sintática (parser) da linguagem SMT-LIB2.
  • CaDiCaL (via interface IPASIR-UP) como motor SAT.
  • A biblioteca de precisão arbitrária para números.
  • O algoritmo de Fechamento de Congruência (Congruence Closure) de Nieuwenhuis-Oliveras para a teoria QF_UF.
  • Lean para a emissão de provas de insatisfiabilidade.
• Iteração e Depuração (Zero Human Code):
  • O desenvolvimento não foi linear. O agente inicialmente falhou em lidar com conectivos booleanos e implementou seu próprio solucionador SAT rudimentar em vez de usar o CaDiCaL.
  • Humanos intervieram apenas fornecendo prompts corretivos, especificações de teorias (SMT-LIB) e instruções de recursos (ex: timeouts).
  • Ferramentas de Depuração: Para superar a "inteligência irregular" (jagged intelligence) do modelo, foram implementados:
    • Fuzzing: Um gerador de fórmulas aleatórias criado pelo próprio agente.
    • Delta-Debugging: Um script de teste diferencial comparando o solucionador do agente com um solucionador de referência.
    • Timeouts: Instruções permanentes para garantir que processos longos fossem interrompidos.
• Pré-processamento: O agente foi instruído a implementar técnicas de simplificação (propagação de unidades, curto-circuito). Um desafio específico foi o problema do "diamante equacional" (equational diamond), onde o solucionador precisava inferir igualdades transitivas não explícitas. O agente desenvolveu uma técnica de pré-processamento que calculava o fechamento de igualdades em cada ramo de uma disjunção e extraía consequências comuns.
• Certificação (Provas): Para fórmulas insatisfiáveis, o agente deveria gerar provas em Lean. O processo envolveu traduzir os lemas da teoria e a fragmentação proposicional para axiomas e teoremas Lean, utilizando as táticas grind (para lemas de teoria) e bv_decide (para a parte proposicional).

3. Contribuições Chave

1. Primeiro Solucionador SMT Completo Gerado por IA: Demonstração de que um agente de LLM pode construir um solucionador DPLL(T) funcional do zero, sem código humano, cobrindo parsing, resolução SAT, fechamento de congruência e geração de provas.
2. Técnica de Pré-processamento Automatizada: O agente descobriu e implementou autonomamente uma técnica para resolver problemas de "diamante equacional" (que causam comportamento exponencial em solucionadores lazy), calculando interseções de fechamentos de igualdade entre ramos de disjunções.
3. Integração com Lean para Provas: Implementação de um mecanismo que emite provas formais em Lean para instâncias insatisfiáveis, validando a lógica interna do solucionador.
4. Metodologia de Desenvolvimento Assistido por IA: O artigo estabelece um roteiro prático para pesquisadores que desejam usar LLMs para desenvolver ferramentas de raciocínio, enfatizando a necessidade de:
   • Especificação rigorosa de linguagens de entrada.
   • Limites explícitos de recursos (timeouts).
   • Uso intensivo de fuzzing e testes diferenciais.
   • Fornecimento de exemplos concretos de falhas para correção.

4. Resultados

O solucionador foi avaliado em benchmarks QF_UF do SMT-LIB e comparado com solucionadores maduros (z3 e cvc5):

• Desempenho: O solucionador llm2smt resolveu 7.468 instâncias de um total de benchmarks, ficando próximo do z3 (7.500) e do cvc5 (7.494).
• Velocidade: Em termos de "vitórias" (tempo não pior que o melhor em 1s), o llm2smt obteve 6.486 vitórias, superado apenas pelo z3 (7.491).
• Análise de Componentes:
  • A versão sem pré-processamento (llm2smt-no-prepro) resolveu menos instâncias (7.355), confirmando a eficácia do pré-processamento desenvolvido pelo agente.
  • Curiosamente, a versão sem propagação de teoria (llm2smt-no-th-prop) foi ligeiramente mais rápida em alguns casos, sugerindo que a propagação introduz overhead desnecessário para certos benchmarks, embora seja crucial para outros.
• Certificação: A geração de provas em Lean foi desafiadora. Embora muitas tentativas tenham falhado devido a limites de recursos do Lean (estouro de pilha, tempo limite), nenhuma prova errônea foi encontrada. Isso indica que, quando o agente consegue gerar uma prova, ela é correta, mas a taxa de sucesso ainda é baixa devido à complexidade da interação com o verificador de provas.

5. Significado e Conclusão

O artigo responde com um "sim qualificado" à pergunta se LLMs podem desenvolver ferramentas de raciocínio automatizado.

• Viabilidade: Um agente de codificação pode criar um solucionador SMT competitivo, capaz de implementar algoritmos descritos em artigos científicos e depurar seu próprio código quando confrontado com exemplos de falha concretos.
• Limitações e Riscos: A correção não pode ser assumida. O agente comete erros sutis (como tratar booleanos como termos e proposições simultaneamente) que requerem ferramentas de fuzzing para serem detectados. A geração de provas formais permanece a tarefa mais difícil, exigindo orientação humana significativa sobre as expectativas do verificador (Lean).
• Futuro: O trabalho sugere que o futuro do desenvolvimento de ferramentas de IA reside em uma análise mais cuidadosa do código gerado e no uso de scaffolding (andaimes) robustos, como testes sistemáticos e especificações rigorosas, para mitigar a "inteligência irregular" dos modelos atuais.

Em suma, o estudo é um marco na demonstração de que LLMs podem atuar como engenheiros de software autônomos em domínios de alta complexidade lógica, desde que supervisionados por um fluxo de trabalho rigoroso de validação.