De acordo com o 1M AI News, a equipe LongCat da Meituan lançou o LongCat-Flash-Prover, um modelo MoE com 560 bilhões de parâmetros, projetado especificamente para tarefas de raciocínio matemático na linguagem de prova formal Lean4. Os pesos do modelo foram liberados sob a licença MIT e já estão disponíveis no GitHub, Hugging Face e ModelScope.
O modelo divide o raciocínio formalizado em três habilidades independentes: formalização automática (converter problemas matemáticos em linguagem natural para declarações em Lean4), geração de esboço (produzir estruturas de prova no estilo lema) e geração de prova completa. Todas as três habilidades são verificadas em tempo real por meio da interação com o compilador Lean4, integrada por meio da Inferência com Ferramentas de Agente (TIR).
Em termos de treinamento, a equipe propôs o Hybrid-Experts Iteration Framework para gerar dados de inicialização a frio e introduziu o algoritmo HisPO na fase de aprendizado por reforço para estabilizar o treinamento de tarefas de longo prazo do modelo MoE, além de incorporar mecanismos de verificação de consistência e legalidade de teoremas para prevenir reward hacking.
Os testes de referência mostram que o LongCat-Flash-Prover estabeleceu novos recordes SOTA em formalização automática e prova de teoremas entre modelos com pesos abertos. Alcançou uma taxa de aprovação de 97,1% no MiniF2F-Test com apenas 72 inferências, e 70,8% e 41,5% no ProverBench e PutnamBench, respectivamente, com no máximo 220 inferências por problema.