Según el monitoreo de 1M AI News , el equipo LongCat de Meituan ha lanzado como código abierto LongCat-Flash-Prover, un modelo MoE de 560 mil millones de parámetros diseñado específicamente para tareas de razonamiento matemático en el lenguaje de demostración formal Lean4. Los pesos del modelo se han publicado bajo la licencia MIT y ya están disponibles en GitHub, Hugging Face y ModelScope.
El modelo descompone el razonamiento formal en tres capacidades independientes: formalización automática (convertir problemas matemáticos en lenguaje natural a declaraciones en Lean4), generación de esquemas (producir marcos de prueba estilo lema) y generación de pruebas completas. Las tres capacidades se validan en tiempo real mediante la interacción con el compilador Lean4 a través de la integración de herramientas de razonamiento del agente (TIR).
En cuanto al entrenamiento, el equipo propuso el marco Hybrid-Experts Iteration para generar datos de arranque en frío, e introdujo el algoritmo HisPO en la fase de aprendizaje por refuerzo para estabilizar el entrenamiento a largo plazo del modelo MoE, además de incorporar mecanismos de verificación de consistencia y legalidad de teoremas para prevenir el reward hacking.
Las pruebas de referencia muestran que LongCat-Flash-Prover ha establecido nuevos récords SOTA en formalización automática y demostración de teoremas entre modelos con pesos abiertos. Alcanza una tasa de aprobación del 97,1% en MiniF2F-Test con solo 72 inferencias, y obtiene 70,8% en ProverBench y 41,5% en PutnamBench, con un máximo de 220 inferencias por problema.