Tin tức AISố chữ 5295Thời gian đọc14 phút

OpenAI công bố chứng minh điểm kỳ dị Navier–Stokes do AI tạo ra

OpenAI đã công bố một chứng minh được hình thức hóa, khẳng định rằng các dòng chảy Navier–Stokes ba chiều trơn có ngoại lực có thể phát triển điểm kỳ dị trong thời gian hữu hạn.

Mục lục · 12
  1. 1. Chứng minh được đề xuất thiết lập điều gì
  2. 2. Điểm kỳ dị trong thời gian hữu hạn được xây dựng như thế nào
  3. 3. Quy trình nghiên cứu với 10.000 tác tử
  4. 4. Bản hình thức hóa Lean giải quyết — và không giải quyết — điều gì
  5. 5. Nghiên cứu đồng thời và các câu hỏi chưa được giải đáp về nguồn gốc
  6. Câu hỏi thường gặp
  7. Bài toán Giải thưởng Thiên niên kỷ Navier–Stokes đã chính thức được giải chưa?
  8. Chứng minh có cho thấy nước thông thường có thể đạt vận tốc vô hạn không?
  9. GPT-6 Astra có phải là mô hình đã tìm ra chứng minh không?
  10. Các nhà nghiên cứu có thể kiểm tra kết quả không?
  11. Chứng minh nói về phương trình Navier–Stokes có ngoại lực hay không có ngoại lực?
  12. Tham khảo nguồn

OpenAI đã công bố một chứng minh dài 166 trang, khẳng định giải quyết Bài toán Giải thưởng Thiên niên kỷ về sự tồn tại và tính trơn của Navier–Stokes bằng cách xây dựng một dòng chất lỏng ba chiều phát triển vận tốc không bị chặn trong thời gian hữu hạn.

Công ty đã phát hành cả một bài báo toán học thông thường lẫn một bản hình thức hóa viết bằng Lean, một trợ lý chứng minh kiểm tra liệu từng bước có tuân theo các định nghĩa và giả thiết được nêu rõ hay không. OpenAI cho biết chứng minh này được tạo ra bởi khoảng 10.000 tác tử chạy đồng thời, sử dụng một mô hình nội bộ chưa phát hành “mạnh hơn đáng kể” so với GPT-6 Astra.

Kết quả này vẫn chưa được Clay Mathematics Institute chấp nhận hoặc được xác thực thông qua quy trình phản biện cần thiết cho một Giải thưởng Thiên niên kỷ. Vì vậy, tính đến ngày 9 tháng 9, nó nên được mô tả là một lời giải đề xuất đã công bố, chứ không phải một định lý đã được chính thức xác lập.

1. Chứng minh được đề xuất thiết lập điều gì

Các phương trình Navier–Stokes mô tả chuyển động của các chất lỏng nhớt như không khí và nước. Trong không gian ba chiều, các nhà toán học từ lâu vẫn chưa thể chứng minh liệu điều kiện ban đầu trơn có nhất thiết tạo ra nghiệm trơn cho mọi thời điểm tương lai hay không, hoặc liệu một điểm kỳ dị có thể hình thành.

Bài báo của OpenAI đi theo khả năng thứ hai. Định lý chính của nó phát biểu rằng với mọi độ nhớt dương, tồn tại một ngoại lực trơn và một nghiệm bắt đầu với vận tốc bằng không nhưng trở nên không bị chặn tại thời điểm \(t=1\). Dòng chảy vẫn bị giới hạn trong không gian ở một vùng compact cố định, và tổng động năng của nó duy trì bị chặn đều khi tiến gần điểm kỳ dị.

Đây là một phát biểu mạnh hơn và cụ thể hơn việc nói rằng một mô phỏng máy tính đã trở nên mất ổn định. Bài báo khẳng định một cấu trúc giải tích trong đó tốc độ cực đại của chất lỏng phân kỳ, dù trạng thái ban đầu, lực tác dụng và diễn biến trước điểm kỳ dị đều trơn.

Việc sử dụng ngoại lực là quan trọng. Phát biểu chính thức của Clay Mathematics Institute đưa ra bốn con đường được chấp nhận để giải quyết bài toán. Các phương án A và B lần lượt yêu cầu tính trơn toàn cục không có ngoại lực trong không gian ba chiều thông thường và trên một miền tuần hoàn. Các phương án C và D cho phép một ngoại lực trơn và yêu cầu một phản ví dụ trong hai bối cảnh đó.

