💻 computer science

Can LLMs Perform Synthesis?

O estudo compara ferramentas simbólicas de ponta com modelos de linguagem (Qwen e GPT-5) em diversas tarefas de síntese de programas e conclui que as ferramentas simbólicas superam ou empatam com os LLMs tanto em taxa de sucesso quanto em tempo de execução, mesmo rodando em hardware menos potente.

Autores originais: Derek Egolf, Yuhao Zhou, Stavros Tripakis

Publicado 2026-03-24

📖 5 min de leitura🧠 Leitura aprofundada

CC BY 4.0

Autores originais: Derek Egolf, Yuhao Zhou, Stavros Tripakis

Artigo original sob licença CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta é uma explicação gerada por IA do artigo abaixo. Não foi escrita nem endossada pelos autores. Para precisão técnica, consulte o artigo original. Ler aviso legal completo

Imagine que você tem um problema muito difícil de resolver, como montar um quebra-cabeça complexo ou escrever um código de computador perfeito. Existem duas formas principais de tentar resolver isso:

O "Mestre da Lógica" (Ferramentas Simbólicas): É como um matemático super focado que usa regras estritas, lógica pura e força bruta para testar cada peça possível até encontrar a solução correta. Ele é lento em alguns casos, mas nunca erra a lógica.
O "Gênio Criativo" (LLMs - Modelos de Linguagem): É como um escritor ou programador muito talentoso que "adivinha" a solução baseada em tudo o que já leu. Ele é rápido e criativo, mas às vezes alucina, inventa regras que não existem ou esquece detalhes importantes.

Este artigo da Universidade Northeastern (Egolf, Zhou e Tripakis) é como uma corrida de obstáculos entre esses dois tipos de "inteligência" para ver quem é melhor em Síntese de Programas.

O que é "Síntese de Programas"?

Pense na síntese como pedir para alguém: "Aqui está a regra do jogo (o que o programa deve fazer), agora escreva o código que faz exatamente isso." O objetivo é que o computador gere o programa sozinho, garantindo que ele funcione perfeitamente.

A Grande Pergunta

Os autores queriam saber: Os novos "Gigantes da IA" (como o GPT-5 e o Qwen) conseguem fazer o trabalho dos "Mestres da Lógica" tradicionais?

Eles testaram isso em quatro cenários diferentes, como se fossem quatro tipos de desafios:

Reações em Tempo Real: Criar um sistema que reage a eventos do mundo (como um semáforo inteligente).
Síntese Guiada por Sintaxe: Criar código que segue regras gramaticais muito específicas.
Protocolos Distribuídos: Escrever regras para computadores que conversam entre si (como um banco de dados em vários servidores).
Funções Recursivas: Criar funções que se chamam repetidamente (como calcular uma sequência de números).

O Experimento (A Corrida)

Eles colocaram os dois competidores na pista:

O Competidor Tradicional: Ferramentas de software especializadas (como ltlsynt, cvc5, PolySemist). Elas são como calculadoras de alta precisão.
O Competidor IA:
- Qwen: Um modelo de código de código aberto (gratuito) com 32 bilhões de "neurônios".
- GPT-5: O modelo mais avançado e proprietário da OpenAI (o "chefe" da IA atual).

A Regra do Jogo:
Para ser justo, eles deram um limite de tempo (10 ou 15 minutos) para cada um resolver os problemas.

A IA não recebe ajuda externa. Ela tenta, o sistema verifica se está certo. Se estiver errado, a IA tenta de novo (no caso do Qwen) ou o sistema para (no caso do GPT-5, que só tenta uma vez por problema para economizar recursos).
Se a IA gerar um código que não funciona, ela é penalizada.

O Veredito: Quem Ganhou?

Aqui estão as descobertas principais, traduzidas para o dia a dia:

1. O "Mestre da Lógica" ainda é o campeão em quantidade

Em quase todos os testes, as ferramentas tradicionais resolveram mais problemas do que a IA.

Analogia: Imagine que você precisa encontrar uma agulha em um palheiro. O "Mestre da Lógica" vai virar cada palha, uma por uma, até achar. A IA pode chutar onde a agulha está e acertar rápido, mas se ela errar o chute, ela pode ficar perdida. Em problemas muito complexos, a IA se perde mais vezes.

2. A IA é mais rápida? Nem sempre!

Você pode pensar: "A IA é super rápida, deve ganhar em tempo!"

A Surpresa: As ferramentas tradicionais foram muito mais rápidas que a IA em quase todos os casos.
Por que? A IA precisa "pensar" (gerar texto) e, se errar, precisa tentar de novo. As ferramentas tradicionais usam algoritmos matemáticos que eliminam caminhos errados instantaneamente. É como comparar um carro de Fórmula 1 (IA) que fica atolando no trânsito e voltando para a largada, com um trem de alta velocidade (Ferramenta Tradicional) que segue trilhos diretos. Mesmo que a IA tenha um motor mais potente (hardware melhor), ela perde tempo tentando adivinhar.

