OpenAI thu hồi 3 bài báo toán học vì lỗi sai dấu

OpenAI mới đây đã công bố việc thu hồi ba bài báo toán học do phát hiện một lỗi sai dấu trong lập luận cốt lõi. Đây là động thái hiếm thấy, cho thấy quy trình kiểm định nội bộ đang được siết chặt khi các mô hình AI ngày càng tham gia sâu vào nghiên cứu khoa học cơ bản.

Lỗi sai dấu làm sụp đổ cả chuỗi chứng minh

Theo ghi chú lịch sử trên kho lưu trữ GitHub của OpenAI, lỗi xuất hiện trong bài báo "Algebraicity of Weil classes on split abelian eightfolds". Cụ thể, một lỗi sai dấu đã vô hiệu hóa lập luận hủy vết ổn định hóa (stabilization-trace cancellation) — vốn là nền tảng cho toàn bộ cấu trúc chứng minh.

Hệ quả là hai bài báo phụ thuộc cũng không còn giá trị, buộc OpenAI phải thu hồi cả ba:

• Algebraicity of Weil classes on split abelian eightfolds
• Algebraicity of Kuga–Satake Correspondences for K3 Surfaces
• The rational Hodge conjecture for products of K3 surfaces

Các bài báo bị thu hồi hiện mang thông báo giải thích khoảng trống trong lập luận và dẫn liên kết đến bản thảo lưu trữ. Đây là cách xử lý minh bạch, cho phép cộng đồng toán học kiểm tra lại và tránh trích dẫn nhầm.

Sửa lỗi trên diện rộng

Không chỉ dừng ở ba bài báo bị thu hồi, OpenAI còn cho biết đã chỉnh sửa 14 bản thảo khác với nhiều dạng sửa chữa: vá lỗi chứng minh, đính chính phát biểu, làm rõ giả thiết và quan hệ phụ thuộc, cùng một chỉnh sửa cho trích dẫn đã lỗi thời.

Các thay đổi đáng chú ý bao gồm:

• Lipschitz heights và Ashkin–Teller currents (4 bản thảo): vá các lập luận về giao cắt, gắn biên, điều kiện hóa và hội tụ, bổ sung phần chứng minh giao diện thực-Lipschitz.
• Kähler minimal model programs và abundance (6 bản thảo): mở rộng lập luận về tính dương và phép co, làm rõ kết quả nào được dùng làm đầu vào cùng các giả thiết kèm theo.
• Taming và hypersymplectic deformation (2 bản thảo): đính chính khẳng định về đẳng thức nón trong "Taming implies compatibility", thêm ví dụ bao hàm chặt và loại bỏ một phụ thuộc so sánh nón không cần thiết.
• Incompressible Box Transport and Finite Computation: chỉnh sửa các ước lượng chiếu torus và đồng hồ chung.
• Exact Birch–Swinnerton-Dyer Formula from Low Selmer Corank: xóa một trích dẫn mở đầu đã lỗi thời trỏ đến bản thảo hỗ trợ đã bị gỡ.

Ngoài ra, 13 bản thảo khác được cập nhật để trích dẫn phiên bản đã chỉnh sửa của các bài báo đồng hành, kèm theo cập nhật ngày phiên bản.

Hình thức hóa: 42% kết quả chủ chốt đã được kiểm chứng máy

Một điểm đáng chú ý khác là tiến độ hình thức hóa (formalization) — tức chuyển chứng minh toán học sang dạng mà máy tính có thể kiểm chứng từng bước. OpenAI cho biết đã bổ sung 6 công trình hình thức hóa và 5 bổ sung khác liên quan đến kết quả hỗ trợ.

Tổng tỷ lệ các kết quả toán học chủ chốt đã được hình thức hóa hiện đạt 300 / 719 ≈ 42%.

Con số này phản ánh xu hướng đáng chú ý: thay vì chỉ sinh ra chứng minh bằng ngôn ngữ tự nhiên, các hệ thống AI ngày càng hướng tới việc tạo ra chứng minh có thể kiểm chứng bằng máy — một cách tiếp cận giúp giảm thiểu rủi ro sai sót như lỗi sai dấu vừa qua.

Góc nhìn cho Việt Nam

Sự việc này mang lại bài học trực tiếp cho cộng đồng nghiên cứu và các nhóm phát triển AI tại Việt Nam. Khi tích hợp mô hình ngôn ngữ lớn vào công việc học thuật — từ viết báo khoa học, hỗ trợ giảng dạy đến kiểm tra bài tập — việc kiểm chứng độc lập là bắt buộc, không thể bỏ qua.

Các trường đại học và viện nghiên cứu trong nước đang dần ứng dụng AI vào nghiên cứu nên sớm xây dựng quy trình đánh giá chéo (peer review) chặt chẽ, đồng thời chú trọng công cụ hình thức hóa như Lean hay Coq để gia tăng độ tin cậy. Việc một tổ chức hàng đầu như OpenAI công khai thu hồi và sửa lỗi cũng là tấm gương về tính liêm chính học thuật trong thời đại AI.