Resumo Técnico: Escapando do Poço Cognitivo: Matemática de Competição Eficiente com Modelos Prontos para Uso

Declaração do Problema

Avanços recentes em raciocínio matemático observaram modelos customizados e não lançados (ex: "Deep Think" do Google DeepMind) e pipelines agentes de larga escala alcançando desempenho de medalha de ouro na Olimpíada Internacional de Matemática (IMO). No entanto, esses sucessos dependem de orçamentos computacionais proibitivos, custando frequentemente milhares de dólares por problema (ex: ~$3.000/questão para o DeepSeekMath V2) e exigindo paralelismo massivo (até 64.000 chamadas de LLM por problema). Além disso, os pipelines existentes que utilizam modelos publicamente disponíveis costumam falhar ao resolver problemas difíceis de forma confiável em uma única chamada, necessitando de refinamento iterativo.

Os autores identificam dois modos de falha críticos em pipelines atuais de solver-grader que necessitam de tal paralelismo caro:

1. Platô Cognitivo: O solver faz progresso, mas o grader identifica falhas que o solver não consegue corrigir, levando a uma estagnação na pontuação.
2. Poço Cognitivo: Uma falha mais insidiosa onde o refinamento iterativo converge para uma solução logicamente consistente, mas fundamentalmente incorreta. O grader interno (frequentemente compartilhando os mesmos parâmetros e contexto do solver) é "contaminado" pelo contexto plausível, porém errôneo, classificando a solução falha com uma nota alta (ex: 7/7) e negligenciando erros fatais. Isso é comparado ao "reward hacking" ou ao ato de ficar preso em um mínimo local.

Metodologia

O artigo propõe um novo pipeline de inferência, o "pipeline Momus", projetado para alcançar desempenho de elite em problemas do tipo IMO usando apenas modelos de uso geral e prontos para uso a uma fração do custo. A metodologia baseia-se em três princípios fundamentais de design:

1. Largura Estreita (Paralelismo Limitado)

Em vez de paralelismo de força bruta (ex: 64 ramos), o pipeline limita o paralelismo a um nível modesto (tipicamente $K=4$ soluções concorrentes). Novas soluções são geradas condicionadas ao estado atual, que inclui soluções anteriores, feedback do grader e resultados de um processo de conjectura.

2. Extração de Conjecturas

Para abordar a incapacidade dos graders internos de distinguir entre "deslizes menores" e "lacunas fatais", o pipeline emprega um prompt de Solver com Conjecturas. Quando as provas estagnam, este módulo força o modelo a formalizar explicitamente lacunas lógicas como conjecturas autossuficientes (e suas negações). Isso transforma a incerteza vaga em afirmações matemáticas falsificáveis.

3. Destacamento Contextual

Para escapar do "Poço Cognitivo", o pipeline remove as conjecturas extraídas de seu contexto de prova pai. Estas conjecturas (e suas negações) são alimentadas como novos problemas independentes para instâncias frescas de solvers.

• Se uma conjectura é provada, ela é adicionada a uma Memória Global ($M_{lemma}$) para guiar futuros solvers.
• Se a negação de uma conjectura é provada, o pipeline usa isso para desacreditar ativamente a lógica da prova estagnada, forçando o solver a abandonar o caminho falho.

Arquitetura do Pipeline

O processo de inferência é um loop de estado com três fases:

• Fase I (Exploração Limitada): Gera um pequeno conjunto de soluções candidatas ($K=4$) usando um "Dialectic Solver" (um framework de engenharia de prompt de múltiplas personas). Um grader adversário verifica lacunas lógicas específicas.
• Fase II (Destacamento Contextual): Se as soluções forem plausíveis, mas não verificadas, o sistema extrai as conjecturas estruturais. Em seguida, executa instâncias paralelas para provar tanto a conjectura quanto sua negação em um contexto novo.
• Fase III (Refinamento com Memória Global): Novos solvers são lançados. A maioria é injetada com os lemas verificados da Fase II, enquanto um solver "zero-shot" permanece para manter a diversidade e evitar a queda de volta em um Poço Cognitivo.

