Trong nỗ lực ứng dụng AI vào việc tự động chứng minh các định lý toán học phức tạp, OpenAI vừa bị phát hiện đã mắc sai lầm trong quá trình dịch thuật ngữ toán học sang mã máy tính đối với dự án chứng minh phương trình Navier-Stokes. Đây là một trong những bài toán Thiên niên kỷ kinh điển của toán học hiện đại, đòi hỏi tính chính xác tuyệt đối ở từng bước logic.
Cụ thể, sự cố xuất phát từ khâu chuyển đổi các phát biểu và công thức toán học thuần túy sang mã code (như ngôn ngữ chứng minh Lean hoặc Python). Việc câu lệnh mã hóa không phản ánh đúng ngữ nghĩa của công thức gốc đã khiến quy trình kiểm định tính chính xác của bài chứng minh bị lệch hướng. Sai sót này làm dấy lên những nghi vấn về độ tin cậy của các mô hình LLM hiện tại khi đảm nhận vai trò tự động hóa toán học (autoformalization).
Dù các mô hình AI ngày nay thể hiện khả năng lập trình và viết code ấn tượng, việc hiểu sâu ngữ nghĩa toán học và dịch chính xác 100% sang mã máy tính vẫn là bài toán vô cùng hóc húa. Việc thiếu sót các ràng buộc logic nhỏ trong mã nguồn có thể dẫn đến toàn bộ kết quả chứng minh bị đứt gãy hoặc sai lệch hoàn toàn.
Sự cố này là bài học đắt giá cho cộng đồng nghiên cứu AI và các kỹ sư tại Việt Nam khi triển khai AI vào các lĩnh vực đòi hỏi độ chính xác cao. Việc duy trì cơ chế kiểm định từ chuyên gia con người (human-in-the-loop) vẫn là yếu tố bắt buộc trước khi đưa các phát kiến do AI tạo ra vào ứng dụng thực tế.
Nguồn: Hacker News — Biên dịch & tổng hợp: danhbaai.com