Meituan mở nguồn mô hình chứng minh định lý với 560 tỷ tham số, 72 lần suy luận đạt tỷ lệ thành công 97,1%, thiết lập lại SOTA nguồn mở

Tin tức Gate News, ngày 21 tháng 3, nhóm LongCat của Meituan đã mở mã nguồn LongCat-Flash-Prover, một mô hình MoE với 5600 tỷ tham số, tập trung vào nhiệm vụ suy luận toán học trong ngôn ngữ chứng minh định lý hình thức Lean4. Trọng lượng mô hình được phát hành theo giấy phép MIT, đã có mặt trên GitHub, Hugging Face và ModelScope.

Mô hình phân chia suy luận hình thức thành ba khả năng độc lập: tự động hóa hình thức (chuyển đổi vấn đề toán học bằng ngôn ngữ tự nhiên thành câu lệnh hình thức Lean4), tạo phác thảo (sinh khung chứng minh theo phong cách định lý) và sinh chứng minh hoàn chỉnh. Ba khả năng này đều tích hợp qua bộ công cụ Agent để suy luận (TIR) và tương tác xác thực thời gian thực với trình biên dịch Lean4.

Về đào tạo, nhóm đề xuất Khung lặp Hybrid-Experts để tạo dữ liệu khởi động lạnh, đồng thời trong giai đoạn học tăng cường, giới thiệu thuật toán HisPO để ổn định quá trình huấn luyện dài hạn của mô hình MoE, cùng với cơ chế kiểm tra tính nhất quán và hợp lệ của định lý nhằm ngăn chặn hack thưởng.

Các bài kiểm tra tiêu chuẩn cho thấy LongCat-Flash-Prover đã đạt thành tích SOTA trong tự động hóa hình thức và chứng minh định lý trong các mô hình mã nguồn mở. Trên MiniF2F-Test, chỉ cần 72 lần suy luận để đạt tỷ lệ đậu 97.1%, ProverBench và PutnamBench lần lượt đạt 70.8% và 41.5%, mỗi câu hỏi không quá 220 lần suy luận.