🤖 machine learning

Solver-Hard Is Not Model-Hard: A Hardness-Controlled Diagnostic for LLM Constraint Reasoning

Este artigo demonstra que o desempenho de grandes modelos de linguagem em tarefas de raciocínio de restrição não é determinado pela dificuldade de resolução subjacente das instâncias do problema, conforme evidenciado pela falta de correlação entre proxies de dureza de prova e a precisão do modelo ou o gasto de tokens através de benchmarks cuidadosamente controlados e de densidade correspondente.

Autores originais: Lucky Verma

Publicado 2026-07-21

📖 5 min de leitura🧠 Leitura aprofundada

CC BY 4.0

Autores originais: Lucky Verma

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ê está tentando ensinar um robô superinteligente a resolver quebra-cabeças de lógica. No mundo da ciência da computação, existe um tipo famoso de quebra-cabeça chamado "SAT" (Satisfatibilidade), que é basicamente perguntar: "Consigo preencher estes espaços em branco com 'Verdadeiro' ou 'Falso' para que cada uma das regras desta lista gigante seja satisfeita?" Por décadas, cientistas notaram algo estranho: quando esses quebra-cabeças ficam apenas na medida certa de complicados — nem muito fáceis, nem impossivelmente difíceis — tanto humanos quanto computadores tendem a bater em um muro. É como um engarrafamento no cérebro.

Para entender o porquê, os pesquisadores geralmente olham para duas coisas. Primeiro, há a densidade, que é apenas uma palavra chique para "o quão crowded (lotadas) as regras estão". Se você tem muitas regras compactadas em um espaço pequeno, parece mais difícil. Segundo, há a dureza estrutural, que é sobre a forma oculta do quebra-cabeça. Alguns quebra-cabeças parecem simples, mas possuem uma estrutura torcida e emaranhada que os torna impossíveis de desvendar rapidamente, enquanto outros parecem bagunçados, mas têm um caminho reto e fácil através deles. A grande questão é: quando os modelos de IA falham, é porque o quebra-cabeça está muito lotado (densidade) ou porque a forma oculta do quebra-cabeça é muito complicada (estrutura)?

Este artigo é como uma história de detetive onde o autor monta uma armadilha muito específica para pegar a IA em flagrante. O pesquisador, Lucky Verma, queria ver se os modelos de IA realmente entendem a "forma torcida" de um quebra-cabeça de lógica, ou se eles estão apenas adivinhando com base em quão "lotadas" as regras parecem. Para fazer isso, ele criou dois tipos de quebra-cabeças que parecem quase idênticos na superfície — eles têm o mesmo número de regras e a mesma "densidade" — mas são secretamente muito diferentes por baixo. Um tipo é um quebra-cabeça "Escada" (Ladder), que é fácil de resolver porque tem uma estrutura simples e reta. O outro é um quebra-cabeça "Expansor" (Expander), que é um pesadelo para computadores tradicionais porque sua estrutura é tão emaranhada que resolvê-la exige um esforço exponencial (pense nisso como tentar desvendar um novelo de lã que fica maior à medida que você puxa).

O experimento foi um confronto entre um resolvedor de computador clássico (uma ferramenta chamada Glucose) e vários modelos de IA de grande escala (como Llama 3.3, Llama 4 e Mistral 3). Primeiro, eles testaram o resolvedor clássico. Como esperado, o resolvedor teve dificuldades massivas com os quebra-cabeças "Expansor", levando até 51 vezes mais esforço (medido em "conflitos", ou momentos em que o resolvedor atinge um beco sem saída) para resolvê-los em comparação aos quebra-cabeças "Escada". O resolvedor claramente sabia a diferença entre a forma fácil e a forma difícil.

Então veio a IA. Se a IA estivesse realmente raccinando como um especialista em lógica, ela deveria ter achado os quebra-cabeças "Escada" mais fáceis e os "Expansor" mais difíceis, assim como o resolvedor clássico. Mas aqui está a reviravolta: os modelos de IA não se importaram com a forma de jeito nenhum. Na verdade, o desempenho deles estava totalmente disperso. Para um modelo, os quebra-cabeças "Escada" eram mais fáceis; para outro, os "Expansor" eram mais fáceis; e quando calculamos a média de todos eles, a diferença era praticamente zero (uma lacuna minúscula de +1.7 pontos que não era estatisticamente significativa). Os modelos de IA pareciam estar ignorando a estrutura oculta completamente.

