وفقًا لمراقبة 1M AI News ، أطلق فريق LongCat في Meituan LongCat-Flash-Prover، وهو نموذج MoE بـ 560 مليار معلمة، مخصص لمهام الاستدلال الرياضي في لغة الإثبات الرسمي Lean4. تم نشر أوزان النموذج بموجب ترخيص MIT، وهو متاح الآن على GitHub وHugging Face وModelScope.
يقوم النموذج بتفكيك الاستدلال الرسمي إلى ثلاث قدرات مستقلة: الترسيم التلقائي (تحويل مشاكل الرياضيات بلغة طبيعية إلى عبارات رسمية بلغة Lean4)، توليد المخطط (إنتاج إطار إثبات على شكل مبرهنات)، وتوليد الإثبات الكامل. يتم تقييم جميع هذه القدرات من خلال دمج أدوات الوكيل مع الاستدلال (TIR) والتفاعل المباشر مع مُجمّع Lean4 للتحقق.
في جانب التدريب، اقترح الفريق إطار عمل Hybrid-Experts Iteration لإنشاء بيانات بدء التشغيل، وأدخل خوارزمية HisPO في مرحلة التعلم المعزز لاستقرار تدريب نموذج MoE على المهام الطويلة، مع إضافة آليات للتحقق من الاتساق والشرعية للنظريات لمنع التلاعب بالمكافآت.
أظهرت الاختبارات المرجعية أن LongCat-Flash-Prover حطّم معايير الأداء الحالية في كل من التشكيل التلقائي وإثبات النظريات ضمن نماذج الأوزان المفتوحة المصدر. فقد حقق معدل نجاح قدره 97.1% على MiniF2F-Test باستخدام 72 استدلالًا فقط، ووصل إلى 70.8% على ProverBench و41.5% على PutnamBench، مع عدم تجاوز عدد الاستدلالات لكل سؤال 220.