Resumo Técnico: IMProofBench

Declaração do Problema

Os benchmarks atuais para avaliar Grandes Modelos de Linguagem (LLMs) em matemática são insuficientes para avaliar capacidades de nível de pesquisa. Os conjuntos de dados existentes focam primariamente em problemas de nível de ensino médio ou graduação (ex: AIME, MATH), que são cada vez mais solúveis por modelos de última geração e falham em testar a verdadeira capacidade de escrita de provas. Além disso, benchmarks que visam matemática avançada, como o FrontierMath e o Humanity's Last Exam (HLE), frequentemente restringem a avaliação à correção da resposta final. Essa limitação permite que os modelos empreguem atalhos ou adivinhem respostas corretas sem construir argumentos logicamente sólidos, negligenciando, assim, a habilidade crítica de gerar provas matemáticas rigorosas. Há uma carência de um benchmark privado e padronizado que avalie a geração de provas de nível de pesquisa dentro de um ambiente realista e aumentado por ferramentas.

Metodologia

Construção do Benchmark (IMProofBench)

O IMProofBench é um benchmark privado composto por 77 problemas revisados por pares, desenvolvidos em colaboração com mais de 44 matemáticos profissionais. O pipeline de criação de problemas envolve:

• Autoria: Os problemas são elaborados por pesquisadores dentro de suas áreas específicas de especialidade, variando de questões de exames orais de pós-graduação a problemas de pesquisa aberta.
• Revisão por Pares: Cada submissão passa por um processo rigoroso de revisão por um membro da equipe central e um especialista externo na área relevante para garantir a correção matemática, a dificuldade apropriada e a clareza.
• Estrutura: Cada problema consiste em uma tarefa principal de escrita de prova e subquestões de acompanhamento com respostas únicas e automaticamente graduáveis. Esta estrutura dupla suporta tanto a avaliação de especialistas humanos da prova quanto a análise quantitativa automatizada de respostas finais.
• Natureza Dinâmica: O benchmark foi projetado como uma plataforma contínua. Problemas são adicionados de forma rotativa, e os autores são incentivados a aposentar problemas caso estes se tornem solucionáveis devido a novas pesquisas, garantindo que o benchmark não fique saturado.

Estrutura de Avaliação

A avaliação simula um ambiente de pesquisa realista usando uma estrutura de agentes construída sobre o framework Inspect. Os modelos operam com acesso a:

• Ferramentas Computacionais: Python (NumPy, SciPy, SymPy), Bash (Arch Linux) e softwares matemáticos especializados, incluindo SageMath, GAP, Maxima, PARI/GP e Singular.
• Busca de Literatura: Capacidades de busca na web para localizar teoremas, artigos ou dados relevantes (ex: OEIS).
• Interação: Os modelos participam de interações de múltiplos turnos, utilizando uma ferramenta submit para distinguir etapas de raciocínio de saídas finais.

Processo de Graduação

A avaliação ocorre em duas etapas:

1. Graduação Automatizada: As subquestões de acompanhamento são graduadas comparando as saídas do modelo com as respostas de referência (ground-truth).
2. Graduação por Especialista Humano: A prova principal é avaliada pelo autor do problema usando uma escala de 0 a 3:
   • 0/3: Sem progresso.
   • 1/3: Progresso mínimo (avanço limitado).
   • 2/3: Progresso significativo (trabalho substancial concluído).
   • 3/3: Solução completa.
     Os graduadores também anotam tipos específicos de erro (erros lógicos, alucinações, erros de cálculo, incompreensões conceituais) e indicadores de realização (compreensão, resultados corretos, insights, utilidade). Para evitar viés, as identidades dos modelos são ocultadas durante a graduação.

Principais Contribuições

1. IMProofBench: Um benchmark privado e evolutivo, projetado especificamente para a geração de provas matemáticas de nível de pesquisa, desenvolvido através de colaboração direta com a comunidade matemática.
2. Análise Sistemática: Uma avaliação abrangente de LLMs de última geração na geração de provas, julgada por especialistas humanos, indo além da simples precisão da resposta final.
3. Insights Qualitativos: Uma análise detalhada das forças e modos de falha dos modelos, destacando a lacuna entre a precisão da resposta final e a capacidade genuína de escrita de provas, bem como a interação dos modelos com ferramentas de pesquisa.

