← Últimos artigos
🤖 AI

Can LLMs Build a MaxSAT Solver from Papers? The CoreForge Experience

O artigo relata sobre o CoreForge, um experimento demonstrando que grandes modelos de linguagem podem auxiliar com sucesso na construção de um resolvedor funcional de MaxSAT não ponderado diretamente a partir de artigos de pesquisa por meio de um fluxo de trabalho iterativo, embora o sistema resultante ainda exija orientação e validação humana, enquanto fica atrás de resolvedores projetados manualmente em termos de desempenho.

Autores originais: Ruben Martins

Publicado 2026-07-17
📖 5 min de leitura🧠 Leitura aprofundada

Autores originais: Ruben Martins

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ê é um detetive tentando resolver um nó enorme e emaranhado de pistas. No mundo da ciência da computação, esse nó é chamado de "problema de restrição". Você tem uma lista de regras (como "a bola vermelha deve estar à esquerda" ou "a bola azul não pode estar ao lado da verde") e o seu trabalho é encontrar uma maneira de organizar tudo para que todas as regras fiquem satisfeitas. Às vezes, é impossível deixar todo mundo feliz, então o objetivo muda para encontrar a organização que deixe o maior número de pessoas felizes. Este é o trabalho de um "solver MaxSAT" — um programa de computador superinteligente que atua como um mestre solucionador de quebra-cabeças, encontrando a melhor solução possível quando uma solução perfeita não existe.

Durante décadas, construir esses solucionadores de quebra-cabeças foi um trabalho para especialistas humanos. Eles precisam ler artigos de pesquisa complexos, entender teorias matemáticas profundas e, depois, passar anos escrevendo milhões de linhas de código, ajustando detalhes minúsculos para tornar o solver rápido o suficiente para ser útil. Mas recentemente, um novo tipo de assistente digital chegou: os Modelos de Linguagem de Grande Escala (LLMs). Estes são os cérebros de IA por trás de ferramentas como o ChatGPT, capazes de escrever histórias, poemas e até código de computador. A grande questão é: pode um IA ler um artigo de pesquisa e construir um solucionador de quebra-cabeças funcional do zero, sem que um humano escreva uma única linha de código? Este é o mistério que o projeto "CoreForge" se propõe a resolver.


O Experimento CoreForge: Ensinando a IA a Construir um Solucionador de Quebra-Cabeças

Em um projeto chamado CoreForge, um pesquisador chamado Ruben Martins, da Carnegie Mellon University, decidiu testar os limites da IA. Em vez de pedir a uma IA para consertar um solucionador de quebra-cabeças quebrado que já existia, ele a desafiou a construir um do zero, usando apenas artigos de pesquisa como seu manual de instruções. Pense nisso como entregar a um robô uma pilha de livros de receitas escritos por chefs famosos e pedir para ele construir uma cozinha de restaurante e cozinhar uma refeição de cinco estrelas, sem nunca ter visto um fogão antes.

O processo não foi um truque de mágica de "um único passo" onde a IA simplesmente cuspiu um programa perfeito. Em vez disso, foi uma longa dança iterativa entre humano e máquina. O pesquisador humano escolhia um artigo de pesquisa, discutia as ideias principais com a IA e, em seguida, pedia à IA (especificamente a uma ferramenta de codificação chamada Codex) para escrever o código. Mas a IA não tinha passe livre. O humano então executava testes, verificava erros e pedia à IA para corrigir seus erros. Eles repetiam esse ciclo repetidamente, como um aluno e um tutor trabalhando em um problema matemático difícil, até terem um solver funcional.

O Que Eles Construíram?
O resultado foi uma base de código massiva de mais de 25.000 linhas de código C++. A IA traduziu com sucesso ideias matemáticas complexas de artigos em software funcional. Ela implementou várias estratégias avançadas, incluindo:

  • Otimização guiada por núcleo (Core-guided optimization): Um método onde o solver aprende com seus erros (chamados de "núcleos") para evitar repeti-los.
  • Pré-processamento (Preprocessing): Limpar o quebra-cabeças antes de tentar resolvê-lo para torná-lo mais fácil.
  • Lookahead: Um novo recurso que a IA ajudou a inventar, onde o solver faz algumas "rodadas de prática" rápidas para adivinhar a melhor estratégia antes de se comprometer com a solução real.

Funcionou?
A parte mais surpreendente da história é que a IA não trapaceou. Os pesquisadores realizaram milhares de testes, incluindo "fuzzing" (jogar dados aleatórios e caóticos no solver para ver se ele quebra) e comparando-o com benchmarks oficiais de competições. Eles encontraram zero respostas erradas nas configurações testadas. O solver era matematicamente correto. Ele não apenas adivinhava; ele realmente resolvia os quebra-cabeças corretamente.

Mas É Rápido o Suficiente?
Aqui está o detalhe. Embora a IA tenha construído um solver correto, ela não construiu o mais rápido. Quando comparado aos melhores solvers projetados por humanos, que foram refinados ao longo de anos, o CoreForge foi mais lento e resolveu menos quebra-cabeças. É como se a IA tivesse construído um carro que dirige perfeitamente e nunca bate, mas que só atinge 60 km/h quando os melhores carros feitos por humanos estão a 200 km/h.

Os pesquisadores descobriram que a IA era ótima em entender as ideias de alto nível e transformá-las em código. No entanto, ela teve dificuldades com os detalhes de "ajuste fino" — as otimizações pequenas e agressivas que tornam um solver extremamente rápido. A IA também às vezes adicionava etapas extras que a atrasavam, como fazer um desvio quando uma estrada reta seria melhor.

O Veredito
A experiência do CoreForge sugere que a IA certamente pode ajudar a construir softwares complexos a partir de artigos de pesquisa, mas ainda não está pronta para substituir engenheiros humanos. A IA precisa de um guia humano para verificar seu trabalho, decidir quais ideias manter e ajudá-la a evitar ficar presa em loops lentos.

O artigo conclui que, embora não tenhamos chegado ao ponto de uma IA construir autonomamente um solver de classe mundial, estamos chegando perto. A IA provou que pode ler os "livros de receitas" e construir a "cozinha". O próximo passo é ensinar a ela como ser um mestre chef que sabe exatamente como ajustar o calor e o tempo para vencer a competição. Por enquanto, os melhores resultados vêm de uma equipe: um humano fornecendo a estratégia e a IA fazendo o trabalho pesado de escrever o código.

Afogado em artigos na sua área?

Receba digests diários dos artigos mais recentes que correspondam às suas palavras-chave de pesquisa — com resumos técnicos, no seu idioma.

Experimentar Digest →