3. O GPT-5 é impressionante, mas não perfeito

O GPT-5 foi o melhor dos dois IAs. Em alguns cenários (como protocolos distribuídos), ele quase empatou com as ferramentas tradicionais.

O problema: Mesmo o GPT-5 cometeu erros de "gramática" (escreveu código que parecia certo, mas tinha um ponto e vírgula faltando ou uma lógica errada). As ferramentas tradicionais nunca cometem erros de sintaxe; elas só geram código que é matematicamente válido.

4. A IA repete os mesmos erros

O estudo mostrou que o modelo Qwen, quando falha, tende a gerar a mesma solução errada várias vezes seguidas.

Analogia: É como se você estivesse tentando abrir uma porta e, em vez de tentar outra fechadura, você continuasse batendo na mesma fechadura emperrada 100 vezes. As ferramentas tradicionais, ao contrário, nunca tentam a mesma solução duas vezes; elas são eficientes.

Conclusão Simples

A IA (LLMs) consegue fazer síntese de programas?
Sim, ela consegue! E em alguns casos, ela até resolve problemas que as ferramentas tradicionais não conseguem. Ela é ótima para ideias criativas e para tarefas onde as regras são flexíveis.

Mas ela substitui as ferramentas tradicionais?
Ainda não. Para tarefas que exigem precisão absoluta, lógica complexa e garantia de que "nada vai dar errado", as ferramentas tradicionais ainda são superiores. Elas são mais rápidas, mais consistentes e não se cansam de tentar.

A Lição Final:
O futuro não é escolher entre um ou outro. A melhor estratégia é usar um time misto:

Use a IA para gerar ideias rápidas e rascunhos criativos.
Use as Ferramentas Tradicionais para verificar, refinar e garantir que o código final é matematicamente perfeito.

É como ter um arquiteto genial (IA) desenhando a casa, mas precisando de um engenheiro estrutural (Ferramenta Tradicional) para garantir que o prédio não vai cair.

Resumo Técnico: Can LLMs Perform Synthesis?

1. Problema e Motivação

O objetivo da síntese de programas é gerar automaticamente sistemas que sejam "corretos por construção", garantindo que satisfaçam uma especificação formal. Historicamente, isso é feito por ferramentas simbólicas (baseadas em lógica e busca exaustiva). Com o avanço dos Grandes Modelos de Linguagem (LLMs) na geração de código, surge a pergunta central: Os LLMs são capazes de realizar síntese de programas a partir de especificações formais, comparáveis às ferramentas simbólicas de ponta?

O artigo investiga essa questão comparando ferramentas simbólicas de última geração com LLMs (Qwen-2.5-Coder-32B e GPT-5) em quatro domínios distintos de síntese.

2. Metodologia

Os autores adotaram uma abordagem pragmática e orientada ao usuário, focando em LLMs "prontos para uso" (sem fine-tuning, RAG ou técnicas neurosimbólicas avançadas), mas acoplados a verificadores simbólicos para garantir correção.

Domínios de Estudo:
1. Síntese Reativa LTL: Síntese de Máquinas de Estado Finito (FSM) a partir de especificações em Lógica Temporal Linear (LTL).
2. Síntese Guiada por Sintaxe (SyGuS): Síntese de programas que obedecem a uma gramática e satisfazem uma especificação.
3. Síntese de Protocolos Distribuídos (TLA+): Completar "esboços" (sketches) de protocolos distribuídos para satisfazer propriedades.
4. Síntese de Programas Recursivos (ACL2s): Completar esboços de funções recursivas em Lisp-like para satisfazer propriedades de lógica de primeira ordem.
Ferramentas Comparadas:
- Simbólicas: ltlsynt (LTL), cvc5 (SyGuS), PolySemist (TLA+), Cataclyst (ACL2s).
- LLMs:
  - Qwen-2.5-Coder-32B: Modelo de código open-source (32B parâmetros), executado localmente em GPU NVIDIA H200.
  - GPT-5: Modelo proprietário de ponta, executado via API.
Protocolo Experimental (ILST):
- Qwen: Utiliza um loop de "tentativa e erro" (Iterate-LLM-until-solution-or-timeout). O LLM gera uma solução, um verificador simbólico a valida. Se falhar, o LLM é consultado novamente (sem feedback de contraexemplos, apenas repetição do prompt) até encontrar uma solução válida ou esgotar o tempo limite (10 ou 15 minutos).
- GPT-5: Consultado apenas uma vez por benchmark para garantir justiça na comparação de recursos computacionais (já que o GPT-5 roda em hardware proprietário muito mais potente).
- Verificação: Todas as saídas dos LLMs são verificadas por ferramentas simbólicas (ex: nuXmv, Z3, TLC) para garantir correção formal.

