Giải thích tuyên bố chứng minh Navier–Stokes của OpenAI

Các phương trình Navier–Stokes mô tả cách các chất lưu như nước và không khí chuyển động. Chúng là trung tâm của động lực học chất lưu, kỹ thuật và vật lý, nhưng các nhà toán học vẫn chưa có hiểu biết giải tích hoàn chỉnh về hành vi của chúng trong ba chiều.

Phiên bản Giải thưởng Thiên niên kỷ hỏi, đại ý, liệu các điều kiện ban đầu trơn có luôn dẫn đến nghiệm trơn cho mọi thời điểm trong tương lai hay không, hay liệu các phương trình có thể “blow up” — tạo ra một kỳ dị nơi một đại lượng như vận tốc trở nên vô hạn. Clay Mathematics Institute đã nêu bài toán này là một trong bảy Bài toán Giải thưởng Thiên niên kỷ vào năm 2000, mỗi bài gắn với giải thưởng $1 triệu. Trước thông báo này, trong số bảy bài toán, chỉ có giả thuyết Poincaré đã được giải, như Wikipedia tóm tắt.

Tuyên bố của OpenAI, theo Quanta Magazine đưa tin, là các tác nhân AI tự trị chạy trên một mô hình nội bộ đã tìm thấy một kỳ dị trong các phương trình Navier–Stokes ba chiều. Quanta cho biết công trình sử dụng khoảng 10.000 tác nhân, các tác nhân tìm được một chứng minh sau 88 giờ, và một mô hình AI khác đã hình thức hóa kết quả trong Lean sau thêm 17 giờ. Các tác nhân đã trao đổi gần 5 triệu tin nhắn, và Sébastien Bubeck của OpenAI ước tính chi phí tính toán là vài triệu đô la, theo Quanta.

MIT Technology Review đưa tin rằng OpenAI nói họ không có kế hoạch nhận giải thưởng $1 triệu. Theo Wikipedia, phản ví dụ này vẫn chưa được các nhà toán học bên ngoài hoặc Clay Mathematics Institute xác minh.

Điểm cuối cùng đó rất quan trọng. Một hình thức hóa trong Lean là tín hiệu mạnh, nhưng không đồng nhất với sự chấp nhận của cộng đồng. Quanta lưu ý rằng chứng minh hình thức có thể xác lập rằng một mệnh đề suy ra được bên trong trợ lý chứng minh, trong khi các nhà toán học vẫn cần kiểm tra rằng mệnh đề đã hình thức hóa tương đương về mặt logic với tuyên bố toán học mà mọi người định chứng minh.

Phương trình vi phân mô tả các quan hệ giữa những đại lượng đang thay đổi. Trong cơ học chất lưu, các phương trình Navier–Stokes kết hợp vận tốc, áp suất, độ nhớt, lực bên ngoài và bảo toàn khối lượng. Chúng đủ dễ để viết ra bằng ký hiệu chuẩn, nhưng hành vi dài hạn của chúng có thể cực kỳ khó hiểu.

Khó khăn cốt lõi không phải là liệu các kỹ sư có thể mô phỏng chất lưu hay không. Họ làm điều đó liên tục. Vấn đề là liệu các phương trình toán học lý tưởng hóa có được đảm bảo hành xử tốt dưới các điều kiện do bài toán Giải thưởng Thiên niên kỷ quy định hay không.

Một kỳ dị sẽ có nghĩa là các phương trình dự đoán một sự sụp đổ: một phần nào đó của chất lưu tiến hóa tới một trạng thái toán học bất khả. Như Quanta giải thích, điều này không hàm ý một thất bại thực tiễn tức thì trong kỹ thuật thế giới thực, vì các chất lưu thực được tạo thành từ phân tử và nguyên tử chứ không phải những continuum trơn hoàn hảo. Nhưng xét như toán học, nó sẽ cho thấy các phương trình lý tưởng hóa có hành vi bất ngờ hơn nhiều người từng nghĩ.

Bài toán này cũng liên quan đến nhiễu loạn, một trong những hiện tượng khó nhất trong vật lý. Wikipedia mô tả nhiễu loạn là một trong những bài toán chưa giải lớn nhất của vật lý, bất chấp tầm quan trọng của nó trong khoa học và kỹ thuật. Một chứng minh về blowup sẽ không “giải quyết nhiễu loạn” theo nghĩa thực tiễn, nhưng nó sẽ định hình lại những gì các nhà toán học biết về các phương trình đứng sau hiện tượng đó.

