OpenAI công bố chứng minh phương trình Navier-Stokes kèm xác thực hình thức bằng Lean 4

Hôm qua, OpenAI đã công bố một bằng chứng giải quyết được câu hỏi tồn tại từ lâu về phương trình Navier-Stokes trong lĩnh vực động lực học chất lưu. Thông báo này đã tạo nên một làn sóng xôn xao như dự đoán. Tuy nhiên, có một khía cạnh trong công trình của OpenAI mà tôi chưa thấy ai đề cập đến: họ đã đăng tải một bản chứng minh hình thức bằng Lean 4 cùng lúc với bản chứng minh thông thường dành cho con người.

Khá nhiều giả thuyết toán học khác gần đây đã được giải quyết bằng AI, và chúng cũng đi kèm với các bản chứng minh hình thức, đặc biệt là sử dụng Lean 4.

Cho đến tận gần đây, việc tạo ra các bản chứng minh hình thức có thể kiểm chứng bằng máy vẫn là một công việc vô cùng tẻ nhạt. Vào năm 2005, Henk Barendregt và Freek Wiedijk đã viết:

Để cho thấy khối lượng công việc cần thiết cho việc hình thức hóa, chúng tôi ước tính rằng cần khoảng một tuần làm việc (năm ngày làm việc, mỗi ngày tám giờ) để hình thức hóa một trang trong sách giáo khoa toán bậc đại học.

Đó là quy tắc chung: bốn mươi giờ cho một trang. Và điều này nằm trong bối cảnh của sách giáo khoa đại học. Các ấn phẩm nghiên cứu có nội dung cô đọng hơn nhiều so với sách giáo khoa. Hơn nữa, trang 100 của một cuốn sách giáo khoa có lẽ chủ yếu phụ thuộc vào nội dung từ trang 1 đến trang 99. Trong khi đó, một câu trong bài báo nghiên cứu có thể trích dẫn bất cứ thứ gì đã được công bố trước đó.

Giả sử một bài báo nghiên cứu tốn công sức hình thức hóa gấp 20 lần so với một trang trong sách giáo khoa đại học. Khi đó, việc hình thức hóa bài báo dài 166 trang của OpenAI sẽ mất 132.800 giờ làm việc. OpenAI chỉ mất 17 giờ để xác minh bằng chứng của họ trong Lean. Tôi ngần ngại khi dùng từ “mang tính cách mạng”, nhưng việc giảm chi phí của bất kỳ thứ gì xuống bốn bậc độ lớn thực sự là một cuộc cách mạng.

Tôi đã từng sử dụng AI để tạo các bản chứng minh hình thức nhằm kiểm tra công việc của mình chỉ cho một bài đăng blog nhỏ. Tôi sẽ không bao giờ mơ đến việc làm điều đó nếu phải trả lương một tuần cho ai đó để kiểm tra công việc của mình.

Xác minh hình thức không chỉ áp dụng cho toán học. Ví dụ, bạn có thể xác minh hình thức rằng một tập hợp các chính sách bảo mật là nhất quán và với những giả định nhất định, chúng đạt được mục đích đề ra. Bạn có thể xác minh hình thức rằng một hợp đồng thông minh áp đặt một mức trách nhiệm pháp lý tối đa nhất định. Bạn có thể xác minh tính đúng đắn của các thuật toán quan trọng. Những vấn đề này dễ dàng hơn so với việc hình thức hóa nghiên cứu toán học, và việc định lượng lợi tức đầu tư cũng dễ dàng hơn.

Các bài viết liên quan