Theo dõi bởi 1M AI News, nhóm LongCat của Meituan đã mở nguồn LongCat-Flash-Prover, một mô hình MoE với 560 tỷ tham số, được thiết kế đặc biệt cho các nhiệm vụ suy luận toán học trên ngôn ngữ chứng minh định lý hình thức Lean4. Trọng số mô hình đã được phát hành theo giấy phép MIT và đã có sẵn trên GitHub, Hugging Face và ModelScope.
Mô hình chia推理 hình thức thành ba khả năng độc lập: hình thức hóa tự động (chuyển đổi bài toán toán học bằng ngôn ngữ tự nhiên thành câu lệnh Lean4), tạo bản phác thảo (tạo khung chứng minh theo phong cách bổ đề) và tạo chứng minh đầy đủ. Cả ba khả năng đều được tích hợp thông qua công cụ Agent với推理 tích hợp (TIR) và tương tác thời gian thực với trình biên dịch Lean4 để xác minh.
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 giới thiệu thuật toán HisPO trong giai đoạn học tăng cường để ổn định việc đào tạo nhiệm vụ dài hạn của mô hình MoE, đồng thời bổ sung cơ chế kiểm tra tính nhất quán và tính hợp lệ của định lý để ngăn chặn reward hacking.
Các bài kiểm tra hiệu năng cho thấy LongCat-Flash-Prover đã thiết lập kỷ lục mới trong cả hai lĩnh vực tự động hình thức hóa và chứng minh định lý trên các mô hình trọng số mã nguồn mở. Trên MiniF2F-Test, nó đạt tỷ lệ vượt qua 97,1% chỉ với 72 lần suy luận, đồng thời đạt 70,8% và 41,5% trên ProverBench và PutnamBench, với không quá 220 lần suy luận cho mỗi bài toán.