Trong một công bố mới đây, OpenAI đã gây chú ý lớn khi giải quyết một bài toán kỳ cựu liên quan đến phương trình Navier-Stokes trong động lực học chất lưu. Đáng chú ý, bên cạnh bản chứng minh cho con người đọc, OpenAI còn đính kèm một bản chứng minh chính thức (formal proof) được mã hóa bằng ngôn ngữ Lean 4 để máy tính có thể tự động xác minh.
Trước đây, việc chuyển đổi một công trình nghiên cứu toán học sang dạng mã xác minh bằng máy tính là quy trình cực kỳ tốn thời gian. Theo ước tính từ giới nghiên cứu, việc hình thức hóa một trang sách giáo khoa toán đại học mất khoảng 40 giờ làm việc. Đối với các bài báo khoa học chuyên sâu dài 166 trang như của OpenAI, quy trình thủ công có thể ngốn tới 132.800 giờ công. Tuy nhiên, hệ thống của OpenAI kết hợp với công cụ như Prove2Me đã hoàn thành việc xác minh trong Lean 4 chỉ mất 17 giờ, cắt giảm chi phí và thời gian tới 4 cấp độ quy mô.
Phương pháp xác minh tự động này không chỉ áp dụng cho toán học lý thuyết mà còn có tiềm năng ứng dụng lớn trong kiểm thử phần mềm, như xác thực chính sách bảo mật, kiểm tra hợp đồng thông minh (smart contract) hay các thuật toán quan trọng trong hệ thống đám mây của Google và AWS.
Đột phá này đánh dấu bước tiến quan trọng trong việc ứng dụng AI vào nghiên cứu toán học chuyên sâu. Đối với cộng đồng công nghệ và các nhà phát triển tại Việt Nam, sự kết hợp giữa LLM và các công cụ xác minh chính thức như Lean 4 sẽ mở ra cơ hội tối ưu hóa kiểm thử phần mềm và xây dựng các hệ thống AI có độ tin cậy tuyệt đối.
Nguồn: Hacker News — Biên dịch & tổng hợp: danhbaai.com