O pipeline também inclui uma etapa de Pós-Melhoria onde, se nenhuma solução verificada for encontrada, o sistema reescreve as provas baseando-se nas conjecturas e executa uma etapa de agregação final para selecionar a melhor saída.

Principais Contribuições

1. Pipeline Eficiente: Um novo pipeline de solução usando apenas modelos prontos para uso que alcança desempenho de elite em problemas de matemática do tipo IMO a um custo ordens de magnitude menor que métodos concorrentes (ex: ~$9/questão vs. $3.000/questão).
2. Identificação de "Poços Cognitivos": O artigo identifica e fornece uma solução eficaz para o modo de falha "Poço Cognitivo" através de um mecanismo de destacamento de contexto baseado em conjecturas. Isso reduz falsos positivos de poços e aumenta mensuravelmente o desempenho.
3. Design de Grader e Avaliação: Os autores propõem novos métodos para projetar graders eficazes (usando um framework de "culpado até que se prove inocente") e avaliam o descompasso entre o desempenho de um grader como pontuador autônomo versus sua utilidade como provedor de feedback em um pipeline.
4. Acessibilidade de Código Aberto: Os prompts e a metodologia são disponibilizados em código aberto, demonstrando eficácia em modelos de fronteira (Gemini 3.1 Pro, Opus 4.6, DeepSeek-V3.2) a custos acessíveis, baixando a barreira de entrada para pesquisadores.

Resultados

O pipeline foi avaliado no IMO-ProofBench Advanced (PB-Adv), um benchmark de 30 questões curadas e difíceis do estilo IMO.

• Desempenho: Usando o Gemini 3.1 Pro, o pipeline alcançou 87,6% de desempenho (avaliado por especialistas), superando o modelo vencedor de ouro da IMO, o DeepThink, e mais que triplicando a taxa de sucesso do próximo melhor pipeline acessível publicamente (Huang e Yang [2025]) operando a um custo acessível.
• Eficiência de Custo: O custo médio por questão foi de aproximadamente $9. Isso é significativamente mais barato que o pipeline de Huang e Yang ($371/questão) e o DeepSeekMath V2 ($3.000/questão).
• Generalização: O método generalizou-se através de diferentes backbones. Por exemplo, no Claude 4.6 Opus, o desempenho saltou de uma chamada base de 23,8% para 85,7% com o pipeline. No DeepSeek-V3.2, melhorou de 15,2% para 66,7%.
• Estudos de Ablação: A remoção da etapa de extração de conjecturas resultou em uma queda significativa de desempenho (de 55% para 34,3% no PB-Adv com Gemini 2.5 Pro), mesmo quando os orçamentos de tokens foram equalizados, confirmando que os ganhos não se devem meramente ao aumento da diversidade de amostragem.

Significância

O artigo afirma que a prova de teoremas confiável por LLMs não requer necessariamente paralelismo massivo ou orçamentos de pensamento gigantescos. Ao identificar e abordar os modos de falha "Poço Cognitivo" e "Platô Cognitivo" através da extração de conjecturas e do destacamento contextual, os autores demonstram que modelos prontos para uso podem alcançar desempenho de estado da arte em problemas de matemática de competição difíceis a uma fração do custo.

O trabalho sugere que os atuais pipelines de solver-grader podem estar profundamente enraizados nesses modos de falha, o que poderia se estender a sistemas mais amplos de IA para a Ciência. Os autores enfatizam que sua abordagem reduz significativamente a barreira de entrada para a pesquisa em raciocínio matemático, tornando a resolução de problemas de alto nível acessível a pesquisadores sem acesso a modelos proprietários, customizados ou recursos massivos de computação.