AlphaProof Code vs MathForm-8B: Duas Etapas do Mesmo Pipeline Lean, Não Dois Rivais

Leia o artigo do AlphaProof Code com atenção e um número salta aos olhos que o anúncio não enfatiza: das quatro semanas que os cinco pesquisadores do DeepMind passaram verificando o Signal, a parte que não pôde ser automatizada foi a etapa inicial. Especialistas humanos trabalharam com uma mistura de modelos para traduzir os objetivos de segurança do Signal em especificações formais em Lean, e um especialista revisou cada uma delas antes de qualquer trabalho de prova começar. Esse é o gargalo. O MathForm-8B, modelo de autoformalização de 8 bilhões de parâmetros da OpenBMB lançado no Hugging Face em 14 de agosto de 2026, é uma tentativa direta de automatizar exatamente essa etapa — pegar um enunciado matemático em linguagem natural e emitir um enunciado de teorema em Lean 4 pronto para outra pessoa provar. Coloque-os lado a lado e você não está comparando dois produtos. Você está olhando para duas etapas consecutivas de um mesmo pipeline, separadas pela diferença entre matemática e segurança de protocolos.

O pipeline, na ordem em que o trabalho acontece

A verificação formal de software real tem três tarefas. Primeiro, decidir o que deve ser verdadeiro e registrá-lo em uma linguagem formal. Segundo, provar que a implementação o satisfaz. Terceiro, verificar as provas mecanicamente, porque uma prova errada é pior do que nenhuma prova.

O MathForm-8B faz a primeira tarefa, para uma classe restrita de entradas: afirmações matemáticas no estilo de livro didático. Dê a ele “para todo número real x, x² é não negativo” e ele retorna os imports, os tipos e um cabeçalho de teorema em Lean 4. O que ele não retorna é uma prova, e seus autores deixam explícito que a busca por provas é problema de outra pessoa. Seus números relatados, todos informados pelo fornecedor e não reproduzidos, são 88,06% de Pass@8 médio sob uma verificação de sintaxe e 72,37% sob a verificação de consistência mais rigorosa em seis benchmarks — a diferença entre esses dois números é a medida honesta de com que frequência uma afirmação sintaticamente válida significa algo diferente do que foi pedido.

O AlphaProof Code executa os trabalhos dois e três, além de uma etapa de especificação que o MathForm-8B não conseguia abordar. Os objetivos de segurança do Signal não são afirmações matemáticas no sentido em que o MathForm foi treinado; são declarações sobre um protocolo — de que as mensagens permanecem protegidas antes e depois de um dispositivo ser temporariamente comprometido, de que o iniciador e o respondedor são quem dizem ser. Converter isso em Lean exigia conhecimento especializado de protocolo que nenhum autoformalizador de 8B possui. Depois que a especificação existiu, o trabalho de prova foi entregue inteiramente a agentes, e a verificação foi entregue ao kernel do Lean mais um agente de controle usando comparador contra uma cópia reservada da especificação.

Quanto cada um realmente custa para você usar

• Pesos — MathForm-8B: disponível para download, Apache 2.0, quatro shards safetensors em BF16, fine-tuned a partir do Qwen3-8B. AlphaProof Code: nenhum. A versão é um desenvolvimento Lean, uma semântica AArch64 e um binding libsignal em github.com/google-deepmind/code-verification.

• Executá-lo — MathForm-8B: Transformers, vLLM ou SGLang, todos expondo um endpoint compatível com OpenAI, em hardware próprio. AlphaProof Code: sem endpoint, sem API, sem lista de espera, sem preço; é um framework de pesquisa que o DeepMind diz precisar de "pesquisa contínua" antes de escalar.

• Entrada — MathForm-8B: uma afirmação matemática em linguagem natural. AlphaProof Code: uma especificação formal mais o binário que você deseja provar em relação a ela.

• Saída — MathForm-8B: um enunciado de teorema em Lean 4, não provado. AlphaProof Code: uma prova verificada por máquina, ou uma refutação quando o código está quebrado.

• Revisão humana — MathForm-8B: você revisa a afirmação emitida e, com 72,37% de consistência, vai revisar muitas delas. AlphaProof Code: especialistas revisam cada especificação antes de o trabalho de prova começar; depois, agentes sinalizam cerca de 1% da base de código para uma segunda análise.

• Limites conhecidos — MathForm-8B: apenas afirmações matemáticas, sem geração de provas, e o repositório de código vinculado em seu README ainda era um espaço reservado no momento do lançamento. AlphaProof Code: nenhuma garantia pós-quântica para o healing do SPQR, nenhuma privacidade do payload, uma sessão por promoção e um limite de falsificação de MAC que se torna vazio perto de 25.000 mensagens em uma única sessão.

A lacuna que o MathForm-8B teria de fechar