Tranh cãi xoay quanh mối quan hệ giữa công trình của OpenAI và công trình của Buckmaster cùng Alpöge.

Quanta đưa tin rằng thông báo của OpenAI xuất hiện khoảng 12 giờ sau khi Buckmaster công bố kết quả với Alpöge về các bài toán có liên quan chặt chẽ. Công trình của họ sử dụng nhiều mô hình AI, bao gồm các mô hình của OpenAI. MIT Technology Review đưa tin rằng Buckmaster và Alpöge đã làm việc gần một năm về bài toán này, và Buckmaster đã đăng một chứng minh cho thấy một phiên bản đơn giản hóa của các phương trình Navier–Stokes có thể sụp đổ.

Cả công trình của OpenAI lẫn công trình Buckmaster–Alpöge dường như đều dựa trên một hướng tiếp cận gắn với Diego Córdoba và Luis Martínez-Zoroa. Quanta nói cả hai nhóm đều dựa nhiều vào công trình của Córdoba và Martínez-Zoroa, những người đã phát triển một chiến lược rời khỏi các phương pháp mà phần lớn nhà toán học đang dùng. MIT Technology Review dẫn lời giáo sư toán học Javier Gómez-Serrano của Brown University nói rằng hướng tiếp cận này là một trong vài hướng được cho là có triển vọng với bài toán.

Theo MIT Technology Review, OpenAI đã thừa nhận rằng nhóm của họ được truyền cảm hứng để theo đuổi bài toán sau khi nghe một tin đồn về nỗ lực của Buckmaster và Alpöge. Tranh chấp nằm ở việc liệu các mô hình hoặc nhân viên của OpenAI có truy cập, được huấn luyện trên, hoặc theo cách khác hưởng lợi từ công trình của Buckmaster và Alpöge hay không.

MIT Technology Review đưa tin rằng Buckmaster đã đăng một tài liệu mô tả các tương tác với nhân viên OpenAI. Theo tường thuật của Buckmaster, nhân viên OpenAI đưa ra hai khả năng. Buckmaster và Alpöge có thể đăng công trình của họ và OpenAI sẽ đăng lời giải Navier–Stokes của mình vào ngày hôm sau, hoặc Buckmaster có thể làm việc với OpenAI trên một bài báo Navier–Stokes loại Alpöge khỏi danh sách tác giả vì mối liên hệ của ông với Anthropic. MIT Technology Review cũng đưa tin rằng OpenAI phủ nhận việc nhân viên hoặc tác nhân của họ truy cập các bản ghi trao đổi của Buckmaster và Alpöge.

Đó là những cáo buộc nghiêm trọng, nhưng hồ sơ công khai vẫn chưa đầy đủ. Lập trường đúng là tách tuyên bố toán học khỏi tranh chấp ghi công. Chứng minh có thể đúng trong khi quy trình vẫn còn bị tranh cãi về mặt đạo đức. Hoặc chứng minh có thể thất bại khi được phản biện trong khi các câu hỏi về ghi công vẫn quan trọng.

Lean là một trợ lý chứng minh: một hệ thống để biểu đạt các mệnh đề toán học và kiểm tra rằng từng bước suy ra từ các quy tắc hình thức. Trong toán học có mức độ rủi ro cao, điều đó có thể loại bỏ một lớp lỗi lớn. Nó cũng có thể khiến các chứng minh do AI sinh ra dễ kiểm toán hơn, vì chứng minh không chỉ là văn xuôi; nó là logic hình thức có thể thực thi.

Đó là lý do thành phần Lean quan trọng. Nếu việc hình thức hóa là vững chắc và khớp với mệnh đề Navier–Stokes dự định, kết quả sẽ khó bị gạt bỏ hơn nhiều như một ảo giác trôi chảy. Với những người xây dựng AI, đây là khác biệt giữa một mô hình viết ra lập luận có vẻ hợp lý và một hệ thống tạo ra các artifact mà một chương trình khác có thể kiểm tra.

Nhưng Lean không giải quyết mọi vấn đề về niềm tin. Nó không xác lập quyền ưu tiên. Nó không tiết lộ chứng minh được tìm thấy như thế nào. Nó không giải thích liệu dữ liệu riêng tư, bản ghi trao đổi hay ý tưởng chưa công bố có ảnh hưởng đến quá trình tìm kiếm hay không. Và nó không thay thế vai trò của cộng đồng toán học trong việc diễn giải ý nghĩa của chứng minh.

