IndiMathBench: Autoformalizing Mathematical Reasoning Problems with a Human Touch

O artigo apresenta o IndiMathBench, um benchmark verificado por humanos composto por 312 teoremas em Lean 4 derivados de olimpíadas de matemática indianas e criados por meio de um pipeline assistido por IA, que demonstra os desafios contínuos da autoformalização e do raciocínio matemático em modelos de linguagem de ponta.

O essencial

Imagine que você tem um livro de contos de fadas cheio de histórias mágicas e aventuras (os problemas de matemática em linguagem natural). Agora, imagine que você precisa traduzir essas histórias para a linguagem de um robô super rigoroso e chato que só entende lógica pura e não aceita nem um ponto fora do lugar (a linguagem formal Lean 4).

O papel "INDIMATHBENCH" é como um novo e desafiador "campo de treinamento" criado por pesquisadores da Microsoft para testar o quanto os robôs (Inteligências Artificiais) estão bons nessa tradução.

Aqui está a explicação do que eles fizeram, usando analogias do dia a dia:

1. O Problema: A Barreira da Tradução

Até hoje, os robôs (LLMs) são ótimos em escrever textos bonitos, mas quando tentam transformar problemas matemáticos complexos em código que um computador pode verificar, eles tendem a "alucinar". É como se um tradutor tentasse traduzir um poema para uma língua que ele nunca estudou: ele inventa palavras que não existem ou erra a gramática.

Além disso, faltam "livros de exercícios" de alta qualidade para treinar esses robôs. Os existentes são poucos e, muitas vezes, os robôs já os viram durante o treinamento, o que distorce os resultados (é como se o aluno decorasse a resposta do livro em vez de aprender a resolver).

2. A Solução: Uma Equipe Humano-Robô (O "Banco de Dados IndiMath")

Os autores criaram o INDIMATHBENCH, um banco de dados com 312 problemas vindos das Olimpíadas de Matemática da Índia. Por que a Índia? Porque esses problemas têm um estilo único (muita geometria e combinatória) que os robôs adoram errar, servindo como um teste de estresse real.

Mas como eles criaram 312 problemas perfeitos sem gastar anos? Usando uma ferramenta de "cozinha colaborativa":

• O Chefe (Humano): Um especialista em matemática e programação.
• Os Cozinheiros (Robôs/LLMs): Vários modelos de IA diferentes tentam "cozinhar" (escrever o código) o problema.
• O Processo:
  1. O robô tenta escrever o código.
  2. O computador (o "chefe de cozinha") diz: "Isso não compila, tem um erro de sintaxe aqui".
  3. O robô tenta de novo, corrigindo o erro.
  4. Eles fazem isso várias vezes (até 6 tentativas).
  5. O Grande Truque: Eles usam 12 robôs diferentes para tentar o mesmo problema. Depois, um "gerente" (outro robô) lê todas as tentativas, resume o que deu certo e o que deu errado, e mostra tudo para o Chefe Humano.
  6. O humano olha para esse resumo, pega as melhores partes de cada tentativa e faz o ajuste final.

A Analogia do "Montagem de Móveis":
Imagine que você precisa montar um móvel complexo.

• Sem ajuda: Você lê o manual e tenta montar sozinho. Demora horas e pode ficar torto.
• Com a ajuda do INDIMATHBENCH: Você pede para 12 pessoas diferentes montarem o móvel. Elas enviam fotos das tentativas. Um robô analisa as fotos e diz: "A pessoa A acertou a perna, a pessoa B acertou a porta, mas ninguém acertou o parafuso X". Você, o humano, pega a perna da A, a porta da B, e conserta o parafuso X. O resultado é um móvel montado em 4 minutos, em vez de 2 horas.

3. Os Resultados: Os Robôs Ainda Estão "Aprendendo a Andar"

Quando testaram os robôs mais inteligentes do mundo (como o GPT-5 e o Claude) nesse novo banco de dados, a notícia não foi tão animadora:

