OpenAI công bố 722 bản thảo toán học từ mô hình AI chưa phát hành, nhưng chỉ 162 bản (khoảng 22%) được Lean kiểm chứng, khiến giới toán học đòi bằng chứng độc lập.
OpenAI hôm thứ Ba đã đăng tải 722 bản thảo toán học trên GitHub, tất cả do một mô hình nội bộ chưa phát hành tạo ra. Theo người phát ngôn của công ty, gần như toàn bộ kết quả xuất phát từ một câu lệnh duy nhất giao cho một tác nhân AI duy nhất, dù một số trường hợp phải thử nhiều lần. Nếu được xác nhận, đây có thể là bước đột phá đáng kể của AI trong nghiên cứu toán học, nhưng tuyên bố này đang vấp phải sự hoài nghi đáng kể từ giới chuyên môn.
Con số 722 cần được hiểu đúng bản chất. Các bản thảo được chia thành 372 “họ” kết quả liên quan, mỗi họ có thể gồm một định lý chính cùng các lập luận bổ trợ, hệ quả hoặc cách chứng minh thay thế, nên đây là số bản thảo chứ không phải số bài toán đã giải.
OpenAI cho biết đã giao khoảng 4.000 bài toán cho mô hình và chỉ giữ lại những kết quả được công ty đánh giá là đủ quan trọng để công bố. Mỗi kết quả tiêu tốn trung bình lượng tài nguyên tính toán tương đương khoảng ba giờ suy luận của ChatGPT Pro, thấp hơn nhiều so với tuyên bố về bài toán Navier–Stokes hồi tháng trước, vốn dùng 10.000 tác nhân phối hợp trong 88 giờ.
Khoảng cách giữa tuyên bố và khả năng kiểm chứng
Điểm gây tranh cãi lớn nhất là mức độ kiểm chứng. Theo danh mục hình thức hóa trong kho mã nguồn, chỉ 162 trong 722 bài báo có kết quả chính được chuyển sang Lean, phần mềm kiểm tra cơ học từng bước logic, tương đương khoảng 22% tập tài liệu. Chính OpenAI thừa nhận một số kết quả chưa được hình thức hóa có thể tồn tại vấn đề. Ngay cả với các bản đã qua Lean, việc kiểm tra chỉ xác nhận chứng minh khớp với mệnh đề như được biểu diễn trong Lean, chứ không bảo đảm mệnh đề ấy phản ánh đúng bài toán gốc, cũng không cho biết kết quả có mới hay có ý nghĩa hay không. Đó là phần việc các nhà toán học vẫn phải đảm nhận.
Andrew Sutherland, nhà toán học tại Viện Công nghệ Massachusetts (MIT), nói với Scientific American rằng mọi tuyên bố về một tác nhân giải bài toán ngay trong một lần thử nên được xem là chưa kiểm chứng cho đến khi mô hình được công bố và người khác có thể tái lập kết quả. Viện Nghiên cứu Cao cấp tại Princeton cũng cảnh báo AI đã có thể tạo ra lập luận mà chính người ra lệnh không thể hiểu, kiểm chứng hay chịu trách nhiệm, đồng thời nhấn mạnh hiểu biết của con người phải là một phần của hoạt động công bố học thuật có trách nhiệm.
Ở chiều ngược lại, Giáo sư Abhishek Saha gọi đây là “một ngày rất quan trọng đối với toán học”, dù lưu ý phần lớn kết quả thuộc nhóm tiến bộ vượt bậc trong các chương trình nghiên cứu sẵn có hoặc những đột phá bất ngờ, chứ chưa phải các bài toán có thể thay đổi cả lĩnh vực. Trong 722 bản thảo, chỉ một bản đụng tới nhóm Bài toán Thiên niên kỷ: Giả thuyết Quasi-Riemann.
Mức độ minh bạch cũng là điểm bị chỉ trích. Đợt công bố chưa đáp ứng đề xuất ngày 29/9 của nhóm cố vấn tại Viện Nghiên cứu Cao cấp về tên mô hình, các câu lệnh, bản tóm tắt chuỗi suy luận, thời gian thực hiện và chi phí tính toán từng kết quả. OpenAI mới công bố số liệu trung bình và 10 bản tóm tắt suy luận, chưa công khai câu lệnh, và cho biết vẫn đang chuẩn bị phát hành mô hình một cách có trách nhiệm. Daniel Litt, nhà toán học tại Đại học Toronto, cho rằng không có lý do gì để giữ kín các câu trả lời cho những bài toán này.
Trong khi đó, Anthropic chọn cách tiếp cận khác: tháng trước, hãng công khai toàn bộ 13 triệu dòng chứng minh Định lý cuối cùng của Fermat đã được Lean kiểm chứng, dù đó là hình thức hóa kết quả Andrew Wiles công bố năm 1995 chứ không phải kết quả mới. OpenAI cho biết sẽ tiếp tục bổ sung các bản hình thức hóa khi hoàn thành.
