Hệ thống chứng minh toán học AlphaProof Nexus của Google DeepMind đã chính thức được đăng trên Science. Tác giả đầu của bài báo là Tsoukalas, toàn bộ nhóm nghiên cứu đều thuộc DeepMind. Công trình này từng được công bố dưới dạng bản thảo tiền in vào cuối tháng 5; lần này là phiên bản tạp chí đã qua bình duyệt đồng cấp.
Bảng thành tích không đổi: hệ thống đã thử sức với 353 bài toán Erdős chưa có lời giải, giải được 9 bài, trong đó 2 bài đã bỏ ngỏ suốt 56 năm; trong 492 giả thuyết mở của cơ sở dữ liệu dãy số nguyên OEIS, nó chứng minh được 44 giả thuyết. Ngoài ra, hệ thống còn trả lời một câu hỏi về hàm Hilbert trong hình học đại số đã treo khoảng 15 năm, và cải thiện một cận đã biết trong bài toán tối ưu min-max.
Một Gemini và một trình biên dịch Lean
Nền tảng của hệ thống là Gemini 3.1 Pro. Mô hình soạn thảo chứng minh bằng ngôn ngữ hình thức Lean; mỗi lần sửa, trình biên dịch Lean lại kiểm tra một lượt, và thông báo lỗi được đưa thẳng trở lại cho vòng thử tiếp theo. Trong cả quá trình, con người chỉ xem kết quả ở bước cuối cùng.
Bài báo tách ra bốn phiên bản:
- Phiên bản A: vòng lặp “sinh – kiểm tra” thuần túy nhất, mô hình lớn viết, trình biên dịch phán xét;
- Phiên bản B: trên nền A, tích hợp AlphaProof, bộ chứng minh trước đây của DeepMind, chuyên bổ sung những đoạn còn thiếu trong chứng minh;
- Phiên bản C: thêm cơ chế tiến hóa, nhiều tác tử con dùng chung một kho bản nháp chứng minh và xếp hạng bằng điểm Elo;
- Phiên bản D: gộp tất cả những thành phần trên, dùng để giải các bài toán Erdős.
Chi tiết đáng suy ngẫm nhất trong kết quả là: phiên bản A cũng tự mình chứng minh được cả 9 bài toán Erdős, chỉ là ở vài bài khó nhất thì tốn nhiều tiền hơn. Chi phí suy luận mà The Decoder dẫn lại là vài trăm USD cho mỗi bài. Nhận định của các tác giả trong bài báo là:
"power of compiler feedback in grounding LLM reasoning"
(Phản hồi từ trình biên dịch giúp neo lập luận của mô hình ngôn ngữ lớn vào thực tế.)
Một số dè dặt từ các học giả Tây Ban Nha
Ngay ngày bài báo lên mạng, Trung tâm Truyền thông Khoa học Tây Ban Nha (SMC) đã mời một số học giả trong nước bình luận, và ý kiến chia làm hai phía.
Nhà nghiên cứu Pablo Haya Coll của UAM cho rằng phương pháp này có thể tạo ra các phát hiện toán học có trọng lượng một cách có hệ thống. Josep Curto của UOC thì đánh giá đây là "a dazzling display of technical capability marred by significant methodological inconsistencies", đại ý là về kỹ thuật thì choáng ngợp nhưng về phương pháp lại có những điểm thiếu nhất quán rõ rệt. Ông nêu ba điểm: phiên bản A và D giải ra cùng một nhóm bài, cho thấy độ phức tạp của khung làm việc chưa chắc quyết định năng lực phát hiện; chi phí chỉ tính các lần chạy thành công, và sổ sách của B và D cũng không tính chi phí suy luận của chính AlphaProof; Lean chỉ bảo đảm chứng minh đúng cho “mệnh đề đã được viết ra”, còn mệnh đề đó có phản ánh trung thực đề bài gốc hay không thì vẫn phải nhờ các nhà toán học kiểm tra thủ công, và bài báo cũng thừa nhận đã từng xảy ra lỗi hình thức hóa.
Giám đốc ICMAT Javier Aramayona lo ngại một điều khác: sẽ xuất hiện hàng loạt kết quả “được biết là đúng nhưng chẳng ai hiểu trọn vẹn”, và khâu thấu hiểu trong nghiên cứu toán học cũng như quá trình đào tạo các nhà nghiên cứu trẻ đều có thể bị suy yếu. Teodoro Calonge của Đại học Valladolid nói thẳng hơn: lĩnh vực này vẫn còn nhiều dư địa cải thiện.
Chính các tác giả cũng nêu rõ phạm vi: tỷ lệ thành công chung của AI trên các bài toán Erdős vào khoảng 1% đến 2%, những bài giải được phần lớn là bài tương đối dễ, tập trung ở các hướng như tổ hợp, tối ưu lồi và lý thuyết số, nơi thư viện Mathlib được tích lũy dày và bài toán dễ chia thành các mục tiêu con. Những bài toán đòi hỏi phải phát minh nhiều lý thuyết mới thì hệ thống gần như không chạm tới được.
Đặt mấy sự kiện trong năm nay cạnh nhau
Hồi tháng 5, chúng tôi đã đưa tin về việc một mô hình của OpenAI chinh phục một giả thuyết Erdős tồn tại 80 năm; sang tháng 9, giữa các nhà toán học và OpenAI lại nổ ra một cuộc tranh cãi về quyền ghi tên tác giả; ngày 6 tháng 10, OpenAI đã đăng một lúc 722 bản thảo toán học do AI tạo ra lên GitHub, dùng kho mã nguồn mở với giấy phép Apache 2.0 chứ không đi qua tạp chí. Theo The Decoder, một nhóm nhà toán học do Terence Tao dẫn đầu sau đó đã kêu gọi tẩy chay cách làm này.
Sự khác biệt giữa hai hướng đi của hai công ty hiện ra rất rõ. OpenAI chọn số lượng lớn, công khai, để cộng đồng tự sàng lọc; DeepMind chọn số lượng ít hơn nhiều, nhưng mỗi kết quả đều đã qua trình biên dịch Lean và qua cả phản biện của tạp chí. Về phần Lean, bài báo của DeepMind cũng định vị khá thận trọng, nguyên văn là hình thức hóa "can serve as a filter for determining which proofs merit human review", tức là dùng để quyết định chứng minh nào xứng đáng để con người bỏ công đọc.
Tính nhẩm một chút: theo mức vài trăm USD mỗi bài, chi phí suy luận cho 9 bài toán Erdős thấp hơn nhiều so với lương một tháng của một nghiên cứu viên sau tiến sĩ; nhưng nếu theo cách tính mà Curto chỉ ra, cộng thêm các lần chạy thất bại và các lượt gọi AlphaProof, con số trên sổ sách sẽ lớn hơn bao nhiêu thì hiện bài báo chưa đưa ra số liệu. DeepMind đã đặt các chứng minh và một phần giải thích trong kho alphaproof-nexus-results trên GitHub, để các nhà toán học bên ngoài có thể đối chiếu từng bài.
Nguồn tham khảo: bài báo trên tạp chí Science, The Decoder, CocoLoop, bình luận của các chuyên gia từ Trung tâm Truyền thông Khoa học Tây Ban Nha; nội dung bài báo đã được đối chiếu về kết quả giải 9 trong 353 bài toán Erdős, chứng minh 44 trong 492 giả thuyết OEIS và phân công của bốn phiên bản tác tử.