Sự phân biệt này sẽ quen thuộc với những người xây dựng sản phẩm AI. Structured outputs, kiểm thử, evals và kiểm tra hình thức có thể làm hệ thống đáng tin cậy hơn, nhưng tự thân chúng không trả lời các câu hỏi về quản trị. Nếu một tác nhân AI có thể gọi công cụ, kiểm tra logs, tái sử dụng ngữ cảnh riêng tư hoặc phối hợp với tác nhân khác, hệ thống cần ranh giới và dấu vết kiểm toán không kém gì năng lực thô.

Đó là một lý do công việc đa tác nhân là một bài toán kỹ thuật, không chỉ là một mẹo prompting. Dù bạn đang thiết kế tác nhân nghiên cứu hay workflow kinh doanh, các câu hỏi thực tế đều tương tự: tác nhân nào có thể thấy ngữ cảnh nào, chúng có thể gọi công cụ nào, handoff diễn ra ở đâu, và điều gì được ghi log? Những lựa chọn thiết kế đó quan trọng trong các tác nhân AI từ rất lâu trước khi mức độ rủi ro chạm tới lãnh địa Giải thưởng Thiên niên kỷ.

Chi tiết vận hành nổi bật nhất là quy mô. Quanta báo cáo khoảng 10.000 tác nhân, 88 giờ tìm kiếm, thêm 17 giờ cho hình thức hóa và gần 5 triệu tin nhắn giữa các tác nhân. MIT Technology Review đưa tin rằng OpenAI nói lần chạy này tốn hàng triệu đô la.

Quy mô đó không nằm trong tầm với của phần lớn nhóm học thuật. Nó gợi ra một tương lai có thể xảy ra, nơi tiến bộ toán học tuyến đầu phụ thuộc vào các mô hình nội bộ, ngân sách tính toán riêng tư và hạ tầng tác nhân tập trung bên trong một vài công ty AI.

MIT Technology Review đóng khung đây là một bước ngoặt đối với toán học: nếu các bài toán mở lớn có thể bị tấn công bởi những bầy tác nhân riêng tư, các chuẩn mực hợp tác học thuật có thể bị căng kéo. Các nhà toán học thường học từ những nỗ lực thất bại, kết quả một phần và các ngã rẽ sai. Nếu những điều đó diễn ra bên trong các hệ thống riêng tư và không bao giờ trở thành công khai, lĩnh vực có thể nhận được câu trả lời mà không có con đường chung vốn truyền thống tạo ra công cụ và phân ngành mới.

Quanta dẫn lời nhà toán học Princeton Charles Fefferman, người viết mô tả bài toán chính thức của Clay Institute, nói rằng ông rất vui vì bài toán đã được giải và xác định Córdoba cùng Martínez-Zoroa là những người hùng của câu chuyện. Sự ghi công đó là một hiệu chỉnh hữu ích. Ngay cả khi bước cuối cùng được tự động hóa, gu nghiên cứu — chọn một hướng đi hứa hẹn — đến từ công trình toán học của con người được xây dựng qua nhiều năm.

Với những người xây dựng, bài học không phải là “dùng thêm tác nhân.” Đó là các hệ thống agentic khuếch đại chất lượng của không gian tìm kiếm mà chúng được giao. Mô hình tốt hơn và ngân sách lớn hơn có ích, nhưng cách đóng khung bài toán, lựa chọn ngữ cảnh, quyền truy cập công cụ và vòng lặp xác minh vẫn quyết định liệu hệ thống khám phá vùng hữu ích hay đốt compute.

Nếu bạn đang routing công việc qua nhiều mô hình, cùng nguyên tắc đó áp dụng ở quy mô nhỏ hơn. Dùng mô hình tốt nhất cho công việc, nhưng đừng xem lựa chọn mô hình là toàn bộ hệ thống. Workflow xung quanh — truy xuất, ràng buộc, kiểm tra, phê duyệt và logs — là nơi độ tin cậy xuất hiện. Nói cách khác, năng lực đến từ toàn bộ workflow, không phải từ một lựa chọn trên leaderboard.

Điều đầu tiên cần theo dõi là xác nhận toán học. Các nhà toán học bên ngoài và Clay Mathematics Institute sẽ cần thời gian để đánh giá liệu chứng minh có đúng hay không, liệu hình thức hóa Lean có khớp với tuyên bố dự định hay không, và kết quả ăn khớp thế nào với các công trình trước đó.

