Giới toán học đang đặt dấu hỏi về mức độ tin cậy của 719 bản thảo toán học do OpenAI sinh ra bằng AI, sau khi một bài báo chỉ ra rằng chứng minh Navier–Stokes mà công ty công bố trước đó không trùng khớp với phiên bản đã được máy tính kiểm tra.
Những điểm chính:
- Danh mục của OpenAI giảm từ 722 xuống 719 bản thảo sau khi công ty rút ba bài vì lỗi dấu.
- Ba nhà toán học tại Anh ghi nhận hai chỗ mà bản chứng minh Navier–Stokes viết trên giấy và mã Lean không khớp nhau.
- Nhóm tác giả không kết luận chứng minh sai, nhưng nhấn mạnh kiểm chứng bằng máy không thể thay thế phản biện chuyên gia.
Đợt công bố toán học của OpenAI
OpenAI công bố bộ sưu tập này ngày 6/10. Một báo cáo công bố hôm thứ Năm cho thấy cách làm của OpenAI lệch khỏi bộ hướng dẫn mà một hội đồng toán học độc lập đưa ra cho các phòng thí nghiệm AI. Danh mục ban đầu có 722 bản thảo; OpenAI đã rút lại ba bản thảo chỉ sau một ngày, sau khi phát hiện một lỗi dấu phá vỡ một lập luận và kéo theo hai bài phụ thuộc vào nó.
Bộ hướng dẫn này, được ban hành ngày 29/9 bởi Nhóm Cố vấn Toán học và Trí tuệ nhân tạo gồm chín thành viên, mở đầu bằng lời kêu gọi các phòng thí nghiệm dừng dùng mô hình độc quyền để thử nghiệm những bài toán toán học nâng cao. Kho lưu trữ của OpenAI cho biết các bản thảo xuất phát từ việc đánh giá một mô hình nội bộ chưa phát hành trên các bài toán nghiên cứu mở.
Phần tóm tắt lập luận của mô hình chỉ xuất hiện kèm 10 kết quả; khoảng 42% kết quả chính đã được hình thức hóa trong Lean, một ngôn ngữ lập trình cho phép máy tính tự kiểm tra chứng minh.
Xem thêm: CEO Anthropic kiếm bao nhiêu? Hồ sơ IPO hé lộ con số
Những lỗ hổng quanh chứng minh Navier–Stokes
Alexander Bastounis (King's College London) cùng Fabian Circelli và Anders Hansen (Đại học Cambridge) đã phân tích chứng minh Navier–Stokes mà OpenAI công bố hồi tháng 9. Họ ghi nhận hai điểm bất nhất giữa lập luận trên bản thảo và mã Lean, trong đó có trường hợp mã Lean chỉ chứng minh được một ước lượng yếu hơn so với khẳng định trong bài báo.
Nhóm tác giả không đưa ra phán quyết về việc chứng minh viết tay là đúng hay sai. Thông điệp của họ hẹp hơn: Lean xác nhận định lý cuối cùng là đúng, nhưng không thể đảm bảo các bước trung gian mà con người đọc được là chuẩn xác; vì thế, những chứng minh kiểu này vẫn cần quy trình phản biện đồng cấp.
Chủ nhân Huy chương Fields Terence Tao viết ngày 6/10 rằng nhiều bài toán đang được “giải” bởi các “người nhắc lệnh AI” (AI prompters) – những người không hiểu đủ đầu ra để trả lời câu hỏi hay thuyết trình về kết quả. Giáo sư Harvard Melanie Matchett Wood, thành viên nhóm cố vấn, cho rằng khi những kết quả như vậy được công bố, “chưa có người nào thực sự hiểu rõ, và giờ mới là lúc công việc thực sự bắt đầu”.
Tranh cãi quanh chứng minh của OpenAI
Nhóm cố vấn khẳng định chỉ cộng đồng toán học rộng lớn mới có thể đánh giá mức độ OpenAI tuân thủ khuyến nghị của họ. Đợt soi xét này diễn ra sau một tháng đầy căng thẳng. OpenAI công bố kết quả Navier–Stokes ngày 8/9, châm ngòi tranh chấp về ghi nhận đóng góp với nhà toán học Tristan Buckmaster (Đại học New York). Ba ngày sau, 25 chủ nhân Huy chương Fields công bố một tuyên bố chung, cảnh báo rằng việc “sản xuất hàng loạt” kết quả toán học bằng AI có thể gây tổn hại cho ngành.
Bài tiếp theo: 722 bài toán AI của OpenAI đã được công khai, giờ đến lượt giới toán học thẩm định