OpenAI khẳng định thiết lập phương án C trong \(\mathbb{R}^3\). Vì vận tốc và áp suất được xây dựng có giá đỡ compact theo không gian, bài báo cho biết cùng cấu trúc đó cũng tạo ra phản ví dụ tuần hoàn cần thiết cho phương án D.

Vì vậy, kết quả không khẳng định mọi dòng chất lỏng thông thường đều trở nên kỳ dị, cũng không đưa ra nghiệm dạng đóng cho nhiễu loạn tùy ý. Nó xây dựng các ngoại lực và dòng chảy trơn cụ thể, cho thấy mô hình toán học có thể đổ vỡ trong các điều kiện được tuyên bố giải thưởng cho phép một cách rõ ràng.

2. Điểm kỳ dị trong thời gian hữu hạn được xây dựng như thế nào

Đối tượng trung tâm trong chứng minh là một xoáy đối xứng trục co lại quanh gốc tọa độ, đồng thời quay và kéo giãn dọc theo trục của nó. Khi thời điểm kỳ dị đến gần, chất lỏng xoắn ốc vào trong và vận tốc góc cùng vận tốc dọc trục của nó tăng lên.

Viết thời gian còn lại là \(\tau=1-t\), bài báo cho lõi xoáy một thang bán kính tỷ lệ xấp xỉ với \(\tau^{1/2}\) và một thang dọc trục co chậm hơn một chút. Các tốc độ góc và dọc trục đặc trưng của nó tăng xấp xỉ theo \(\tau^{-1/2-h}\), trong đó \(h\) là một tham số dương nhỏ hơn \(1/100\).

Chuyển động ngày càng nhanh bị giới hạn trong một thể tích ngày càng nhỏ. Theo cấu trúc này, động năng của lõi tỷ lệ theo \(\tau^{1/2-3h}\), tiến về không đối với các giá trị \(h\) được phép. Sự tách biệt giữa vận tốc cực đại và tổng năng lượng đó là cách chứng minh tạo ra tốc độ không bị chặn mà không vi phạm điều kiện năng lượng bị chặn trong phát biểu của Clay.

Chỉ tạo ra một xoáy co lại thì chưa đủ. Với một trường vận tốc và áp suất tùy ý, người ta có thể đơn giản định nghĩa một ngoại lực khiến phương trình Navier–Stokes được thỏa mãn, nhưng bản thân lực đó có thể phân kỳ tại thời điểm kỳ dị. Một cấu trúc như vậy sẽ không đáp ứng yêu cầu ngoại lực trơn của bài toán.

Lời giải đề xuất của OpenAI xử lý vấn đề này bằng các xung dao động cục bộ trong một vùng vành khăn bao quanh lõi xoáy. Các xung lấy năng lượng từ độ trượt nền và tạo ra các dòng thông lượng động lượng phi tuyến. Hai họ xung được bố trí để các hiệu ứng trung bình của chúng triệt tiêu phần kỳ dị của lực mà xoáy nền đang co lại lẽ ra sẽ cần.

Các hiệu chỉnh bổ sung làm giảm các sai số còn lại, trong khi một dòng chảy bên ngoài chịu chi phối bởi khuếch tán nhớt cho phép cấu trúc được cắt cụt trơn theo không gian. Kết quả cuối cùng được khẳng định là một trường vận tốc phân kỳ trong khi phần dư xuất hiện dưới dạng ngoại lực kéo dài trơn qua thời điểm kỳ dị.

3. Quy trình nghiên cứu với 10.000 tác tử

OpenAI cho biết họ bắt đầu huấn luyện mô hình nội bộ không được nêu tên vào ngày 28 tháng 8 năm 2026. Ngày 1 tháng 9, sau khi nghe các tin đồn về tiến triển đối với hai bài toán Giải thưởng Thiên niên kỷ, các nhà nghiên cứu đã giao cho các nhóm tác tử tất cả các bài toán chưa giải trong bộ sưu tập của Clay và một số câu hỏi liên quan.

