DeepSeek đã phát hành một mô hình chuyên dụng trong lĩnh vực chứng minh định lý toán học mang tên Prover-V2, với mục tiêu sử dụng AI để tự động chứng minh các định lý toán học trong hệ thống xác minh hình thức Lean 4.
Tại sao hướng đi này lại quan trọng?
Chứng minh định lý toán học là một bãi thử nghiệm cực hạn cho năng lực của AI. Bởi vì toán học không chấp nhận "gần đúng" – một chứng minh hoặc là hoàn toàn chính xác, hoặc là sai. Không có thứ gọi là "chứng minh đúng 95%".
Các hệ thống xác minh hình thức (như Lean 4) sẽ kiểm tra từng bước suy luận logic giống như trình biên dịch kiểm tra cú pháp. Chỉ cần một bước sai, toàn bộ chứng minh sẽ báo lỗi. Đây là thử thách khắt khe nhất đối với khả năng suy luận logic của AI.
Hiệu suất của Prover-V2
Trên benchmark miniF2F, Prover-V2 đạt được kết quả gần hoặc ngang bằng với kết quả tốt nhất hiện tại. Phương pháp mà nó sử dụng là phân rã mục tiêu con – chia nhỏ một chứng minh phức tạp thành một loạt các mục tiêu con nhỏ hơn, và giải quyết từng cái một.
Điều này rất giống với cách suy nghĩ của các nhà toán học: khi đối mặt với một bài toán khó, trước tiên họ nghĩ "để chứng minh A đúng, tôi cần chứng minh B và C trước, và để chứng minh B thì lại cần xác nhận D…"
Sự khác biệt so với các mô hình suy luận đa năng
Các mô hình đa năng (GPT, Claude, Gemini) thực hiện suy luận toán học dựa trên Chain-of-Thought – về bản chất là "suy luận từng bước bằng ngôn ngữ tự nhiên". Cách này hiệu quả với các bài toán đơn giản, nhưng với các chứng minh phức tạp, rất dễ xuất hiện lỗ hổng logic ở một bước nào đó.
Prover-V2 đi theo hướng hình thức hóa, mỗi bước đều được Lean 4 xác minh. Ưu điểm là không có "ảo giác" (hallucination), nhược điểm là phạm vi ứng dụng rất hẹp – chỉ hoạt động được trong các hệ thống hình thức.
Ý nghĩa
Chứng minh định lý toán học là một hướng đi có vẻ rất ngách nhưng lại có tác động sâu rộng. Nếu AI thực sự có thể chứng minh một cách đáng tin cậy các định lý phức tạp trong hệ thống hình thức, nó có thể được ứng dụng vào xác minh phần mềm, xác minh phần cứng, chứng minh mật mã và một loạt các lĩnh vực quan trọng khác.
Việc DeepSeek đầu tư vào hướng đi này cho thấy họ không chỉ chạy đua benchmark trên các mô hình đa năng lớn – mà còn đang nghiêm túc xây dựng các công cụ khoa học nền tảng.
Nguồn tham khảo: CocoLoop, bài báo Prover-V2 của DeepSeek