No avanço contínuo dos grandes modelos rumo a áreas cada vez mais especializadas, a Meituan acaba de apresentar um resultado que chamou a atenção tanto da academia quanto da indústria.
No dia 21 de março, a empresa anunciou oficialmente o código aberto do LongCat-Flash-Prover, um modelo gigantesco focado em provas matemáticas formais. Com impressionantes 567,7 bilhões de parâmetros, ele utiliza a arquitetura MoE (Mixture of Experts), projetada para lidar com problemas matemáticos extremamente complexos com alta precisão.
🚀 Desempenho que impressiona
Nos principais benchmarks que avaliam capacidade de raciocínio lógico, o modelo demonstrou resultados de alto nível:
- Novo recorde: alcançou 97,1% no MiniF2F-Test, utilizando apenas 72 tentativas de inferência.
- Desafio avançado: resolveu 41,5% das questões do PutnamBench, estabelecendo um novo padrão global (SOTA).
Esses números colocam o LongCat-Flash-Prover entre os modelos mais avançados do mundo quando o assunto é raciocínio matemático rigoroso.
🧠 Como o modelo evita “alucinações”
Um dos grandes desafios da IA em matemática é evitar respostas incorretas que parecem plausíveis. Para isso, a Meituan implementou:
- Verificação rigorosa baseada em AST (Árvore de Sintaxe Abstrata)
- Integração com a linguagem formal Lean4, garantindo que cada etapa do raciocínio seja validada
Esse processo reduz drasticamente erros lógicos e elimina respostas “inventadas”.
⚙️ Inovação no treinamento
Treinar modelos desse porte não é simples. Para superar limitações comuns da arquitetura MoE, a equipe desenvolveu:
- Algoritmo HisPO, que melhora a estabilidade em tarefas de longo prazo
- Mecanismo de consistência de teoremas, evitando que o modelo explore “atalhos” durante o aprendizado (problema conhecido como reward hacking)
⚡ Arquitetura poderosa e eficiente
Mesmo com um total de mais de 560 bilhões de parâmetros, o uso do MoE permite que apenas uma parte deles seja ativada em cada tarefa. Isso garante:
- Maior eficiência computacional
- Flexibilidade no raciocínio
- Melhor desempenho em problemas complexos
🌍 Código aberto e impacto global
A Meituan disponibilizou o modelo e seu código tanto no GitHub quanto no Hugging Face, permitindo que pesquisadores e desenvolvedores do mundo inteiro possam explorar e evoluir a tecnologia.
📊 Um passo importante rumo à AGI
Com o lançamento do LongCat-Flash-Prover, fica claro que os modelos chineses estão ganhando força em áreas de raciocínio avançado, como:
- Provas matemáticas formais
- Verificação de código
- Lógica simbólica
Quando problemas que antes exigiam anos de estudo humano começam a ser resolvidos por modelos com bilhões de parâmetros ativos, estamos mais próximos de um marco importante: a inteligência artificial geral (AGI).
Em resumo, não se trata apenas de mais um modelo grande — mas de um avanço significativo na capacidade da IA de pensar com rigor, como um verdadeiro matemático.