Các tác tử có thể đọc một phiên bản Internet được lưu đệm, thực thi mã và trao đổi thông tin trong các nhóm. Những nhóm riêng biệt nhận các phiên bản khác nhau của thách thức Navier–Stokes, bao gồm cả các phương án về tính trơn toàn cục và sự đổ vỡ trong thời gian hữu hạn.

Một kết quả trung gian được cho là đã thay đổi hướng tìm kiếm. Gần 100 tác tử đã làm việc khoảng 50 giờ về bài toán chính quy cho các phương trình Euler không có ngoại lực, mô tả một chất lỏng lý tưởng không có độ nhớt. Sau khi các tác tử đó tạo ra một cấu trúc bùng nổ trong thời gian hữu hạn được đề xuất, OpenAI đã chuyển thêm nguồn lực sang bài toán Navier–Stokes nhớt và cung cấp kết quả Euler cho các nhóm mới.

OpenAI cũng sử dụng Codex để hợp nhất các phát hiện trung gian hữu ích và lưu chuyển chúng giữa các nhóm. Công ty cho biết cấu trúc Navier–Stokes thành công xuất hiện vào ngày 5 tháng 9, khoảng 88 giờ sau khi các tác tử đầu tiên được khởi chạy.

Nỗ lực Navier–Stokes đã tạo ra 2,7 triệu tin nhắn tác tử và khoảng 130 tỷ token đầu ra. Trên tất cả các bài toán toán học được thử trong dự án, các hệ thống đã tạo ra 4,9 triệu tin nhắn và khoảng 300 tỷ token đầu ra. Các lãnh đạo OpenAI cũng cho Axios biết chi phí tính toán lên tới hàng triệu đô la.

Mô hình tạo sinh chưa được phát hành, khiến các nhà nghiên cứu bên ngoài không thể tái tạo trực tiếp thí nghiệm. GPT-6 Astra được dùng cho giai đoạn hình thức hóa và xác minh sau đó, mà OpenAI cho biết cần thêm 17 giờ; đây không phải là mô hình ban đầu tìm ra chứng minh.

4. Bản hình thức hóa Lean giải quyết — và không giải quyết — điều gì

OpenAI đã phát hành mã nguồn Lean 4 theo giấy phép Apache 2.0. Kho mã chứa các bản hình thức hóa cho cả kết quả Navier–Stokes và Euler, đồng thời cung cấp hướng dẫn xây dựng bằng Lean 4.34.0-rc2, Mathlib và Lake.

Một chứng minh được máy kiểm tra làm tăng đáng kể độ vững chắc của bản đệ trình vì Lean yêu cầu lập luận hình thức phải kiểm tra kiểu thành công đối với một phát biểu chính xác. Nó có thể phát hiện các bước logic còn thiếu vốn có thể bị che khuất trong một suy diễn dài bằng ngôn ngữ tự nhiên, và các nhà nghiên cứu khác có thể tải xuống và xây dựng lại các tệp công khai.

Tuy nhiên, xác minh hình thức tự nó không thiết lập rằng định lý hình thức bao quát mọi điều kiện mà phát biểu Giải thưởng Thiên niên kỷ dự kiến. Các chuyên gia vẫn cần kiểm tra các định nghĩa, giả thiết, kết quả được nhập và sự tương ứng giữa lập luận giải tích dài 166 trang với phát biểu Lean. Các chuyên gia độc lập cũng phải đánh giá liệu cấu trúc toán học có hoạt động như được khẳng định hay không.

Clay Mathematics Institute không chấp nhận các lời giải đề xuất qua hình thức nộp trực tiếp. Theo quy định của viện, một lời giải trước hết phải xuất hiện trong một ấn phẩm đủ điều kiện, phải chờ ít nhất hai năm, và kết quả phải được cộng đồng toán học toàn cầu chấp nhận rộng rãi trước khi viện xem xét.

OpenAI cho biết họ không có ý định nhận giải thưởng $1 million. Quyết định đó không rút ngắn quy trình xác thực hay biến thông báo của công ty thành sự công nhận từ một tổ chức.

5. Nghiên cứu đồng thời và các câu hỏi chưa được giải đáp về nguồn gốc

