OpenAI tuyên bố mô hình AI thế hệ tiếp theo đã giải quyết 10 vấn đề đẳng cấp thế giới, trong đó bao gồm việc bác bỏ Phỏng đoán Tính cứng Connes (Connes Rigidity Conjecture).
Ngay ngày hôm sau, đã có một bài báo của con người phản hồi: Ví dụ phản chứng do AI đưa ra không hợp lệ.
Tác giả là J. L. Nielsen từ Trung tâm Vật lý Tô pô, Đại học Kansas. Ông đã truy dấu toàn bộ 37.000 dòng mã Lean 4 được OpenAI công bố, ánh xạ từng đối tượng về nguyên mẫu toán học của nó, và cuối cùng đưa ra hai con đường thất bại độc lập.
Quá trình chứng minh cụ thể thì người thường như chúng ta cũng khó hiểu, hãy cứ để AI và các nhà toán học "tiên nhân" đánh nhau.
Nhưng qua sự việc này, có thể thấy việc con người thẩm tra kết quả nghiên cứu khoa học của AI vẫn rất quan trọng.
Phỏng đoán Tính cứng Connes là gì
Phỏng đoán Tính cứng Connes đề cập đến một vấn đề như sau.
Trong toán học, có thể gán cho một nhóm một cấu trúc đại số. Đôi khi hai nhóm trông khác nhau, nhưng cấu trúc gán cho chúng lại hoàn toàn giống nhau.
Connes vào khoảng năm 1980 đã đưa ra phỏng đoán: chỉ cần nhóm đó thỏa mãn hai điều kiện bổ sung, tình huống này sẽ không xảy ra, cấu trúc giống nhau thì nhóm cũng phải giống nhau.
Hai điều kiện bổ sung này, một gọi là ICC, một gọi là tính chất (T) của Kazhdan.
Nói cách khác, muốn phản bác phỏng đoán này, cần đưa ra các nhóm thỏa mãn hai điều kiện nhưng có cấu trúc khác nhau.
Cách làm của mô hình mới OpenAI là xây dựng hai nhóm không đẳng cấu, để chúng sinh ra cùng một đại số, và đưa ra chứng minh rằng cả hai nhóm đều thỏa mãn ICC và tính chất (T).
Toàn bộ lập luận được viết thành 37.000 dòng mã Lean 4, được hạt nhân Lean xác minh từng dòng một, kèm theo một tài liệu hướng dẫn giải thích cách hai nhóm này được xây dựng.
Nielsen chỉ ra: Một trong hai nhóm mà AI xây dựng, trên thực tế không thỏa mãn điều kiện bổ sung, không phải ICC, cũng không có tính chất (T).
Có ba khả năng ở đây:
Tính chất (T) trong mã không tương ứng trung thực với định nghĩa gốc của Kazhdan; hoặc chứng minh chỉ đúng với một phần, nhưng lại bị tính cho toàn bộ nhóm; hoặc nhóm trong mã hoàn toàn không phải là nhóm được mô tả trong tài liệu hướng dẫn.
37.000 dòng, ánh xạ từng dòng
Để kiểm chứng kết luận này, Nielsen còn làm một việc vất vả hơn.
Mã được công bố công khai là một phiên bản đã tích hợp thành tệp đơn, tất cả tên gọi trong mã nguồn phân mô-đun giai đoạn đầu đều biến mất.
Ông ấy đã lập một bảng đối chiếu, đánh dấu từng tên đối tượng toán học trong mã mới cùng số dòng tương ứng:
Nhóm xích đóng trên không ở dòng 13700, nhóm xoắn ở dòng 14069, chứng minh hai đại số đẳng cấu ở dòng 36712, định lý chính ở dòng 36954.
Ông còn truy dấu toàn bộ chuỗi suy luận trong mã chứng minh tính ICC. Chuỗi này bắt đầu từ dòng 31430, truyền lên từng lớp, và cuối cùng tổng hợp thành kết luận ở dòng 31610.
Vấn đề Nielsen chỉ ra là, các bổ đề này xử lý các đối tượng sau khi đã biến đổi đối ngẫu, không phải là nhóm ban đầu có phần tử trung tâm, do đó không trực tiếp bao phủ phần tử then chốt đó.
Việc chúng có đúng với mọi phần tử trong nhóm cụ thể đi vào định lý cuối cùng hay không, phụ thuộc vào cách giao diện giữa hai khối cấu trúc được kết nối.
Điều này cho thấy vấn đề nằm ở "cần chứng minh điều gì", chứ không phải "chứng minh có đúng không". Lean chỉ chịu trách nhiệm xác minh điều sau.
Với nhóm xoắn còn lại, thái độ của Nielsen là thận trọng. Ông nói mình không độc lập xác minh từ mã liệu nó có thỏa mãn ICC hay không, và thừa nhận các bổ đề trong mã có khả năng thực sự đã chứng minh nó thỏa mãn, nhưng điều đó không làm thay đổi kết luận, vì một điều kiện đã không thỏa mãn.
Ông cũng viết hai lập luận phản bác của mình thành mã Lean, biên dịch trên Lean 4.32.2.
Máy kiểm tra hình thức, không phải ý nghĩa
Phần cuối bài báo đặt sự việc này vào một bối cảnh rộng hơn.
Điều mà hạt nhân Lean có thể đảm bảo, chỉ là một đoạn chứng minh về mặt hình thức hoàn toàn chính xác, nhưng không chịu trách nhiệm liệu nó có thực sự chứng minh được kết luận gốc hay không.
Có thể trực tiếp trích dẫn lời của Terence Tao (Đào Triết Hiên): Việc xác minh chứng minh là bản thân phát biểu hình thức, chứ không phải là phát biểu đó tương thích với ý định, vì vậy việc thẩm tra của con người không thể bị thay thế trực tiếp.
Những sự cố loại này đã có ghi chép trong quá khứ.
Một cuộc kiểm toán đối với năm bộ tiêu chuẩn Lean thông dụng đã đưa ra 4833 phát hiện, bao gồm ví dụ phản chứng, định lý rỗng và tiên đề không đáng tin cậy, tất cả đều đã vượt qua xác minh của máy. Cuối cùng chính con người mới xây dựng được ví dụ phản chứng, mới phát hiện ra bản thân câu được chứng minh là sai.
Trong công việc hình thức hóa lý thuyết học thống kê, tình huống nguy hiểm nhất được mô tả là "không phải một chứng minh thất bại, mà là một chứng minh thành công cho một phát biểu sai".
Nghiên cứu về mạng tensor cũng từng ghi nhận hiện tượng tương tự: Hệ thống đưa ra chứng minh hoàn toàn đúng về mặt hình thức, chỉ là mệnh đề nó chứng minh yếu hơn dự kiến.
Nielsen viết, việc hình thức hóa của OpenAI có thể đã thiết lập đúng mọi kết luận mà nó tuyên bố. Nhưng điều nó không thiết lập, và hạt nhân Lean cũng không kiểm tra được, là những kết luận đó có liên quan gì đến lời phát biểu gốc của phỏng đoán hay không.
Con người đọc phỏng đoán sẽ thấy điều kiện tiên quyết, nhưng trợ lý chứng minh nhận được một kết luận không thỏa mãn điều kiện tiên quyết, vẫn sẽ xác minh mọi khẳng định về nó.
Phỏng đoán Tính cứng Connes vẫn còn mở.
Địa chỉ bài báo:
https://philarchive.org/archive/NIEWTCv17
Liên kết tham khảo:
[1]https://openai.com/index/ten-advances-in-mathematics/
[2]https://github.com/openai/ten-proofs/blob/main/ConnesRigidity.lean
Bài viết này đến từ tài khoản công chúng WeChat "Quantum Bit", tác giả: Mộng Thần
