A Meituan lançou um modelo de prova de teoremas com 560 bilhões de parâmetros de código aberto, atingindo uma taxa de sucesso de 97,1% em 72 inferências, superando o estado da arte de código aberto.

Notícias Gate, 21 de março, a equipa LongCat da Meituan lançou open source o LongCat-Flash-Prover, um modelo MoE com 5600 bilhões de parâmetros, focado em tarefas de raciocínio matemático na linguagem de prova formal Lean4. Os pesos do modelo foram publicados sob licença MIT e já estão disponíveis no GitHub, Hugging Face e ModelScope.

Este modelo divide o raciocínio formal em três capacidades independentes: raciocínio formal automático (conversão de problemas matemáticos em linguagem natural para declarações formais em Lean4), geração de esboços (produção de estruturas de prova ao estilo de lemas) e geração de provas completas. Todas as capacidades integram raciocínio através do conjunto de ferramentas Agent (TIR) com interação em tempo real com o compilador Lean4.

Na fase de treino, a equipa propôs o Hybrid-Experts Iteration Framework para gerar dados de arranque frio, e na fase de aprendizagem por reforço introduziu o algoritmo HisPO para estabilizar o treino de tarefas de longo prazo do modelo MoE, além de incluir mecanismos de deteção de consistência e legalidade de teoremas para evitar manipulação de recompensas.

Testes de referência mostram que o LongCat-Flash-Prover supera o estado da arte em raciocínio formal automático e prova de teoremas entre modelos de código aberto. No MiniF2F-Test, alcançou uma taxa de sucesso de 97,1% com apenas 72 tentativas de raciocínio, enquanto no ProverBench e PutnamBench atingiu 70,8% e 41,5%, respetivamente, com o máximo de 220 tentativas por questão.