Resumo Técnico: Julgando o que Não Podemos Resolver

Declaração do Problema

Avanços recentes em Grandes Modelos de Linguagem (LLMs) demonstraram a capacidade de gerar tentativas plausíveis de matemática de nível de pesquisa. No entanto, um gargalo crítico permanece: a verificação. Validar essas soluções normalmente requer o tempo escasso de especialistas ou depende de avaliadores "livres de oráculo" (oracle-free), como juízes de LLM e modelos de recompensa, que são frequentemente pouco confiáveis, tendenciosos e propensos a serem induzidos por pistas estilísticas ou afirmações de autoridade.

O desafio central abordado é como avaliar a correção de soluções candidatas para questões de nível de pesquisa onde as respostas de verdade fundamental (ground-truth) não estão disponíveis, os problemas são atualmente insolúveis para os modelos de estado da arte e a validação por especialistas não é escalável. Métodos existentes livres de oráculo (ex: votação majoritária, modelos de recompensa, juízes de LLM) lutam para distinguir soluções corretas de incorretas neste regime de alta dificuldade, muitas vezes falhando em separar o raciocínio válido de alucinações "plausíveis, mas erradas".

Metodologia: Utilidade Baseada em Consequência (CBU)

Os autores propõem a Utilidade Baseada em Consequência (CBU - Consequence-Based Utility), uma estrutura de avaliação livre de oráculo fundamentada no conceito matemático de "suporte por consequências". A hipótese central é que uma solução correta contém informação de nível de método que se transfere efetivamente para problemas relacionados, enquanto uma solução incorreta não o faz.

Mecanismo Central

1. Construção de Vizinhança: Para uma questão de nível de pesquisa alvo $Q$ e uma solução candidata $C$, o sistema constrói um conjunto de questões de vizinhança $\mathcal{N}(Q)$. Estas são variantes de $Q$ (ex: parâmetros modificados ou teoremas relacionados) que são projetadas para serem verificáveis (possuindo verdades fundamentais conhecidas) e ligeiramente mais fáceis que a questão original, porém solucionáveis utilizando a lógica de $C$.
2. Transferência em Contexto: A solução candidata $C$ é usada como um exemplar de contexto (in-context exemplar) para um modelo de resolução $M_\theta$. O resolvedor é instruído a resolver cada questão $Q^* \in \mathcal{N}(Q)$ condicionado a $(Q, C)$.
3. Pontuação de Utilidade: A pontuação de utilidade $U(C)$ é definida como a acurácia média do resolvedor nas questões de vizinhança quando $C$ é fornecido como contexto.
   $$U(C) = \frac{1}{|\mathcal{N}(Q)|} \sum_{Q^* \in \mathcal{N}(Q)} \mathbb{E}_{\tilde{C} \sim M_\theta(\cdot|Q,C,Q^*)} [v(Q^*, \tilde{C})]$$
   onde $v$ é um verificador que checa a correção da saída do resolvedor.
4. Classificação: Os candidatos são classificados por suas pontuações de utilidade induzidas. Uma pontuação mais alta implica que o candidato fornece um raciocínio mais útil e transferível, sugerindo que é mais provável que esteja correto.

Dataset: EXPERTMATH

Para avaliar esta abordagem, os autores introduzem o EXPERTMATH, um benchmark composto por:

• 192 problemas de nível de pesquisa escritos por especialistas (abrangendo teoria da representação, combinatória algébrica, geometria e teoria da homotopia). Metade destes permanece insolúvel para os principais modelos (ex: GPT-5, Gemini-3-Pro).
• 425 problemas gerados por LLM derivados da literatura existente.
• Verdade Fundamental (Ground Truth): Cada problema é pareado com uma solução escrita por especialista e nove soluções candidatas geradas por LLM (quatro corretas, cinco incorretas), verificadas manualmente por humanos.

Principais Contribuições