Ainda mais estranho, os pesquisadores verificaram quanto "tempo de pensamento" (medido em tokens, ou palavras geradas) a IA gastava nesses quebra-cabeças. Você esperaria que a IA gastasse mais tempo nos quebra-cabeças "Expansor" difíceis. Em vez disso, a IA frequentemente gastava mais tempo nos quebra-cabeças "Escada" ou ficava presa nos quebra-cabeças mais fáceis de todos, desperdiçando seu orçamento sem resolvê-los de fato. O artigo também testou se a IA estava apenas memorizando a aparência do quebra-cabeça ao embaralhar as letras (um "relabeling preservador de prova"). O desempenho de um modelo despencou quase 93 pontos quando o quebra-cabeça foi apenas rearranjado, provando que ele estava contando com truques superficiais em vez de lógica real.

A conclusão é que, para esses quebra-cabeças específicos, "Dificuldade do Solver não é Dificuldade do Modelo" (Solver-Hard is Not Model-Hard). Só porque um quebra-cabeça é matematicamente difícil para um computador tradicional, não significa que seja difícil para uma IA, e vice-versa. A IA não está falhando porque o quebra-cabeça é muito difícil; ela está falhando porque não está realmente rastreando a estrutura lógica da maneira que esperávamos. É como se a IA estivesse olhando para o quebra-cabeça e dizendo: "Isso parece lotado, então deve ser difícil", ou "Isso parece um padrão que eu já vi antes", sem nunca realizar o trabalho estrutural profundo necessário para resolvê-lo. O estudo sugere que não podemos assumir que os modelos de IA estão ficando melhores em raciocínio apenas porque estão ficando maiores; às vezes, eles estão apenas ficando melhores em adivinhar com base em pistas superficiais.

Resumo Técnico: Solver-Hard Is Not Model-Hard (Difícil para o Solver não é Difícil para o Modelo)

Definição do Problema
As avaliações atuais de Grandes Modelos de Linguagem (LLMs) em problemas de satisfatibilidade booleana (SAT) e satisfação de restrições frequentemente confundem duas propriedades distintas: densidade de cláusulas (a razão entre cláusulas e variáveis, $\alpha = m/n$ ) e complexidade de prova (a dificuldade estrutural de refutar uma instância insatisfatível). Em fórmulas aleatórias uniformes, essas propriedades co-variam próximo à transição de fase de satisfatibilidade, tornando impossível determinar se as falhas dos modelos são impulsionadas por pistas de densidade de superfície ou pela dificuldade algorítmica subjacente da instância. Esse fator de confusão obscurece se os LLMs rastreiam custos de busca ao nível da instância ou se apenas reproduzem curvas de falha qualitativas associadas a limiares de densidade.

Metodologia
Os autores propõem um diagnóstico de validade de construto que desacopla a densidade de cláusulas da complexidade de prova usando dissociações controladas. O design experimental baseia-se em três contrastes principais:

C1 (Contraste Principal): Comparar fórmulas de Tseitin em duas estruturas de grafos com densidade de cláusulas quase idêntica ( $\alpha \approx 2,67$ $α \approx 2, 67$ ) e largura máxima de cláusula (3), mas com diferença na dificuldade de resolução:
- Grafos Expansores: Expansores 3-regulares que exigem resolução exponencial (difíceis de prova).
- Grafos Ladder (Escada): Grafos com treewidth dois, que admitem provas polinomiais (fáceis de prova).
C2 (Controle de Densidade): Comparar as fórmulas de Tseitin Expansoras de baixa densidade contra fórmulas aleatórias UNSAT de alta densidade ( $\alpha \approx 6$ ). Estas últimas são estruturalmente fáceis para solvers de Aprendizado de Cláusulas Baseado em Conflito (CDCL), apesar de sua alta densidade.
C3 (Âncora de Pigeonhole): Usar fórmulas de Princípio do Pombal (PHP) como uma segunda âncora de dificuldade de prova sem estrutura de grafo, contrastando-as com o UNSAT aleatório.

Validação do Solver:
Antes de avaliar os LLMs, os autores verificaram a dissociação usando o solver CDCL Glucose (e outros cinco). Eles mediram a contagem de conflitos como um proxy específico do solver para o custo de refutação. A construção separou com sucesso os custos do solver: em tamanhos equivalentes, a mediana da razão de conflitos entre as fórmulas Expansoras e Ladder cresceu monotonicamente, atingindo até 51× nos maiores bins. As fórmulas UNSAT aleatórias de alta densidade permaneceram as mais fáceis para o solver, confirmando que a densidade e o custo do solver são desacoplados nesta construção.

Protocolo de Avaliação de LLM:

Modelos: Avaliados Llama 3.3 70B, Llama 4 Maverick 17B e Mistral Large 3 675B (todos transformadores autorregressivos) com temperatura zero. Um quarto modelo (gpt-oss-120b) foi excluído devido à alta taxa de abstenção.
Tarefa: Os modelos foram solicitados a fornecer um veredito binário SAT/UNSAT para 243 instâncias por modelo (60 de cada família grande, 3 âncoras PHP).
Métricas: Precisão do veredito (com abstenções pontuadas como incorretas), lacunas de precisão entre famílias de prova-difíceis e prova-fáceis, e a correlação entre corretude e contagens de conflito do solver.
Análise de Gasto de Tokens: Uma extensão pré-registrada analisou se os tokens de conclusão reportados pelo provedor (um proxy para o computo de tempo de teste) rastreavam o proxy de custo do solver, controlando o comprimento da fórmula e o censuramento.

Resultados Principais

Falha de Transferência: A ordenação de dificuldade observada em solvers clássicos não se transferiu para os LLMs.
- Lacunas de Precisão: A lacuna de precisão prevista (Ladder > Expander) foi inconsistente. O Llama 3.3 mostrou um gap de +20 pontos (na direção prevista), o Llama 4 mostrou um gap de -32 pontos (invertido) e o Mistral 3 mostrou +17 pontos. O gap agrupado foi de +1,7 pontos ( $p=0,74$ ), falhando em atingir o limiar pré-especificado para um efeito de transferência significativo.
- Correlação: Não houve associação negativa entre as contagens de conflito do solver e a corretude do modelo. Em vez disso, a correlação agrupada foi fracamente positiva ( $r = +0,15$ ), indicando que custos de solver mais altos não previram menor precisão do modelo.
- Densidade vs. Dificuldade: Os modelos tiveram o pior desempenho nas fórmulas UNSAT aleatórias de alta densidade (que foram as mais fáceis para o solver), demonstrando ainda mais que nem a densidade de cláusulas nem a complexidade de prova ordenam consistentemente os erros dos modelos.
Sensibilidade de Superfície: Um experimento de rotulagem preservadora de prova (embaralhamento de variáveis e cláusulas sem alterar a estrutura lógica) revelou sensibilidade de superfície específica do modelo. Para o Llama 3.3, a precisão caiu em uma média de 93 pontos em todos os clusters após a rotulagem, enquanto o Llama 4 permaneceu amplamente inafetado. Isso sugere que os modelos podem depender de formas superficiais em vez de estrutura lógica.
Dissociação de Gasto de Tokens: O gasto de tokens de conclusão observado não aumentou consistentemente com o custo do solver.
- Com orçamentos de 16k tokens, o modelo de raciocínio (Nemotron) gastou mais tokens nas fórmulas Ladder (prova-fácil) do que nas fórmulas Expander (prova-difícil).
- O consumo de tokens mais severo (atingindo o limite de 16k) ocorreu na família mais fácil para o solver (UNSAT aleatório), onde a precisão era próxima de zero.
- As correlações de comprimento controlado entre tokens e conflitos do solver foram geralmente negativas ou nulas, falhando em mostrar que os modelos alocam mais computo para instâncias estruturalmente mais difíceis.

Significância e Alegações
O artigo conclui que "Solver-Hard Is Not Model-Hard" dentro do regime testado. A principal contribuição é um diagnóstico delimitado mostrando que a dificuldade de instância clássica (definida por complexidade de prova e validada por solvers CDCL) não prevê a precisão do veredito do LLM ou a alocação de tokens quando a densidade de cláusulas é controlada.

Validade de Construto: O estudo demonstra que avaliações anteriores que dependem de fórmulas aleatórias próximas à transição de fase podem estar medindo a sensibilidade a pistas de densidade em vez da capacidade de raciocínio.
Limitações: Os autores declaram explicitamente que estes resultados não constituem uma teoria universal de falha de raciocínio ou um resultado de impossibilidade para arquiteturas autorregressivas. Os achados são limitados ao escalonamento específico (12–30 variáveis), às famílias específicas de fórmulas utilizadas e aos modelos testados.
Implicação: Alegações de que os LLMs falham devido à complexidade de prova devem primeiro demonstrar que a ordenação de dificuldade transfere-se sob dissociações controladas. A evidência atual sugere que, para estes modelos, nem a densidade de cláusulas nem a complexidade de prova são preditores confiáveis de desempenho, e que os modelos podem ser altamente sensíveis a variações superficiais na serialização das fórmulas.

Mais como este