A OpenBMB liberou por completo seu sistema MathForm de formalização matemática automática: os pesos do modelo de 8B, um conjunto de dados com cerca de 367 mil exemplos verificados em Lean 4, o código de avaliação e os scripts de Pass@k. O modelo está hospedado no Hugging Face sob licença Apache 2.0, construído sobre o Qwen3-8B, com pesos em precisão BF16. O projeto foi conduzido pela equipe da OpenBMB, com apoio do laboratório de processamento de linguagem natural de Tsinghua e da ModelBest; o artigo de mesmo nome, assinado por dez autores, foi submetido ao arXiv em meados deste mês.
A formalização automática consiste em traduzir proposições matemáticas escritas em linguagem natural para uma linguagem formal verificável por máquina, como o Lean 4. A dificuldade não está na tradução literal. A hierarquia de tipos e o conjunto de definições do Mathlib são enormes: noções como "função contínua" ou "grupo finito" precisam corresponder exatamente à definição certa dentro da biblioteca, ao mesmo tempo em que a proposição formalizada precisa continuar dizendo a mesma coisa que a original. Se qualquer um dos dois pontos falhar, o compilador ainda assim pode validar o resultado.
Como os dados foram construídos
O pipeline do MathForm tem quatro etapas. Um planejador consulta primeiro o Mathlib sobre os conceitos matemáticos presentes na proposição, com a ferramenta de busca LeanExplore retornando sempre os 22 melhores resultados. O modelo então gera a proposição em Lean 4 condicionado a esse contexto recuperado. Os candidatos passam por uma verificação de formato, um teste de compilação e, em seguida, um julgamento de consistência semântica feito por um modelo de linguagem atuando como juiz. As trajetórias bem-sucedidas são reconstruídas retroativamente como trajetórias de treinamento limpas.
Um número do artigo ilustra por que a iteração é necessária: as rodadas seguintes contribuíram com 31,0% adicionais sobre o total de amostras finalmente retidas. Ou seja, se fosse feita apenas uma única geração e os exemplos inválidos fossem descartados, quase um terço dos dados utilizáveis seria perdido.
A busca de informação é o elemento mais econômico de todo o projeto. Pedir a um modelo que lembre de memória o nome exato e a assinatura de uma definição do Mathlib é, essencialmente, testar se ele decorou uma biblioteca que continua sendo atualizada. Ao delegar a biblioteca a uma ferramenta de busca e deixar que o modelo apenas monte os resultados, a quantidade de parâmetros necessária cai naturalmente. Isso também explica por que um modelo de 8B consegue competir com um de 32B: no fundo, os dois não estão resolvendo o mesmo problema.
O conjunto de dados resultante se chama FormalVerse, com cerca de 367 mil amostras verificadas, vindas de DeepTheorem, NuminaMath, AceReason-Math, Lean Workbook, Principia-Collection, DeepMath e OpenR1-Math, complementadas com conteúdo de livros didáticos clássicos. Esse conjunto de dados já recebeu 358 curtidas no Hugging Face.
O boletim de resultados e seus dois critérios
O treinamento combina ajuste fino supervisionado seguido de aprendizado por reforço. A avaliação cobre seis benchmarks: FormalMATH-Lite e DeepSeek-ProverBench tratam de matemática competitiva, CombiBench testa combinatória, e a série FATE é dividida em três níveis de dificuldade algébrica: M, H e X.
O MathForm-8B obtém, em média, Pass@8 de 88,06% na verificação de sintaxe e 72,37% na verificação de consistência; as taxas de consistência nos três níveis do FATE são, respectivamente, 97,33%, 63,00% e 37,00%. Os modelos de comparação incluem Herald Translator-7B, Kimina-Autoformalizer-7B, Mathesis-HPO-7B, além das versões de 7B/8B e 32B do StepFun-Formalizer, Goedel-Formalizer-V2 e ReForm. O modelo de 8B supera, em vários conjuntos de teste, os modelos de formalização especializados de 32B.
A diferença entre os dois critérios diz mais do que os números absolutos. A verificação de sintaxe só pergunta se o código compila; a verificação de consistência pergunta se a proposição formalizada significa a mesma coisa que a original — 88% contra 72%, e esses dez e tantos pontos percentuais são exatamente o gargalo real dessa cadeia hoje. Algo que compila não é necessariamente o teorema que se queria provar.
A barreira cai para uma única estação de trabalho
Este site publicou há poucos dias o alerta de Terence Tao de que provas geradas por IA poderiam se acumular a ponto de ninguém conseguir lê-las todas. A formalização oferece a outra metade da resposta para esse problema: enquanto uma prova passar pelo compilador Lean, entendê-la deixa de ser pré-requisito para aceitá-la. O que continua sendo pré-requisito é que a proposição em si esteja traduzida corretamente, e os 37% obtidos no FATE-X mostram que ainda há um caminho considerável até lá.
Fazendo as contas por alto, um modelo de 8B carregado em BF16 precisa de cerca de 16 GB de memória de vídeo, enquanto um de 32B na mesma precisão fica na faixa de 64 GB. O primeiro roda em uma única placa de vídeo de consumo de 24 GB; o segundo exige múltiplas placas ou hardware profissional. Para departamentos de matemática universitários, a comunidade de assistentes de prova e equipes pequenas, a barreira de hardware para rodar um pipeline de formalização cai assim do nível de cluster para o nível de uma única máquina. Com o conjunto de dados e o código de avaliação publicados ao mesmo tempo, o custo para terceiros reproduzirem e testarem o trabalho também diminui.
A lista de modelos comparados também mostra o quanto essa área já está disputada: Herald, Kimina, Mathesis, StepFun-Formalizer, Goedel-Formalizer-V2, ReForm — todos modelos de formalização especializados surgidos no último ano ou dois, e todos de código aberto. Diferente do diálogo de propósito geral, a formalização não avança apenas com poder computacional, mas com a qualidade da construção de dados e o ciclo de verificação; o tamanho dos parâmetros passa a ser uma variável secundária. Ver um pipeline sair de uma demonstração em artigo para uma entrega de código aberto nesse ritmo é mais rápido do que a maioria esperava.
Fontes: repositório do projeto e ficha do modelo da OpenBMB, CocoLoop, preprint do arXiv 2608.14221, página do conjunto de dados no Hugging Face; foram verificados o tamanho dos parâmetros, a licença, o volume de amostras do FormalVerse e os números de Pass@8 de cada conjunto de teste.