1. Utilidade Baseada em Consequência (CBU): Um novo método de validação livre de oráculo que pontua soluções com base em seu desempenho subsequente em questões relacionadas e verificáveis, em vez da inspeção direta do texto da solução.
2. Benchmark EXPERTMATH: Um conjunto de dados de alta dificuldade de problemas matemáticos de nível de pesquisa com soluções verificadas por especialistas e candidatos gerados por LLM, especificamente desenhado para testar métodos de avaliação em problemas que os modelos atuais não conseguem resolver diretamente.
3. Superioridade Empírica: Demonstração de que a CBU supera consistentemente as linhas de base (baselines) livres de oráculo, incluindo juízes de LLM, modelos de recompensa (RM) e modelos de recompensa generativos (GenRM).
4. Análise de Erros e Modos de Falha: Identificação de modos de falha específicos de juízes de LLM (ex: dependência excessiva de verbosidade, compressão injustificada e pistas de autoridade) que a CBU evita com sucesso ao penalizar soluções que falham em transferir o raciocínio.

Resultados Experimentais

Avaliado no EXPERTMATH usando modelos como GPT-OSS-120B e Qwen3-235B-A22B:

• Qualidade de Classificação: A CBU melhora significativamente as métricas de classificação sobre as linhas de base, incluindo juízes de LLM, modelos de recompensa (RM) e modelos de recompensa generativos (GenRM).
  • Para o GPT-OSS-120B atuando como o resolvedor/avaliador, a CBU melhora o Acc@1 (acurácia da solução melhor classificada) de 67,2% para 76,3% e o AUC (Área Sob a Curva) de 71,4% para 79,6%.
  • Ganhos semelhantes são observados para modelos menores (ex: o AUC do GPT-OSS-20B aumenta de 69,0 para 79,2).
• Gap entre Resolvedor e Avaliador: A CBU mantém uma separação maior entre soluções corretas e incorretas mesmo em questões que o próprio resolvedor subjacente não consegue resolver. Enquanto a capacidade dos juízes de LLM de distinguir soluções corretas de incorretas degrada-se drasticamente conforme a dificuldade do problema aumenta, a CBU permanece robusta.
• Poder Preditivo: Classificadores de regressão logística treinados em pontuações CBU alcançam maior acurácia na previsão de correção binária em comparação com aqueles treinados em pontuações de juízes de LLM (ex: ganhos de +6 a +18 pontos percentuais através de diferentes backbones).
• Robustez ao Estilo: Ao contrário dos juízes de LLM, que são frequentemente induzidos por soluções incorretas verbosas ou de tom "autoritário", a CBU rebaixa soluções com compressão injustificada (passos ausentes) e raciocínio incorreto, pois estas falham em fornecer informação transferível para as questões de vizinhança.

Significância e Alegações

O artigo alega que a Utilidade Baseada em Consequência oferece uma alternativa escalável e confiável à validação por especialistas humanos para outputs científicos de nível de pesquisa. Sua significância reside em:

• Validação Livre de Oráculo: Permite a avaliação de problemas "insolúveis" sem exigir um oráculo de verdade fundamental para a questão alvo específica.
• Mudança no Paradigma de Avaliação: Move a avaliação da "inspeção estática" (julgar o texto de uma prova) para a "utilidade dinâmica" (julgar a capacidade de uma prova de possibilitar a solução de problemas relacionados).
• Aplicabilidade Prática: Os autores fornecem um guia para o praticante, mostrando que a CBU permanece eficaz mesmo quando as questões de vizinhança são geradas por LLMs (desde que as questões alvo sejam suficientemente difíceis) e que estimativas estáveis podem ser alcançadas com um número moderado de rollouts (ex: $n \ge 8$).

Os autores concluem que a CBU é particularmente bem adequada para validação científica de alto risco, onde é necessária uma separação de alta confiança entre hipóteses corretas e incorretas, e onde os juízes tradicionais de LLM falham devido a erros sutis de raciocínio ou vieses estilísticos.