Resumo Técnico: Menos é Mais – Carga Cognitiva e o Teto de Prompt Único no Raciocínio Matemático de LLMs

1. Problema e Contexto

O artigo investiga o desempenho de Grandes Modelos de Linguagem (LLMs) em raciocínio matemático formal, especificamente no contexto da Competição SAIR Equational Theories Stage 1.

• A Tarefa: Decidir se uma lei equacional ($E_1$) implica universalmente em outra lei ($E_2$) sobre todos os magmas (estruturas algébricas com uma única operação binária, sem axiomas como associatividade ou comutatividade).
• Assimetria Computacional: O problema é computacionalmente assimétrico:
  • Falso: Pode ser certificado exibindo um único contraexemplo finito (decidível via busca de modelos finitos).
  • Verdadeiro: Requer provar que nenhum contraexemplo existe em qualquer magma (incluindo infinitos), o que é indecidível em geral e exige quantificação universal.
• O Desafio: Os LLMs devem aproximar ambas as tarefas (prova universal e busca de contraexemplo) em uma única geração, sem ferramentas simbólicas externas. O estudo questiona até que ponto a engenharia de prompts pode superar a falta de raciocínio matemático interno do modelo.

2. Metodologia

Os autores conduziram um estudo empírico sistemático ao longo de cinco semanas, testando mais de 40 variantes de prompts em três modelos de linguagem diferentes.

• Modelos Avaliados:
  • gpt-oss-120b (120B parâmetros, MoE, foco principal).
  • Llama 3.3 70B.
  • Gemma 4 31B.
• Dados: Utilizaram quatro divisões de dados (splits): normal (balanceado), hard1 (focado em Falso), hard2 (balanceado, complexo) e hard3 (principalmente balanceado, usado para avaliação principal).
• Design de Prompts: As variantes variaram de 0 a 4.878 bytes e foram testadas em dimensões como:
  • Conteúdo de tabelas de contraexemplos (CE).
  • Regras de "forçamento de singleton" (heurísticas para detectar Verdadeiro).
  • Regras de "bloco" (classificadores condicionais para Falso).
  • Ordenação: A ordem em que as instruções aparecem (ex: verificar magma trivial antes ou depois da tabela de contraexemplos).
• Métricas: Acurácia, Recall de Verdadeiro (True recall) e Recall de Falso (False recall).

3. Contribuições Principais

A. O "Teto de Prompt Único" (Single-Prompt Ceiling)

Os autores identificam uma região de saturação empírica: um limite onde melhorias adicionais na complexidade do prompt não resultam em ganhos generalizáveis.

• Para o modelo gpt-oss-120b, a acurácia em problemas difíceis e balanceados estagna entre 71% e 79%, independentemente do tamanho do prompt.
• Prompts mais longos e complexos tendem a degradar o desempenho em modelos menores (como Llama 70B), causando colapso no recall de Verdadeiro.

B. Falha por Desajuste de Distribuição (Distribution Mismatch)

O estudo documenta um modo de falha crítico: um prompt otimizado para uma distribuição específica (ex: muitos casos Falso) pode falhar catastroficamente em uma distribuição balanceada.

• Exemplo: O prompt AN3c, otimizado para hard1 (35% Verdadeiro), atingiu 78,3% de acurácia. No entanto, em hard2 (50% Verdadeiro), a acurácia caiu para 60%, pois o prompt bloqueou incorretamente 51% dos casos Verdadeiros.

C. Efeito de Ordenação e o "Portão de Saída"

A descoberta mais significativa foi que a ordem das instruções é mais importante que o conteúdo adicional.

• A melhor variante local (AN45c) colocou a verificação de magma trivial (que força a igualdade de todos os elementos, tornando a implicação verdadeira) antes da tabela de busca de contraexemplos.
• Isso permitiu que o modelo "saísse" rapidamente com uma resposta Verdadeira antes de ser influenciado pela pressão das tabelas de contraexemplos (que tendem a empurrar para Falso).
• Resultado: AN45c alcançou 79,25% de acurácia localmente, superando o baseline sem "cola" (cheatsheet) em +19,5 pontos percentuais.

D. Hipótese do Roteador (Router Hypothesis)

Os autores propõem que os LLMs neste contexto não atuam como provadores de teoremas simbólicos, mas como classificadores heurísticos de padrões estruturais.

• O prompt funciona como um roteador que mapeia características estruturais (repetição de variáveis, profundidade de aninhamento) para uma decisão.
• Prompts que tentam ensinar novos raciocínios matemáticos falham; prompts que organizam o conhecimento existente de forma estruturada funcionam.

4. Resultados Chave

Métrica	Resultado Principal	Observação
Acurácia Local (gpt-oss-120b)	79,25% (AN45c, n=400)	IC 95%: [75,0%, 82,9%].
Acurácia Oficial (SAIR)	55,5% (AN45c)	Falha na generalização: Caiu abaixo do baseline (56,3%) na avaliação oficial devido a desajuste de distribuição.
Melhor Robustez	65,3% (AN38)	O prompt mais simples (AN38) teve melhor desempenho na avaliação oficial (+5,6pp sobre o baseline), demonstrando que "menos é mais" para generalização.
Comportamento Cruzado	Colapso em Llama	Prompts longos (>2KB) causaram 0% de recall de Verdadeiro no Llama 70B.
Eficiência de Custo	DeepSeek V3.2	Com o prompt mínimo (AN19c, 289 bytes), alcançou 80% de acurácia a um custo ~10x menor que o gpt-oss-120b.

Análise de Fusão (Merge Pattern)

Experimentos de combinar prompts complementares (ex: um bom para Verdadeiro, outro para Falso) resultaram em desempenho médio (aritmético), e não na soma das forças. Isso confirma que prompts estáticos não conseguem rotear dinamicamente entre estratégias conflitantes.

5. Significado e Conclusões

1. Menos é Mais: Aumentar a complexidade e o tamanho do prompt não melhora o raciocínio matemático formal além de um certo limite. Prompts curtos e bem ordenados superam prompts longos e elaborados.
2. Limitação de Engenharia de Prompt: Um prompt não pode ensinar ao modelo matemática que ele não internalizou. Ele apenas guia a aplicação do que o modelo já sabe. O "teto" observado (~79%) é uma barreira prática para prompts estáticos em tarefas assimétricas.
3. Fragilidade Distribucional: Ganhos obtidos em conjuntos de dados de validação locais não garantem generalização. A otimização para uma distribuição específica (ex: muitos Falsos) frequentemente degrada o desempenho em distribuições balanceadas.
4. Caminhos Futuros: Para superar esse teto, os autores sugerem:
   • Uso de ensembles com roteamento externo baseado em características sintáticas do problema.
   • Fine-tuning no grafo de implicações do Projeto Equational Theories (22 milhões de pares).
   • Arquiteturas híbridas LLM + Verificador Simbólico (onde o LLM propõe contraexemplos e uma ferramenta formal verifica).

Conclusão Final: O sucesso no raciocínio formal com LLMs atuais depende menos de adicionar mais conteúdo matemático ao prompt e mais de controlar a ordem e o fluxo com que o modelo aplica seu conhecimento interno. A estrutura deliberada e mínima supera a complexidade excessiva.