Navier-Stokes mất đi trong bản dịch: Vì sao việc kiểm chứng Lean đối với autoformalisation của AI không đảm bảo chứng minh ngôn ngữ tự nhiên chính xác

Autoformalisation ngày càng được dùng để kiểm chứng các văn bản toán học, gồm cả văn bản do AI tạo ra, như thông báo của OpenAI về việc chứng minh sự bùng nổ của nghiệm phương trình Navier-Stokes. Trong quá trình này, hệ thống AI dịch văn bản từ ngôn ngữ tự nhiên sang ngôn ngữ hình thức như Lean. Khi dịch xong, lập luận diễn đạt bằng ngôn ngữ hình thức có thể dễ dàng được máy móc kiểm chứng. Mục đích của bài viết này là chỉ ra vì sao quy trình đó có thể không mang lại độ tin cậy đối với lập luận ngôn ngữ tự nhiên ban đầu, do nhiều khó khăn trong việc thực hiện bản dịch chuẩn xác về mặt ngữ nghĩa. Đặc biệt, chúng tôi nhấn mạnh rằng bài toán giải quyết sự mơ hồ trong văn bản ngôn ngữ tự nhiên toán học vốn cần thiết để cung cấp bản dịch chuẩn xác về mặt ngữ nghĩa, lại nằm ở mức độ tùy ý cao trong phân cấp Solvability Complexity Index (SCI) hoặc phân cấp số học (SCI = $\infty$). Do đó, hiểu một cách nôm na, việc cung cấp AI autoformalisation chuẩn xác về mặt ngữ nghĩa còn khó hơn bất kỳ bài toán tính toán nào, kể cả Halting problem (có SCI = 1). Để làm nổi bật tác động của kết quả này, chúng tôi đưa ra một số ví dụ về việc AI dịch sai các nhận định và chứng minh ngôn ngữ tự nhiên sang Lean trong thực tế, dẫn đến sự lệch pha giữa các chứng minh ngôn ngữ tự nhiên và phần kiểm chứng Lean của chúng. Các ví dụ này bao gồm cả bản chứng minh Navier-Stokes do OpenAI công bố. Cụ thể, chúng tôi cho thấy chứng minh Lean được hình thức hóa không khớp với chứng minh ngôn ngữ tự nhiên về sự bùng nổ của nghiệm phương trình Navier-Stokes.