OpenAI rút lại ba kết quả toán học trên kho GitHub chính thức

OpenAI vừa công bố bản cập nhật mới nhất cho kho lưu trữ toán học của mình trên GitHub, trong đó có 6 bản hình thức hóa mới bằng Lean, 19 chỉnh sửa và đặc biệt là 3 kết quả bị rút lại. Đây là động thái hiếm thấy cho thấy ngay cả những kết quả được công bố bởi các phòng thí nghiệm AI hàng đầu cũng cần được kiểm chứng lại một cách nghiêm ngặt.

Dan Roberts thông báo cập nhật kho toán học của OpenAI

Chuyện gì đã xảy ra?

Theo chia sẻ từ Dan Roberts — người đảm nhận vai trò cập nhật kho lưu trữ — OpenAI đã bổ sung 6 bản hình thức hóa Lean mới, thực hiện 19 chỉnh sửa và rút lại 3 kết quả khỏi kho lưu trữ toán học của mình. Hiện tại, kho này đã hình thức hóa được khoảng 42% các kết quả chủ chốt (top-line results).

Điều đáng chú ý là việc rút lại kết quả không phải là chuyện hiếm trong giới toán học, nhưng việc một phòng thí nghiệm AI công khai thừa nhận và gỡ bỏ kết quả của chính mình lại là tín hiệu tích cực về tính minh bạch.

"Chúng tôi sẽ tiếp tục cập nhật kho lưu trữ với các hình thức hóa mới và bất kỳ lỗi nào chúng tôi phát hiện."

Lean là gì và tại sao quan trọng?

Lean là một trợ lý chứng minh (proof assistant) và ngôn ngữ lập trình hàm, cho phép các nhà toán học viết chứng minh theo cách mà máy tính có thể kiểm chứng tự động. Mỗi định lý được hình thức hóa trong Lean đều phải tuân theo các quy tắc logic chặt chẽ, không có chỗ cho sai sót chủ quan của con người.

Việc các công ty AI như OpenAI đầu tư vào hình thức hóa toán học có ý nghĩa chiến lược:

• Kiểm chứng đầu ra của AI: Khi mô hình ngôn ngữ lớn đưa ra các bước lập luận toán học, Lean có thể xác minh chúng có đúng hay không.
• Tạo dữ liệu huấn luyện chất lượng cao: Các chứng minh đã được kiểm chứng là nguồn dữ liệu vàng để huấn luyện AI suy luận.
• Thúc đẩy nghiên cứu toán học: Hình thức hóa giúp phát hiện lỗi logic mà con người có thể bỏ sót.

Kho lưu trữ toán học của OpenAI trên GitHub

Ba kết quả bị rút lại nói lên điều gì?

Việc rút lại kết quả là một phần tất yếu của quy trình khoa học nghiêm túc. Trong toán học truyền thống, các bài báo bị rút lại thường xảy ra khi phát hiện lỗi trong chứng minh. Với hình thức hóa Lean, quá trình này có phần khác biệt:

• Lỗi có thể đến từ việc định nghĩa chưa chính xác trong mã nguồn Lean.
• Đôi khi kết quả đúng về mặt logic nhưng không phản ánh đúng định lý gốc cần chứng minh.
• Một số trường hợp là do phát hiện vấn đề về giả thiết của định lý.

Con số 42% kết quả đã hình thức hóa cũng cho thấy khối lượng công việc còn lại khá lớn. Việc hình thức hóa toán học là quá trình tốn thời gian, đòi hỏi cả chuyên môn toán học lẫn kỹ năng lập trình Lean.

Ý nghĩa với cộng đồng công nghệ Việt Nam

Với các nhà phát triển và nghiên cứu AI tại Việt Nam, câu chuyện này mang lại vài bài học đáng lưu ý:

• Minh bạch là yếu tố then chốt: Việc công khai rút lại kết quả giúp cộng đồng tránh xây dựng nghiên cứu dựa trên nền tảng sai.
• Kiểm chứng tự động ngày càng quan trọng: Khi AI tham gia vào nghiên cứu khoa học, các công cụ như Lean sẽ trở thành chuẩn mực.
• Cơ hội học tập: Kho lưu trữ mở của OpenAI là nguồn tài liệu quý cho sinh viên và nhà nghiên cứu muốn tìm hiểu về hình thức hóa toán học.

Trong bối cảnh các mô hình AI ngày càng được ứng dụng vào lập luận toán học và khoa học, việc duy trì tính chính xác và minh bạch sẽ là yếu tố quyết định để cộng đồng tin tưởng vào kết quả do AI tạo ra.