OpenAI cho biết tin đồn thúc đẩy nỗ lực ngày 1 tháng 9 của họ sau đó được liên hệ với giáo sư NYU Tristan Buckmaster và nhà nghiên cứu Anthropic Levent Alpöge. Công trình đồng thời của họ liên quan đến sự bùng nổ trong thời gian hữu hạn đối với các phương trình Euler có ngoại lực và các hệ chất lỏng liên quan, thay vì kết quả Navier–Stokes nhớt do OpenAI phát hành.

Theo OpenAI, chứng minh Navier–Stokes và xác minh Lean của họ đã hoàn thành vào ngày 6 tháng 9. Sau đó, công ty liên hệ Buckmaster và Alpöge vì tin rằng họ cũng có thể đã giải Navier–Stokes, đồng thời đề xuất phối hợp công bố trong khi công nhận quyền ưu tiên của họ. OpenAI cho biết sau đó họ biết rằng kết quả của hai người xử lý Euler có ngoại lực thay vào đó.

Buckmaster đã công khai đặt câu hỏi liệu hiểu biết về dự án bên ngoài có khiến OpenAI chạy đua theo cùng hướng nghiên cứu rộng hơn hay không, và nêu quan ngại vì các bản nháp đã được xử lý qua Codex. OpenAI cho biết cả các nhà nghiên cứu lẫn tác tử của họ đều không truy cập công trình của cặp này trước khi nó được công bố, và các chứng minh kết quả sử dụng những cách tiếp cận khác biệt đáng kể.

Tuy vậy, công ty tuyên bố rằng họ không thể loại trừ hoàn toàn khả năng dữ liệu đã được khử định danh, có nguồn gốc từ việc hai người sử dụng sản phẩm OpenAI, từng đóng góp vào quá trình huấn luyện mô hình. Hiện không có bằng chứng công khai nào xác lập rằng mô hình nội bộ đã tái tạo các bản nháp của họ, và Buckmaster cũng không khẳng định biết liệu dữ liệu của mình có được sử dụng hay không.

Sự việc này tạo ra một vấn đề quản trị cụ thể cho nghiên cứu có sự hỗ trợ của AI. Các nhà khoa học sử dụng mô hình được lưu trữ cho công trình chưa công bố phải có thể xác định liệu dữ liệu đầu vào của họ có được lưu giữ, sử dụng để huấn luyện hay hiển thị cho nhà cung cấp hay không. Khi cùng một nhà cung cấp có thể triển khai các hệ tác tử lớn hơn nhiều với tư cách nhà nghiên cứu cạnh tranh, các biện pháp kiểm soát dữ liệu kỹ thuật và nguồn gốc có thể kiểm toán trở thành một phần của ghi nhận công lao khoa học — không chỉ là các cài đặt quyền riêng tư của sản phẩm.

Câu hỏi thường gặp

Bài toán Giải thưởng Thiên niên kỷ Navier–Stokes đã chính thức được giải chưa?

Chưa. OpenAI đã công bố một lời giải đề xuất, nhưng lời giải này chưa hoàn tất các yêu cầu của Clay Mathematics Institute về công bố, thời gian chờ và sự chấp nhận rộng rãi.

Chứng minh có cho thấy nước thông thường có thể đạt vận tốc vô hạn không?

Không. Nó xây dựng một dòng chảy toán học cụ thể với một ngoại lực trơn được thiết kế cẩn thận. Vận tốc vô hạn báo hiệu sự đổ vỡ của phương trình liên tục, chứ không dự đoán một chất lỏng vật lý thực sự tăng tốc không giới hạn.

GPT-6 Astra có phải là mô hình đã tìm ra chứng minh không?

Không. OpenAI quy kết khám phá này cho một mô hình nội bộ chưa phát hành mạnh hơn GPT-6 Astra. Astra được dùng trong giai đoạn hình thức hóa và xác minh Lean kéo dài 17 giờ.

Các nhà nghiên cứu có thể kiểm tra kết quả không?

Có. OpenAI đã công khai phát hành bài báo dài 166 trang và bản hình thức hóa Lean 4. Tuy nhiên, mô hình nội bộ và toàn bộ hạ tầng tác tử không thể được tái tạo công khai.

Chứng minh nói về phương trình Navier–Stokes có ngoại lực hay không có ngoại lực?

Nó sử dụng một ngoại lực trơn. Điều này được cho phép theo các phương án C và D trong phát biểu bài toán chính thức của Clay Mathematics Institute.

Tham khảo nguồn

Share

Chia sẻ bài viết