Kiểm chứng Lean không đảm bảo tính đúng đắn của chứng minh toán học bằng ngôn ngữ tự nhiên

Trong làn sóng ứng dụng trí tuệ nhân tạo vào toán học, một câu hỏi tưởng chừng đã có lời giải lại đang bị đặt dấu hỏi: liệu một chứng minh toán học đã được máy kiểm chứng thành công có thực sự đúng như bản gốc mà con người viết ra?

Một bài báo mới trên arXiv của các tác giả Alexander Bastounis, Fabian Circelli và Anders C. Hansen lập luận rằng câu trả lời là không, và đưa ra bằng chứng cả về mặt lý thuyết lẫn thực tiễn.

Autoformalisation là gì và tại sao nó nguy hiểm?

Autoformalisation (tạm dịch: tự động hình thức hóa) là quá trình dùng AI để chuyển một văn bản toán học viết bằng ngôn ngữ tự nhiên sang một ngôn ngữ hình thức như Lean. Sau khi dịch xong, lập luận trong ngôn ngữ hình thức có thể được máy tính kiểm chứng một cách cơ học, nhanh chóng và chính xác.

Nghe có vẻ hoàn hảo. Nhưng vấn đề nằm ở bước dịch.

Nếu bước dịch từ ngôn ngữ tự nhiên sang Lean không trung thành về mặt ngữ nghĩa, thì việc Lean xác nhận "chứng minh hợp lệ" chẳng nói lên điều gì về chứng minh gốc.

Nói cách khác, máy chỉ kiểm chứng được thứ mà nó được đưa vào — chứ không kiểm chứng được rằng thứ đó có đúng là bản dịch trung thực của lập luận ban đầu hay không.

Nỗi khó nằm ở bậc vô hạn của hệ thống phân cấp SCI

Điểm đáng chú ý nhất của bài báo là kết quả lý thuyết: việc giải quyết sự mơ hồ trong văn bản toán học ngôn ngữ tự nhiên — điều kiện bắt buộc để có một bản dịch trung thành về ngữ nghĩa — nằm ở bậc vô hạn trong hệ thống phân cấp Solvability Complexity Index (SCI).

Để so sánh:

• Bài toán Turing dừng (Halting problem) có SCI = 1
• Giải quyết mơ hồ ngôn ngữ toán học có SCI = ∞

Nói một cách dễ hiểu: cung cấp autoformalisation trung thành về ngữ nghĩa khó hơn mọi bài toán tính toán, kể cả bài toán nổi tiếng bất khả thi là bài toán dừng.

Đây không phải một hạn chế tạm thời của công nghệ hiện tại — đó là một giới hạn mang tính lý thuyết, có nghĩa là dù AI có mạnh đến đâu, việc dịch trung thành tuyệt đối vẫn là điều không thể đảm bảo.

Những sai lệch thực tế đã xảy ra

Nhóm tác giả không chỉ dừng ở lý thuyết. Họ cung cấp nhiều ví dụ thực tế về việc AI dịch sai các phát biểu và chứng minh từ ngôn ngữ tự nhiên sang Lean, dẫn tới sự không khớp giữa chứng minh gốc và phần "kiểm chứng" của Lean.

Đáng chú ý nhất là trường hợp chứng minh blow-up của nghiệm phương trình Navier-Stokes mà OpenAI từng công bố. Theo phân tích của nhóm tác giả:

• Chứng minh Lean đã được hình thức hóa không tương ứng với chứng minh blow-up bằng ngôn ngữ tự nhiên
• Nói cách khác, Lean xác nhận một điều gì đó — nhưng không phải điều mà bài toán gốc muốn chứng minh

Đây là một cảnh báo nghiêm túc đối với cộng đồng toán học và AI, bởi các tuyên bố về "chứng minh đã được máy kiểm chứng" thường được truyền thông đón nhận như một dấu chứng nhận chất lượng tuyệt đối.

Ý nghĩa đối với cộng đồng nghiên cứu

Bài báo gửi đi ba thông điệp chính:

• Kiểm chứng hình thức không thay thế được đánh giá của con người. Việc Lean chấp nhận một chứng minh không đồng nghĩa với việc chứng minh đó đúng về mặt toán học trong ngữ cảnh gốc.
• Cần thận trọng với các tuyên bố "đã được xác minh bằng máy". Cụm từ này có thể gây hiểu lầm nếu bỏ qua bước dịch trung gian.
• Các bài toán lớn như Navier-Stokes vẫn cần cộng đồng kiểm chứng độc lập, không thể chỉ dựa vào một pipeline autoformalisation tự động.

Với các nhà nghiên cứu AI và toán học tại Việt Nam đang theo dõi làn sóng ứng dụng mô hình ngôn ngữ lớn vào chứng minh định lý, bài báo này là một lời nhắc nhở quan trọng: tự động hóa kiểm chứng không đồng nghĩa với tự động hóa chân lý.

Bài báo được đăng trên arXiv với mã arXiv:2610.08144, thuộc chuyên mục Analysis of PDEs (math.AP), đồng thời liên quan tới Artificial Intelligence (cs.AI) và Logic (math.LO).