1M AI News کی نگرانی کے مطابق، میانگو LongCat ٹیم نے LongCat-Flash-Prover کو اوپن سورس کیا ہے، جو ایک 5600 ارب پیرامیٹر کا MoE ماڈل ہے جو فارمل ثبوت زبان Lean4 کے ریاضیاتی استدلال کے کاموں پر مرکوز ہے۔ ماڈل کے وزن MIT لائسنس کے تحت جاری کیے گئے ہیں اور اب GitHub، Hugging Face اور ModelScope پر دستیاب ہیں۔
ماڈل فارمل ریزوننگ کو تین الگ الگ صلاحیتوں میں تقسیم کرتا ہے: خودکار فارملائزیشن (فطری زبان کے ریاضی کے مسائل کو Lean4 فارمل جملوں میں تبدیل کرنا)، اسکیچ جنریشن (لیما کے انداز میں ثبوت کے فریم ورک کی پیداوار) اور مکمل ثبوت جنریشن۔ تینوں صلاحیتیں Agent ٹولز کے ذریعہ ریزوننگ کو ٹی آئی آر کے ساتھ ادھم کرکے اور Lean4 کمپائلر کے ساتھ ریل ٹائم میں تصدیق کرکے حاصل کی جاتی ہیں۔
ٹریننگ کے حوالے سے، ٹیم نے ہائبرڈ-ایکسپرٹس اٹیریشن فریم ورک کا استعمال کرکے کول اسٹارٹ ڈیٹا تیار کیا اور ری انفورسمنٹ لرننگ کے مراحل میں HisPO الگورتھم شامل کیا تاکہ MoE ماڈل کی لمبی مدتی ٹاسک ٹریننگ کو مستحکم کیا جا سکے، ساتھ ہی ری وارڈ ہیکنگ کو روکنے کے لیے تھیورم کی مطابقت اور قانونی چیک مکینزم شامل کیا گیا۔
بینچ مارکس نے ظاہر کیا کہ LongCat-Flash-Prover نے اوپن سورس وزن ماڈلز میں خودکار فارملائزیشن اور ثبوت کے شعبوں میں SOTA کو نئی سطح پر پہنچایا ہے۔ MiniF2F-Test پر صرف 72 استدلالوں کے ساتھ 97.1% پاس ریٹ حاصل کیا گیا، جبکہ ProverBench اور PutnamBench پر ہر سوال کے لیے 220 استدلالوں سے زیادہ کے بغیر 70.8% اور 41.5% حاصل کیے گئے۔