Điều thứ hai là ghi công. Các tường thuật công khai từ OpenAI, Buckmaster, Alpöge và các nhà toán học bên ngoài vẫn chưa tạo thành một hồ sơ đã ngã ngũ. Các câu hỏi trung tâm mang tính sự kiện: các tác nhân hoặc nhân viên của OpenAI đã truy cập gì, họ được huấn luyện trên gì, họ biết gì, và họ biết điều đó khi nào?

Điều thứ ba là liệu việc này có trở thành một khuôn mẫu hay không. Nếu các phòng thí nghiệm AI tuyến đầu có thể hướng những bầy tác nhân khổng lồ vào các bài toán nổi tiếng chưa giải, sẽ có thêm nhiều thông báo nối tiếp. Một số sẽ sạch sẽ. Một số sẽ bị tranh chấp. Một số sẽ thất bại khi được phản biện. Các lĩnh vực bị ảnh hưởng sẽ cần chuẩn mực về ghi công, công bố, compute riêng tư và các tuyên bố quyền ưu tiên có AI hỗ trợ.

Với những người xây dựng bằng AI ngoài toán học thuần túy, thông điệp đủ rõ: năng lực đang dịch chuyển về phía các hệ thống, không phải từng prompt đơn lẻ. Tác nhân, công cụ, model routing và xác minh đang trở thành đơn vị công việc. Những đội xử lý tốt nguồn gốc và phản biện sẽ ở vị thế tốt hơn các đội chỉ chạy theo đầu ra lớn hơn.

Chúng tôi sẽ tiếp tục theo dõi câu chuyện xác minh và ghi công khi nó phát triển. Nếu bạn muốn nhận tin AI với phần bối cảnh kỹ thuật được giữ lại, bạn có thể đăng ký bản tin LIA.

• OpenAI tuyên bố các tác nhân AI tự trị đã tìm thấy một kỳ dị trong các phương trình Navier–Stokes ba chiều và tạo ra một hình thức hóa Lean.
• Kết quả vẫn chưa được các nhà toán học bên ngoài xác minh hoặc được Clay Mathematics Institute chấp nhận.
• Một chứng minh Lean có thể giảm nhiều lỗi kiểm tra chứng minh, nhưng người phản biện vẫn cần xác nhận rằng mệnh đề hình thức khớp với tuyên bố toán học dự định.
• Thông báo này vướng vào một tranh chấp ghi công liên quan đến công trình của Tristan Buckmaster, Levent Alpöge, Diego Córdoba và Luis Martínez-Zoroa.
• Quy mô được báo cáo của lần chạy làm nổi bật khoảng cách tài nguyên giữa các phòng thí nghiệm AI tuyến đầu và phần lớn nhóm học thuật.
• Với những người xây dựng AI, sự kiện này cho thấy tác nhân cần nguồn gốc, dấu vết kiểm toán, vòng lặp xác minh và ranh giới rõ ràng, chứ không chỉ thêm compute.

Phần này trả lời các câu hỏi thực tế đằng sau tuyên bố Navier–Stokes của OpenAI: các câu trả lời bên dưới bao quát thông báo, vai trò của Lean và những phần vẫn cần phản biện độc lập. Nó cũng tách mức độ quan trọng về toán học khỏi tranh chấp ghi công quanh công trình.

OpenAI nói họ có một lời giải do AI sinh ra, nhưng tuyên bố này vẫn cần được phản biện toán học bên ngoài và được Clay Mathematics Institute đánh giá.

Theo các báo cáo được trích dẫn, OpenAI tuyên bố các tác nhân của họ đã tìm thấy một kỳ dị trong các phương trình Navier–Stokes ba chiều và một mô hình khác đã hình thức hóa kết quả trong Lean.

Lean có thể kiểm tra rằng từng bước hình thức suy ra từ các quy tắc, khiến chứng minh khó bị gạt bỏ hơn như văn xuôi có vẻ hợp lý. Các nhà toán học vẫn cần xác minh rằng mệnh đề đã hình thức hóa khớp với tuyên bố Navier–Stokes dự định.

Tranh chấp liên quan đến việc liệu công trình của OpenAI có hưởng lợi từ nghiên cứu có AI hỗ trợ của Tristan Buckmaster và Levent Alpöge mà không ghi công đúng mức hay không. Theo MIT Technology Review, OpenAI đã phủ nhận rằng nhân viên hoặc tác nhân của họ truy cập các bản ghi trao đổi của hai người này.

Không. Một chứng minh blowup sẽ định hình lại hiểu biết toán học về các phương trình đứng sau chuyển động chất lưu, nhưng nó sẽ không trực tiếp giải quyết nhiễu loạn như một bài toán kỹ thuật thực tiễn.