เมituan เปิดตัวแบบจำลองพิสูจน์ทฤษฎีบทที่มีพารามิเตอร์ 560B อัตราความสำเร็จในการอนุมาน 72 ครั้งอยู่ที่ 97.1% ทำลายสถิติใหม่ในวงการโอเพ่นซอร์ส

ข่าว Gate News เมื่อวันที่ 21 มีนาคม ทีม LongCat ของเมตาเปิดซอร์ส LongCat-Flash-Prover ซึ่งเป็นโมเดล MoE ขนาด 5600 พันล้านพารามิเตอร์ เน้นงานตรรกะทางคณิตศาสตร์ในภาษา Lean4 สำหรับการพิสูจน์ทฤษฎีเชิงฟอร์มาลา โมเดลนี้เผยแพร่ภายใต้สัญญาอนุญาต MIT พร้อมให้ดาวน์โหลดบน GitHub, Hugging Face และ ModelScope

โมเดลนี้แยกการตรรกะเชิงฟอร์มาลาออกเป็นสามความสามารถอิสระ: การตรรกะเชิงฟอร์มาลาอัตโนมัติ (แปลงโจทย์คณิตศาสตร์ภาษาธรรมชาติเป็นประโยคใน Lean4), การสร้างร่าง (สร้างโครงร่างการพิสูจน์ในสไตล์สมมุติฐาน) และการสร้างการพิสูจน์สมบูรณ์ ทั้งสามความสามารถนี้ผนวกกับเครื่องมือ Agent เพื่อรวมการตรรกะ (TIR) และการโต้ตอบแบบเรียลไทม์กับคอมไพเลอร์ Lean4 เพื่อการตรวจสอบ

ด้านการฝึก ทีมได้เสนอกรอบการทำงาน Hybrid-Experts Iteration Framework สำหรับสร้างข้อมูลเริ่มต้น และในช่วงการเรียนรู้เชิงเสริม ได้แนะนำอัลกอริทึม HisPO เพื่อเสถียรภาพของโมเดล MoE ในการฝึกงานระยะยาว พร้อมทั้งเพิ่มกลไกตรวจสอบความสอดคล้องและความถูกต้องของทฤษฎีเพื่อป้องกัน reward hacking

ผลการทดสอบมาตรฐานแสดงว่า LongCat-Flash-Prover ทำลายสถิติในโมเดลเปิดซอร์สด้านการตรรกะเชิงฟอร์มาลาและการพิสูจน์ทฤษฎี โดยใน MiniF2F-Test ใช้เพียง 72 การตรรกะก็ผ่านได้ 97.1% ใน ProverBench และ PutnamBench ทำได้ 70.8% และ 41.5% ตามลำดับ โดยแต่ละโจทย์ใช้การตรรกะไม่เกิน 220 ครั้ง