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