É tentador dizer que um autoformalizador poderia ter escrito as especificações do Signal e poupado aos pesquisadores as semanas de trabalho inicial. O próprio relato do artigo diz o contrário, e o motivo é específico. Uma especificação de protocolo não é uma reafirmação de uma afirmação; é uma escolha sobre o modelo de adversário. O trabalho sobre o Signal traz uma trilha simbólica em Dolev–Yao com um atacante quântico que quebra Diffie–Hellman após o handshake, e uma trilha computacional com adversários clássicos e um limite concreto. Essas duas trilhas enunciam teoremas diferentes sobre o mesmo código, e escolher entre elas é uma decisão de engenharia com consequências de segurança. Nenhum modelo treinado para transformar “mostrar que x² ≥ 0” em Lean vai tomar essa decisão.

O que um autoformalizador plausivelmente poderia fazer é a parte mecânica desse trabalho: dado um objetivo de segurança em prosa e uma biblioteca de definições Lean existentes, produzir um primeiro rascunho do enunciado no idioma próprio do projeto, para que um especialista o corrija. Isso é uma economia real e muito menor do que a manchete sugere. O artigo relata um catálogo de desvios de especificação com mais de 200 entradas computacionais e cerca de 35 simbólicas — quinze delas lacunas ou bugs na análise do Double Ratchet — que foi o que a etapa de revisão humana encontrou. Um modelo que rascunha enunciados teria de ser medido em relação a esse catálogo, e não em relação a uma pontuação Pass@8 em benchmarks de matemática.

Onde os dois números não são de modo algum comparáveis

Os 88,06% do MathForm-8B e as 6,5 milhões de linhas do AlphaProof Code medem coisas diferentes e nunca deveriam ser colocados na mesma coluna. Um é uma taxa de acerto em uma suíte de benchmark criada pelos autores; o outro é uma quantidade de provas produzida para um único alvo. O fornecedor é franco ao dizer que os 88,06% usam uma verificação sintática, que é um critério fraco — uma declaração pode compilar e ainda assim formalizar a afirmação errada, razão pela qual o índice de consistência é 16 pontos menor.

A figura do AlphaProof Code com um sabor comparável é o trabalho de validação: dois bugs do Signal corrigidos anteriormente, um bug de estado fraco e um bug de subgrupo pequeno, foram reintroduzidos em uma cópia isolada, e em ambos os casos o sistema produziu uma prova verificada por máquina de que a versão com bugs falha no teorema de segurança. Isso é um teste negativo, e um teste negativo é exatamente o que falta por completo em um benchmark de autoformalizador. O MathForm-8B não relata nenhum resultado do tipo "dada uma afirmação deliberadamente errada, o modelo disse que sim."

Como você realmente os usaria juntos

Concretamente, e esta é a única parte da comparação com um caminho de curto prazo: use um autoformalizador para elaborar o rascunho, um modelo geral forte para criticar o rascunho e um agente de provas para tentar a prova. Cada etapa tem um modo de falha diferente, e encaminhar as três por uma única chave é a conveniência prática. No OrcaRouter, mais de 200 modelos ficam atrás de uma única API pelo preço de tabela do provedor com 0% de margem, então um loop de elaboração de especificações que envia a mesma afirmação para dois modelos e compara os Lean de ambos é uma chamada de DSL de roteamento em vez de três contratos e três SDKs. O failover automático cobre o caso em que o modelo escolhido está tendo uma tarde ruim.

O que nada disso fornece é a garantia. O MathForm-8B fornece uma afirmação, os modelos fornecem uma crítica, e algo ainda precisa prová-la. Atualmente, o único sistema publicado que fecha esse ciclo em código real implantado é o AlphaProof Code, e ele não está à venda.

A razão para ler os dois artigos em vez de escolher um vencedor

O MathForm-8B é um artefato útil com uma tarefa restrita e um teto de precisão real e medido. O AlphaProof Code é uma demonstração de fluxo de trabalho cuja descoberta mais transferível não é o volume de provas, mas a divisão: o trabalho de especificação pede humanos e um modelo geral forte, o trabalho de prova pede equipes de agentes e um kernel, e a fronteira entre eles é onde reside toda a dificuldade. Qualquer pessoa que esteja construindo um pipeline de verificação deve levar a divisão a sério e tratar a autoformalização como a peça que reduz o custo da primeira etapa — não a peça que a substitui.

O resumo honesto para uma equipe decidindo o que baixar este mês: MathForm-8B, sim, se você trabalha com Lean e quer um auxílio para elaborar rascunhos. AlphaProof Code, leia o repositório de artefatos e o catálogo de desvios de especificação, porque o catálogo lhe diz mais sobre o que a verificação formal de código de produção ainda não consegue alcançar do que qualquer anúncio dirá.