• Tradução (Autoformalização): Os robôs conseguem escrever código que parece correto (sintaxe), mas muitas vezes o significado está errado (semântica). É como escrever uma frase em inglês perfeitamente gramatical, mas que diz o oposto do que você queria.
• Prova (Theorem Proving): Quando pediram para os robôs provar que a resposta estava certa, eles falharam quase totalmente.
  • Em tentativas únicas, eles resolveram apenas 1 problema entre 312.
  • Com 10 tentativas e correções (como um aluno que erra, vê a correção e tenta de novo), o melhor modelo (GPT-5) conseguiu resolver cerca de 11% dos problemas.

A Lição: A matemática formal exige um nível de precisão que a IA atual ainda não alcançou sozinha. A IA é ótima em sugerir ideias, mas ainda precisa de um "olho humano" para garantir que a lógica não está vazia.

4. O Legado: Uma Ferramenta para Todos

Os autores não apenas criaram o banco de dados, mas liberaram uma extensão para o VS Code (um editor de código). É como um "assistente de tradução" que ajuda humanos a formalizar matemática mais rápido, mostrando as melhores tentativas dos robôs e resumindo os erros.

Resumo Final:
O paper diz: "Nós criamos um novo teste de matemática difícil, mostramos que os robôs ainda tropeçam muito sozinhos, mas descobrimos que, se você deixar os robôs fazerem o trabalho pesado de rascunho e usar humanos para polir o resultado, podemos criar bancos de dados de alta qualidade muito mais rápido. É uma parceria onde o humano é o maestro e a IA é a orquestra que ainda precisa de regência."

Resumo técnico

Resumo Técnico: INDIMATHBENCH

1. O Problema

A autoformalização (tradução automática de raciocínio matemático informal para lógica formal verificável por máquina, como Lean) permanece um desafio significativo, mesmo na era dos Grandes Modelos de Linguagem (LLMs). Os principais obstáculos identificados são:

• Escassez de Dados: A falta de dados de treinamento de alta qualidade, pareando problemas informais com formalizações corretas.
• Custo de Anotação: A criação de benchmarks existentes (como MINIF2F e PutnamBench) depende de anotação manual intensiva por especialistas, o que é lento e caro.
• Contaminação de Dados: Muitos benchmarks populares já estão presentes nos corpora de pré-treinamento dos LLMs, obscurecendo a avaliação real da capacidade de raciocínio.
• Desalinhamento Semântico: Embora os LLMs tenham melhorado na fidelidade sintática, eles ainda falham em alinhar o significado matemático profundo com a lógica formal, especialmente em domínios como geometria e combinatória.
• Limitação de Escopo: Os benchmarks atuais cobrem principalmente álgebra e teoria dos números, sub-representando geometria e combinatória, que são áreas críticas e desafiadoras nas Olimpíadas de Matemática.

2. Metodologia

Os autores introduzem o INDIMATHBENCH, um benchmark verificado por humanos composto por 312 problemas das Olimpíadas de Matemática da Índia (RMO e INMO), cobrindo Geometria, Álgebra, Teoria dos Números e Combinatória.

A construção do benchmark utiliza um pipeline híbrido de IA e Humanos com as seguintes etapas:

• Recuperação Baseada em Categoria: Os problemas são classificados em domínios. Um agente de IA explora a biblioteca Mathlib do Lean para extrair definições e teoremas relevantes, criando um contexto estático para cada categoria. Isso reduz alucinações de imports e sintaxe.
• Refinamento Iterativo com Feedback do Compilador:
  1. Um LLM gera uma formalização inicial baseada no contexto.
  2. O código é compilado no Lean 4.
  3. Erros de sintaxe ou de tipo são extraídos e retornados ao modelo como feedback.
  4. Este ciclo repete-se até 6 vezes, alcançando uma taxa de validade sintática de 95,3%.
• Ensemble Multi-Modelo: 12 modelos de ponta (incluindo GPT-5, Claude Opus 4, Gemini 2.5 Pro) geram candidatos para cada problema. As saídas são agregadas e resumidas por um LLM para identificar erros comuns e candidatos promissores.
• Dashboard de Colaboração Humano-AI: Os autores desenvolveram uma extensão para o VS Code que consolida as gerações dos modelos, resumos de qualidade e feedback de compilação. Isso permite que anotadores humanos validem e corrijam rapidamente as formalizações, focando apenas nos casos ambíguos ou com erros críticos.
• Verificação Humana Rigorosa: Todos os 312 teoremas foram revisados manualmente por especialistas em Lean para garantir a correção semântica e a qualidade estilística.

