MathForm: Scaling Mathematical Autoformalization with Knowledge Retrieval and Verification-Guided Refinement

Imagine que você está tentando ensinar um robô brilhante, mas ligeiramente desastrado, a falar a linguagem da lógica pura. Este robô, um Modelo de Linguagem de Grande Escala (LLM), é incrível em ler histórias, escrever poemas e resolver enigmas matemáticos em inglês comum. Mas há um porém: para provar um teorema matemático com certeza absoluta, você não pode apenas usar palavras; você precisa escrevê-lo em uma linguagem de computador superestrita chamada Lean 4. Pense no Lean 4 como um cofre de alta segurança onde cada palavra, símbolo e regra deve ser perfeita, ou a porta do cofre não abrirá. O problema é que o robô conhece matemática, mas não conhece o "livro de regras" específico (chamado Mathlib) que o Lean 4 utiliza. É como pedir a um chef que sabe cozinhar um bife perfeito para seguir uma receita escrita em uma língua que ele nunca viu, usando ingredientes cujos nomes ele desconhece. Ele pode até tentar adivinhar, mas provavelmente errará.

É aqui que entra a "autoformalização": a arte de traduzir a matemática humana para este código de computador estrito. Por muito tempo, pesquisadores tentaram apenas pedir ao robô para "traduzir" a matemática, esperando que ele lembrasse das regras de seu treinamento. Mas o robô continuava cometendo erros, como usar os ingredientes errados ou esquecer um passo crucial, porque estava tentando confiar apenas em sua memória. O novo artigo, MathForm, argumenta que essa abordagem de "adivinhar e esperar" está quebrada. Em vez disso, eles construíram um sistema onde o robô tem permissão para consultar o livro de regras antes de começar a escrever e, se cometer um erro, um editor rigoroso não apenas joga o trabalho fora — ele diz ao robô exatamente o que deu errado e permite que ele tente novamente até acertar.

Os pesquisadores por trás do MathForm perceberam que, para fazer um robô falar a linguagem da matemática formal perfeitamente, você não pode simplesmente deixá-lo escrever um rascunho e esperar o melhor. Eles construíram uma linha de montagem de três etapas para corrigir o fluxo de trabalho do robô. Primeiro, antes que o robô escreva uma única linha de código, um agente "Pesquisador" varre a massiva biblioteca Mathlib para encontrar as definições e regras exatas que o robô precisa para aquele problema específico. É como dar ao chef a página específica do livro de receitas para "Bife" antes mesmo de ele pegar uma faca. Segundo, o robô escreve seu código e, em seguida, um "Inspetor" o verifica. Se o código tiver um erro de sintaxe (como uma vírgula ausente), o Inspetor aponta o erro. Se o código compilar, mas significar a coisa errada (como dizer "todos os números" quando o problema pretendia dizer "apenas números positivos"), o Inspetor explica o erro semântico. Terceiro, em vez de desistir, o robô usa esse feedback para reescrever seu código. Ele continua repetindo este ciclo de "escrever-verificar-corrigir" até que o código esteja perfeito.

Usando este ciclo inteligente, a equipe criou um novo e massivo conjunto de dados chamado FormalVerse, contendo cerca de 367.000 exemplos matemáticos verificados. Eles então treinaram um novo modelo, o MathForm-8B, com esses dados. Os resultados foram surpreendentes: este modelo relativamente pequeno (8 bilhões de parâmetros) tornou-se melhor em formalizar matemática do que modelos especializados muito maiores (32 bilhões de parâmetros) que dependiam dos antigos métodos de "adivinhar e esperar". Em seis testes matemáticos difíceis diferentes, o MathForm-8B passou na rigorosa "Verificação de Consistência" (o que significa que o código realmente significava o que o problema humano dizia) cerca de 72,4% das vezes, superando os melhores modelos anteriores. Mesmo nos problemas de álgebra abstrata mais difíceis e complexos, ele superou significativamente seus rivais maiores. O artigo sugere que, ao dar ao modelo as ferramentas certas para buscar informações e a chance de aprender com seus erros, você não precisa de um cérelar gigante para ser um gênio da matemática; você só precisa de um fluxo de trabalho inteligente.