1M AI News এর মনিটরিং অনুযায়ী, মেইটুয়ান LongCat টিম একটি 5600 বিলিয়ন প্যারামিটার বিশিষ্ট MoE মডেল LongCat-Flash-Prover ওপেন-সোর্স করেছে, যা ফর্মাল থিওরেম প্রুফ ভাষা Lean4-এর গাণিতিক যুক্তি কাজের জন্য বিশেষায়িত। মডেলেরওয়েটস MIT লাইসেন্সের অধীনে প্রকাশিত হয়েছে এবং GitHub, Hugging Face এবং ModelScope-এ আপলোড করা হয়েছে।
মডেলটি ফর্মাল যুক্তিকে তিনটি স্বতন্ত্র ক্ষমতায় বিভক্ত করে: অটোমেটিক ফর্মালাইজেশন (প্রাকৃতিক ভাষার গাণিতিক সমস্যাকে Lean4 ফর্মাল বিবৃতিতে রূপান্তর করা), স্কেচ জেনারেশন (লেমা-স্টাইলের প্রমাণ কাঠামো তৈরি করা) এবং পূর্ণাঙ্গ প্রমাণ জেনারেশন। তিনটি ক্ষমতা সম্পূর্ণরূপে Agent টুল ইন্টিগ্রেটেড রিজনিং (TIR) এবং Lean4 কম্পাইলারের সাথে রিয়েল-টাইম ইন্টারঅ্যাকশনের মাধ্যমে যাচাইকৃত।
ট্রেনিংয়ের ক্ষেত্রে, দল Hybrid-Experts Iteration Framework ব্যবহার করে কুল-স্টার্ট ডেটা তৈরি করে এবং রিইনফোর্সমেন্ট লার্নিং পর্যায়ে HisPO অ্যালগরিদম চালু করে MoE মডেলের দীর্ঘ-পরিসরের টাস্ক ট্রেনিংকে স্থিতিশীল করে, একইসাথে রিওয়ার্ড হ্যাকিং প্রতিরোধের জন্য থিওরেম সামঞ্জস্যতা এবং বৈধতা পরীক্ষার মেকানিজম যোগ করা হয়।
বেঞ্চমার্ক দেখায় যে LongCat-Flash-Prover ওপেন-সোর্স ওয়েট মডেলগুলিতে অটোমেটেড ফর্মালাইজেশন এবং থিওরেম প্রুভিং উভয়ের জন্য SOTA রেকর্ড ভাঙল। MiniF2F-Test-এ শুধুমাত্র 72টি ইনফারেন্স ব্যবহার করে 97.1% পাস রেট অর্জন করা হয়েছে, যখন ProverBench এবং PutnamBench-এ যথাক্রমে 70.8% এবং 41.5% অর্জন করা হয়েছে, প্রতিটি প্রশ্নের জন্য 220টিরও কম ইনফারেন্স ব্যবহার করে।