DeepSeek phát hành DeepSeek-Prover-V2 với tính năng tìm kiếm chứng minh đệ quy và chuẩn mới ProverBench

DeepSeek AI công bố DeepSeek-Prover-V2, một mô hình ngôn ngữ lớn mã nguồn mở dành cho chứng minh định lý hình thức trong Lean 4. Mô hình này sử dụng quy trình chứng minh định lý đệ quy, tận dụng DeepSeek-V3 để tạo dữ liệu khởi tạo chất lượng cao bằng cách phân rã các định lý phức tạp thành các mục tiêu con và hình thức hóa chúng. Một mô hình 7 tỷ tham số sau đó chứng minh các mục tiêu con này, và các chứng minh hoàn chỉnh được ghép cặp với suy luận chuỗi tư duy của DeepSeek-V3 để huấn luyện. Học tăng cường với phản hồi nhị phân tiếp tục tinh chỉnh mô hình. Phiên bản 671 tỷ tham số đạt 88,9% trên MiniF2F-test và giải được 49 trong số 658 bài toán PutnamBench. DeepSeek cũng giới thiệu ProverBench, một bộ dữ liệu gồm 325 bài toán từ các kỳ thi AIME và sách giáo khoa để đánh giá suy luận toán học. Mô hình có sẵn ở hai kích thước: 7 tỷ và 671 tỷ tham số.