3. Principais Contribuições

1. Novo Benchmark (INDIMATHBENCH): Um conjunto de dados de 312 problemas de Olimpíada Indianos com formalizações Lean 4 verificadas por humanos, preenchendo lacunas em geometria e combinatória.
2. Pipeline de Autoformalização Escalável: Uma metodologia sistemática que combina recuperação de contexto, feedback de compilador e ensembles de modelos para acelerar a anotação humana.
3. Ferramenta de Colaboração: Uma extensão do VS Code open-source que facilita a anotação e validação de formalizações matemáticas.
4. Estudo Controlado de Eficiência: Uma avaliação quantitativa que demonstra como o pipeline proposto reduz drasticamente o tempo de anotação humana em comparação com a formalização manual pura.

4. Resultados Experimentais

A. Avaliação de Autoformalização (Qualidade da Tradução):

• Métricas: Utilizaram Bidirectional Equivalence (BEq) para equivalência lógica e Generalized Tree Edit Distance (GTED) para similaridade sintática.
• Desempenho: O modelo Claude Opus 4 liderou com 67 formalizações passando no teste BEq (equivalência lógica) e 243 compilando com sucesso.
• Gap Sintático vs. Semântico: Há uma grande discrepância entre código que compila e código que é semanticamente correto. Por exemplo, o Claude Opus 4 teve 77,9% de sucesso na compilação, mas apenas 21,5% de precisão semântica (BEq).
• Dificuldade em Geometria: Apenas 12 dos 108 problemas resolvidos pelos melhores modelos (Claude Opus 4, Gemini 2.5 Pro, GPT-5) foram de geometria, indicando que a falta de suporte robusto no Mathlib para geometria competitiva é um gargalo.

B. Avaliação de Prova Automática (ATP):

• Os modelos foram testados para provar os teoremas gerados (substituindo sorry por uma prova válida).
• Cenário de Turno Único: A taxa de sucesso foi extremamente baixa (apenas 1 problema resolvido por modelo entre os 312).
• Cenário de 10 Turnos (Refinamento Iterativo): Com feedback do compilador e múltiplas tentativas, o GPT-5 alcançou 36/312 (11%) de sucesso no INDIMATHBENCH e 28/660 (4%) no PutnamBench.
• Conclusão: Mesmo com refinamento iterativo, a taxa de sucesso permanece baixa, evidenciando a dificuldade extrema da prova formal de teoremas de nível olímpico.

C. Eficiência da Anotação Humana:

• Um estudo comparativo mostrou que a formalização manual leva em média 14 minutos por problema.
• O uso de candidatos gerados por IA (sem resumos) reduziu para 9 minutos.
• O sistema completo (com resumos e dashboard) reduziu o tempo para 4 minutos por problema (uma aceleração de 3,5x em relação ao manual).

5. Significado e Impacto

• Validade do Benchmark: O INDIMATHBENCH oferece um conjunto de dados "limpo" (não contaminado por pré-treinamento) e diversificado, essencial para avaliar o verdadeiro raciocínio matemático de LLMs.
• Limitações Atuais: Os resultados confirmam que, embora os LLMs de ponta possam gerar código Lean sintaticamente válido, eles ainda lutam para capturar a intenção semântica complexa e realizar provas completas sem intervenção humana significativa.
• Futuro da Colaboração: O trabalho demonstra que a abordagem mais promissora não é a automação total, mas sim um ciclo de colaboração humano-IA, onde a IA gera candidatos e sugere correções, e o humano valida a lógica matemática.
• Reprodutibilidade: O código, o dataset e a extensão do VS Code foram disponibilizados como recursos open-source para avançar a pesquisa em prova de teoremas neural e autoformalização.

Em suma, o artigo estabelece que a autoformalização e a prova automática de matemática de nível olímpico ainda estão em estágios iniciais, exigindo ferramentas de suporte robustas e verificação humana para garantir a confiabilidade dos resultados.