Meituan publica el modelo de prueba de teoremas con 560B parámetros de código abierto, con una tasa de éxito del 97.1% en 72 inferencias, estableciendo un nuevo récord SOTA en código abierto.

Noticias de Gate News, 21 de marzo, el equipo LongCat de Meituan ha lanzado de código abierto LongCat-Flash-Prover, un modelo MoE de 5600 millones de parámetros, enfocado en tareas de razonamiento matemático en el lenguaje de prueba formal Lean4. Los pesos del modelo se publican bajo la licencia MIT y ya están disponibles en GitHub, Hugging Face y ModelScope.

Este modelo descompone el razonamiento formal en tres capacidades independientes: formalización automática (convertir problemas matemáticos en lenguaje natural a enunciados formales en Lean4), generación de bocetos (producir marcos de prueba estilo lema) y generación de pruebas completas. Las tres capacidades integran razonamiento mediante el conjunto de herramientas Agent (TIR) y verifican en tiempo real mediante el compilador Lean4.

En cuanto a entrenamiento, el equipo propuso el Marco de Iteración de Expertos Híbridos (Hybrid-Experts Iteration Framework) para generar datos de arranque en frío, e introdujo el algoritmo HisPO en la fase de aprendizaje reforzado para estabilizar el entrenamiento de tareas a largo plazo del modelo MoE, además de incorporar mecanismos de detección de coherencia y legalidad de los teoremas para prevenir el manipuleo de recompensas.

Las pruebas de referencia muestran que LongCat-Flash-Prover establece nuevos estados del arte en formalización automática y prueba de teoremas en modelos de peso abierto. En MiniF2F-Test, alcanza una tasa de éxito del 97.1% con solo 72 inferencias, y en ProverBench y PutnamBench logra un 70.8% y un 41.5% respectivamente, con no más de 220 inferencias por problema.