Resultados Experimentais

Visão Geral do Desempenho

Os autores avaliaram 10 LLMs na parte baseada em provas do benchmark:

• Melhores Desempenhos: O GPT-5.4 alcançou o maior desempenho, produzindo soluções completas (3/3) para 49% das tarefas. O GEMINI-3.1-PRO seguiu de perto com 46%.
• Desempenhos Inferiores: O CLAUDE-OPUS-4.6 forneceu soluções completas para apenas 32% das tarefas.
• Problemas Abertos: Entre as 23 questões de pesquisa aberta no benchmark, o GPT-5 resolveu uma em dezembro de 2025.

Resposta Final vs. Geração de Prova

No subconjunto de 45 questões com subquestões de acompanhamento, o GPT-5.4 obteve 75% de precisão na resposta final. A correlação entre as pontuações das subquestões e o progresso da prova graduado por humanos foi de 0,51, sugerindo que, embora a precisão da resposta final seja um proxy útil, ela carece da nuance necessária para avaliar a qualidade do processo de raciocínio.

Análise de Erros e Ferramentas

• Tipos de Erro: Erros lógicos foram o modo de falha mais comum (ex: suposições infundadas), particularmente no CLAUDE-OPUS-4.6 (40% das respostas). Alucinações de teoremas inexistentes também foram observadas.
• Uso de Ferramentas: Os modelos variaram significamente no uso de ferramentas. O GEMINI-3.1-PRO realizou quase quatro vezes mais chamadas de ferramentas do que outros modelos, mas utilizou o menor número de tokens de saída.
• Estudo de Ablação: Uma ablação na configuração de agentes revelou que o acesso a ferramentas geralmente melhorou o desempenho (ex: +14,4% para o GROK-4), embora alguns modelos (ex: GEMINI-2.5-PRO) tenham visto pequenas quedas, provavelmente devido à seleção subótima de ferramentas (ex: uso excessivo de interpretadores de código para raciocínio matemático).

Observações Qualitativas

• Conhecimento de Literatura: Os modelos líderes demonstraram forte familiaridade com a literatura matemática especializada, mas tiveram dificuldades com fontes obscuras, como notas de aula privadas.
• Alucinação e Confiança: Os modelos frequentemente alucinaram resultados para forçar uma resposta e raramente se abstiveram de fornecer uma solução, mesmo quando estavam travados. Eles frequentemente apresentavam argumentos falhos com alta confiança.
• Insight: Apesar dos erros, os modelos frequentemente forneceram insights e progresso parcial que poderiam ser úteis para pesquisadores humanos, com o GPT-5.4 oferecendo contribuições significativas em aproximadamente 60% das tentativas.

Significância e Alegações

O artigo afirma que o IMProofBench aborda uma lacuna crítica na avaliação de IA ao mudar o foco de problemas de estilo competição para a geração de provas de nível de pesquisa. Os autores afirmam que:

1. Capacidades Atuais: LLMs de última geração já podem resolver um subconjunto significativo de problemas de nível de pesquisa, indicando seu potencial como colaboradores matemáticos.
2. Limitações: Os modelos atuais permanecem imperfeitos, propensos a erros lógicos e alucinações, e muitas vezes carecem da habilidade de distinguir entre uma resposta final correta e uma prova válida.
3. Necessidade de Avaliação: O benchmark demonstra que métricas de resposta final são insuficientes para medir a capacidade matemática; a avaliação humana especialista do processo de raciocínio é essencial.
4. Direção Futura: O trabalho estabelece um framework para avaliação contínua e dinâmica de LLMs em ambientes de pesquisa realistas, facilitando o estudo de como a IA pode ser efetivamente integrada aos fluxos de trabalho matemáticos.

Os autores mantêm uma postura modesta, observando que o benchmark está atualmente em desenvolvimento ativo com um número limitado de problemas (77), mas argumentam que mesmo esta escala fornece insights valiosos sobre a trajetória da IA na pesquisa matemática.