Nhà toán học bác bỏ bước đột phá giả thuyết của OpenAI trong vòng 24 giờ: 'AI chứng minh từng câu, nhưng không còn liên quan đến giả thuyết ban đầu'

OpenAI tuyên bố rằng mô hình AI thế hệ mới của họ đã giải được mười bài toán toán học đẳng cấp thế giới, bao gồm việc bác bỏ giả thuyết cứng nhắc Connes. Ngay hôm sau, một nhà toán học con người đã đáp lại bằng một bài báo lập luận rằng phản ví dụ của AI là không hợp lệ. Tác giả, J. L. Nielsen từ Trung tâm Vật lý Tôpô tại Đại học Kansas, đã theo dõi 37.000 dòng mã Lean 4 của OpenAI từ đầu đến cuối, ánh xạ từng đối tượng trở lại nguyên mẫu toán học của nó, và xác định hai con đường thất bại độc lập. Giả thuyết cứng nhắc Connes phát biểu rằng nếu hai nhóm có cùng cấu trúc đại số liên kết và thỏa mãn hai điều kiện bổ sung (ICC và tính chất (T) của Kazhdan), thì các nhóm đó phải đẳng cấu. Mô hình của OpenAI đã xây dựng hai nhóm không đẳng cấu tạo ra cùng một đại số, với các chứng minh rằng cả hai nhóm đều thỏa mãn ICC và tính chất (T). Nielsen chỉ ra rằng một trong các nhóm do AI xây dựng thực tế không thỏa mãn các điều kiện bổ sung, vừa không có ICC vừa không có tính chất (T). Cô liệt kê ba lý do có thể: biểu diễn của mã về tính chất (T) không tương ứng trung thực với định nghĩa gốc của Kazhdan; chứng minh chỉ đúng cho một phần của nhóm nhưng lại được áp dụng cho toàn bộ; hoặc nhóm trong mã không phải là những gì tài liệu giải thích mô tả. Nielsen cũng thực hiện kiểm tra từng dòng mã, liệt kê tên của từng đối tượng toán học và số dòng trong một bảng tham chiếu chéo. Cô phát hiện ra rằng các bổ đề dùng để chứng minh ICC áp dụng cho các đối tượng sau một phép biến đổi đối ngẫu, không phải cho nhóm ban đầu với các phần tử trung tâm của nó, vì vậy chúng không trực tiếp bao phủ các phần tử quan trọng. Cô viết hai lời bác bỏ của mình dưới dạng mã Lean và biên dịch chúng bằng Lean 4.32.2. Phần cuối của bài báo thảo luận về bối cảnh rộng hơn: hạt nhân Lean đảm bảo tính đúng đắn về mặt hình thức, nhưng không đảm bảo liệu phát biểu có thực sự chứng minh kết luận dự kiến hay không. Trích dẫn Terence Tao, việc xác minh một chứng minh kiểm tra phát biểu hình thức, không kiểm tra sự phù hợp của nó với ý định, vì vậy không thể thay thế việc đánh giá của con người. Các cuộc kiểm toán trước đây về năm điểm chuẩn Lean phổ biến đã tìm thấy 4.833 vấn đề, bao gồm phản ví dụ, định lý rỗng và tiên đề không đáng tin cậy, tất cả đều được máy xác minh, sau đó con người xây dựng phản ví dụ để chỉ ra các phát biểu được chứng minh là sai. Nielsen viết rằng việc hình thức hóa của OpenAI có thể đã thiết lập chính xác mọi kết luận mà nó tuyên bố, nhưng điều nó không thiết lập—và điều hạt nhân Lean không thể kiểm tra—là liệu các kết luận này có liên quan đến cách diễn đạt của giả thuyết ban đầu hay không. Giả thuyết cứng nhắc Connes vẫn còn bỏ ngỏ.