Một bài báo mới trên arXiv đặt dấu hỏi lớn về cách giới toán học kiểm chứng các chứng minh do AI tạo ra. Nhóm tác giả do Alexander Bastounis dẫn đầu cho rằng việc dùng AI để dịch một chứng minh sang ngôn ngữ Lean rồi để máy kiểm tra có thể không mang lại niềm tin thực sự vào chứng minh gốc.

Autoformalisation là gì?

Autoformalisation là quá trình AI chuyển một lập luận viết bằng ngôn ngữ tự nhiên sang ngôn ngữ hình thức như Lean. Khi đã dịch xong, máy tính kiểm tra từng bước rất nhanh và chính xác. Cách này được dùng để xác minh cả những chứng minh do AI viết, trong đó có chứng minh mà OpenAI công bố về hiện tượng nghiệm "nổ" của phương trình Navier-Stokes, một trong những bài toán nổi tiếng nhất của toán học.

Vấn đề nằm ở khâu dịch

Hãy hình dung bạn nhờ người dịch một hợp đồng, rồi thuê luật sư kiểm tra bản dịch. Nếu bản dịch sai ý, bản dịch có thể hoàn toàn "hợp lệ" nhưng không còn là hợp đồng ban đầu. Tương tự, Lean chỉ xác nhận bản dịch đúng logic, không xác nhận nó trung thành với bản gốc. Các tác giả chỉ ra nhiều ví dụ AI dịch sai, và cho thấy bản Lean của chứng minh Navier-Stokes không khớp với chứng minh gốc.

Ý nghĩa với người dùng

Bài học rõ ràng: dấu "đã xác minh" không đồng nghĩa với "đúng". Khi AI ngày càng tham gia nghiên cứu công nghệ và khoa học, con người vẫn cần đọc kỹ và kiểm chứng độc lập.