ตามการติดตามของ 1M AI News ทีม LongCat ของ Meituan เปิดตัว LongCat-Flash-Prover ซึ่งเป็นโมเดล MoE ขนาด 560,000 ล้านพารามิเตอร์ ที่ออกแบบมาเฉพาะสำหรับงานการให้เหตุผลทางคณิตศาสตร์ในภาษาพิสูจน์ทางรูปนิยม Lean4 น้ำหนักของโมเดลได้รับการเผยแพร่ภายใต้ใบอนุญาต MIT และได้上线บน GitHub, Hugging Face และ ModelScope
แบบจำลองแยกการให้เหตุผลเชิงรูปนิยมออกเป็นสามความสามารถที่เป็นอิสระ: การแปลงเชิงรูปนิยมอัตโนมัติ (แปลงปัญหาคณิตศาสตร์ภาษาธรรมชาติให้เป็นประโยคใน Lean4), การสร้างร่าง (ผลิตกรอบการพิสูจน์ในรูปแบบเลมมา) และการสร้างการพิสูจน์อย่างสมบูรณ์ ความสามารถทั้งสามนี้ใช้การรวมเครื่องมือตัวแทนเพื่อให้เหตุผลกับคอมไพเลอร์ Lean4 เพื่อตรวจสอบแบบเรียลไทม์
ในด้านการฝึกอบรม ทีมได้เสนอกรอบการทำงาน Hybrid-Experts Iteration เพื่อสร้างข้อมูลสำหรับการเริ่มต้นแบบเย็น และในขั้นตอนการเรียนรู้แบบเสริมแรง ได้นำอัลกอริทึม HisPO มาใช้เพื่อเสถียรภาพการฝึกอบรมงานระยะยาวของโมเดล MoE พร้อมทั้งเพิ่มกลไกการตรวจสอบความสอดคล้องและกฎหมายของทฤษฎีเพื่อป้องกันการหลอกลวงรางวัล
การทดสอบพื้นฐานแสดงว่า LongCat-Flash-Prover ได้ทำลายสถิติ SOTA สองรายการในโมเดลน้ำหนักแบบเปิดแหล่งที่มา ได้แก่ การพิสูจน์เชิงอัตโนมัติและการพิสูจน์ทฤษฎีบท โดยมีอัตราการผ่าน 97.1% บน MiniF2F-Test ด้วยการให้เหตุผลเพียง 72 ครั้ง และได้คะแนน 70.8% และ 41.5% ตามลำดับบน ProverBench และ PutnamBench โดยไม่เกิน 220 ครั้งต่อคำถาม