Ngày 26/10, OpenAI công bố cùng lúc ba kết quả nghiên cứu do mô hình AI của hãng tạo ra, thuộc các lĩnh vực khoa học máy tính lý thuyết, giải tích điều hòa và vật lý toán. Kết quả nặng ký nhất là một chứng minh rằng Giả thuyết Thời gian Mũ (ETH) không đúng. Công ty không nói rõ đã dùng mô hình nào, chỉ gọi là “mô hình AI của OpenAI”, đồng thời cho biết cả ba kết quả đều cần giới học thuật tiếp tục xác nhận độc lập.
ETH: nền móng của hàng trăm bài báo
Giả thuyết Thời gian Mũ nói về độ khó tính toán của bài toán thỏa mãn công thức Boole (3-SAT): nói đại khái, nó khẳng định loại bài toán này không thể giải trong thời gian dưới mũ. Giả thuyết này mạnh hơn và cũng dễ dùng hơn so với “P khác NP”. Suốt nhiều thập kỷ, nó được xem như tiền đề mặc định, và kết luận về cận dưới trong hàng trăm bài báo về lý thuyết đồ thị, sinh học tính toán, cơ sở dữ liệu và hình học tính toán đều được xây dựng trên nó.
Theo mốc thời gian OpenAI công bố, mô hình đã sinh ra chứng minh bằng ngôn ngữ tự nhiên vào ngày 16/10 và hoàn tất việc hình thức hóa bằng Lean vào hôm sau. Tham gia hợp tác có Russell Impagliazzo và Ramamohan Paturi của Đại học California, San Diego, cùng Ryan Williams của Viện Công nghệ Massachusetts (MIT). Hai người đầu chính là những người đề xuất ETH.
Theo thông tin được tiết lộ, các học giả đã đưa ra hai điều kiện với OpenAI: công khai toàn bộ dữ liệu gốc, và tài trợ tổ chức một hội nghị học thuật chuyên thảo luận về tác động của kết quả này đối với khoa học máy tính. OpenAI đồng ý cả hai. Nếu chứng minh đứng vững trước thẩm định, những bài báo lấy ETH làm tiền đề sẽ phải được đánh giá lại từng bài: kết luận nào chỉ là “điều kiện không còn hiệu lực”, kết luận nào có thể cứu được bằng giả thuyết khác, là một khối lượng công việc không nhỏ.
Giả thuyết Kakeya: mạch nghiên cứu quen thuộc với giới học giả Trung Quốc
Kết quả thứ hai là chứng minh giả thuyết làm mượt cục bộ trong mọi số chiều, từ đó suy ra giả thuyết Kakeya và giả thuyết hạn chế Stein trong mọi số chiều. Yếu tố then chốt ở đây là một phương trình đạo hàm riêng bổ trợ do mô hình dựng ra. OpenAI cho biết đã nhận được chứng minh vào ngày 18/10 và hoàn tất hình thức hóa bằng Lean vào ngày hôm sau; cả bản ngôn ngữ tự nhiên lẫn tệp Lean đều đã được đưa lên GitHub.
Mạch nghiên cứu này không xa lạ với độc giả Trung Quốc. Giả thuyết làm mượt cục bộ do Christopher Sogge đề xuất năm 1991; năm 2019, Larry Guth, Hong Wang (Vương Hồng) và Ruixiang Zhang (Trương Duệ Tường) chứng minh trường hợp hai chiều; năm 2025, Hong Wang cùng Joshua Zahl chứng minh giả thuyết Kakeya ba chiều, khi đó được coi là một trong những tiến bộ quan trọng nhất của giải tích điều hòa trong nhiều năm. Bước nhảy từ ba chiều lên mọi số chiều là rất lớn; các nhà toán học bên ngoài đánh giá thế nào thì hiện chưa có phát biểu công khai nào.
Yang–Mills: chỉ có chuyên gia đọc duyệt
Kết quả thứ ba thuộc vật lý toán. Nghiên cứu chứng minh, theo nghĩa toán học chặt chẽ, rằng trong không gian bốn chiều tồn tại một số lý thuyết trường lượng tử tương tác vừa chứa trường chuẩn vừa chứa fermion, bao gồm cả sắc động lực học lượng tử, đồng thời xử lý luôn một bài toán con về sự tồn tại của lý thuyết Yang–Mills thuần túy. Sự tồn tại và khoảng cách khối lượng của lý thuyết Yang–Mills thuần túy là một trong những bài toán Thiên niên kỷ của Viện Toán học Clay.
Phương pháp đi theo hướng lý thuyết trường lượng tử kiến thiết của Tadeusz Balaban. Vì Mô hình Chuẩn không thể được suy trực tiếp xuống các thang khoảng cách ngắn tùy ý, chứng minh nhắm tới lý thuyết thống nhất lớn đơn giản nhất chứa trường chuẩn và fermion của Mô hình Chuẩn. Việc đọc duyệt do người đoạt giải Nobel David Gross dẫn đầu, với sự tham gia của Michael Douglas, Arthur Jaffe, Igor Klebanov và Nikita Nekrasov. Kết quả này chưa được kiểm chứng bằng hình thức hóa.
Từ tháng 5 đến tháng 10
Đặt các lần công bố về toán học của OpenAI trong năm nay cạnh nhau, có thể thấy nhịp độ đang nhanh lên và đối tượng cũng thay đổi. Tháng 5 là một bài toán Erdős đã tồn tại tám mươi năm; tháng 9 là bài toán về tính trơn của phương trình Navier–Stokes, cũng kèm tệp Lean nhưng khi đó chưa có nhà toán học nào hoàn tất kiểm chứng độc lập; lần này là một giả thuyết về độ phức tạp tính toán mà vô số công trình phía sau phụ thuộc vào, và lần đầu tiên chính những người đề xuất giả thuyết đó có tên trong danh sách hợp tác.
Cách thức kiểm chứng cũng phân hóa: hai kết quả toán học có chứng minh Lean mà máy có thể kiểm tra, còn kết quả vật lý chỉ dựa vào con người đọc duyệt. Lean bảo đảm phép suy dẫn không có lỗ hổng, với điều kiện việc phát biểu chính mệnh đề khi hình thức hóa không bị sai lệch. Điểm này vẫn phải chờ các nhóm độc lập đọc kỹ từng dòng của tệp thì mới xác nhận được.
Nguồn tham khảo: thông báo nghiên cứu của OpenAI, CocoLoop, ITHome; các tệp hình thức hóa Lean công khai trên GitHub được dùng để đối chiếu đối tượng chứng minh và cách thức kiểm chứng.