3. Resultados Principais

Os resultados variam por domínio, mas apresentam tendências claras:

Desempenho em Benchmarks Resolvidos:
- Domínio LTL: As ferramentas simbólicas (ltlsynt) superaram amplamente ambos os LLMs, resolvendo significativamente mais benchmarks. O GPT-5 foi ligeiramente melhor que o Qwen, mas ambos ficaram muito atrás do simbólico.
- Domínios SyGuS, TLA+ e ACL2s: O GPT-5 teve desempenho comparável ou até superior às ferramentas simbólicas em alguns casos (ex: SyGuS, onde o GPT-5 resolveu mais que o cvc5). O Qwen geralmente ficou atrás das ferramentas simbólicas, exceto em alguns casos específicos onde encontrou soluções que o simbólico não encontrou (e vice-versa).
- Conclusão Geral: As ferramentas simbólicas resolvem mais benchmarks que o Qwen em todos os domínios. O GPT-5 compete de perto ou supera as ferramentas simbólicas em três dos quatro domínios, mas perde no domínio LTL.
Tempo de Execução:
- As ferramentas simbólicas foram significativamente mais rápidas que o GPT-5 em todos os domínios (diferenças de uma a duas ordens de grandeza), apesar de o GPT-5 rodar em hardware muito mais potente.
- O Qwen, apesar de rodar em GPU, muitas vezes demorou mais que as ferramentas simbólicas devido à necessidade de múltiplas iterações para encontrar uma solução válida.
Qualidade e Falhas:
- Erros Sintáticos: O Qwen frequentemente falhou devido a erros de sintaxe (código mal formado, violação de gramática), enquanto o GPT-5 foi muito mais robusto em seguir restrições sintáticas.
- Repetição: O Qwen tendeu a gerar repetidamente as mesmas soluções incorretas durante o loop de iteração, desperdiçando tempo. As ferramentas simbólicas, por natureza enumerativa, não repetem candidatos.
- Custo: O uso do GPT-5 teve um custo monetário variável (de ~ $0.80 a ~$ 44 USD dependendo do domínio), enquanto o Qwen teve custo de hardware local.

4. Contribuições Chave

Avaliação Justa e Rigorosa: O estudo fornece uma das primeiras comparações diretas e controladas entre LLMs de ponta e ferramentas de síntese simbólica, utilizando benchmarks padrão da comunidade (SYNTCOMP, SyGuS-COMP, etc.).
Metodologia de Verificação Híbrida (Leve): Demonstra como acoplar LLMs a verificadores simbólicos sem depender de fine-tuning complexo, focando na capacidade do LLM "puro" de gerar código correto.
Análise de Domínios Específicos: Mostra que a eficácia dos LLMs na síntese depende fortemente do domínio. Eles são fortes em tarefas de preenchimento de esboços (SyGuS, TLA+) onde a estrutura é mais flexível, mas fracos em síntese reativa pura (LTL) que exige raciocínio lógico profundo e garantias de correção por construção.
Recomendação de Abordagem de Portfólio: Os resultados sugerem que a melhor estratégia prática não é escolher entre LLM ou Símbólico, mas usar uma abordagem de portfólio, rodando ambas as ferramentas em paralelo para maximizar a cobertura de benchmarks resolvidos.

5. Significância e Conclusão

O artigo conclui que, embora os LLMs (especialmente o GPT-5) tenham demonstrado capacidades impressionantes na síntese de programas, eles ainda não substituem as ferramentas simbólicas em termos de confiabilidade, velocidade e cobertura total de problemas complexos.

Pontos Fortes dos LLMs: Capacidade de encontrar soluções em domínios onde as ferramentas simbólicas podem falhar (devido a limitações de busca ou heurísticas) e habilidade de gerar código sintaticamente correto em domínios menos restritivos.
Pontos Fortes das Ferramentas Simbólicas: Garantia de correção, velocidade superior, ausência de erros sintáticos e capacidade de resolver problemas que exigem raciocínio lógico profundo (como LTL).

O trabalho sugere que o futuro da síntese de programas provavelmente residirá em sistemas híbridos, onde LLMs podem ser usados para guiar buscas simbólicas ou gerar candidatos iniciais, enquanto ferramentas simbólicas garantem a correção e eficiência. No entanto, como ferramentas autônomas "caixa-preta" para síntese formal, os LLMs atuais ainda têm limitações significativas.