GPT-5.6 giải quyết bài toán tối ưu hóa lồi tồn tại suốt 30 năm chỉ với một câu lệnh

TL;DR: Trong một phiên làm việc kéo dài 148 phút, với một câu lệnh (prompt) được mô phỏng theo cách OpenAI đã sử dụng để chứng minh CDC, GPT 5.6 Sol Pro đã cung cấp một chứng minh giúp khép lại khoảng cách về độ phức tạp trong tối ưu hóa lồi vốn tồn tại từ năm 1996. Kết quả này đã được xác thực chính thức bằng Lean. Các liên kết đến mọi tài liệu và suy ngẫm về năng lực của AI nằm ở cuối bài viết này.

Tiết lộ: Tôi là tác giả của bản in thử (preprint) và kho lưu trữ Lean được liên kết bên dưới. Tôi có bằng Tiến sĩ toán ứng dụng và hiện là giảng viên tại khoa IEOR thuộc UC Berkeley. Kết quả này vẫn chưa được bình duyệt.

Tiếp nối thông báo gần đây về việc GPT-5.6 Sol Pro đã đưa ra chứng minh cho Giả thuyết Cycle Double Cover, tôi đã điều chỉnh phương pháp đặt câu lệnh được sử dụng trong dự án đó cho một bài toán trong tối ưu hóa lồi. Sau 148 phút làm việc liên tục, GPT-5.6 Sol Pro đã đưa ra lập luận chính cho một cận dưới mà bản thân tôi trước đây không thể chứng minh được (trong khi phần lớn công việc trước đây của tôi là chứng minh các cận dưới về độ phức tạp trong các bối cảnh khác nhau).

Bài toán liên quan đến tối ưu hóa lồi bậc không (zeroth-order) tất định: Cho B_d là hình cầu đơn vị Euclid trong ℝᵈ, và xét tất cả các hàm lồi, 1-Lipschitz f: B_d → ℝ. Một thuật toán có thể truy vấn bất kỳ điểm x ∈ B_d nào và chỉ nhận lại giá trị số thực chính xác f(x), không có thông tin nào khác (nhưng thuật toán "biết" rằng f là hàm lồi và Lipschitz). Thuật toán này hoàn toàn không bị hạn chế về mặt khác, có thể sử dụng tài nguyên tính toán và bộ nhớ không giới hạn. Các bài toán chỉ dựa trên giá trị hàm số này xuất hiện một cách tự nhiên khi một mục tiêu được đánh giá thông qua thí nghiệm vật lý hoặc mô phỏng. Bạn có thể hình dung việc chọn d tham số kỹ thuật và chỉ quan sát chi phí trả về từ mô phỏng. Nếu việc đánh giá tốn kém (như đo lường một hệ thống vật lý), câu hỏi tự nhiên là cần bao nhiêu lần đánh giá về mặt cơ bản. Điều này được chính thức hóa thành độ phức tạp oracle. Cụ thể, đây là độ phức tạp oracle của tối ưu hóa lồi dưới một oracle giá trị hàm số chính xác.

Gọi Q(d, ε) là số lượng truy vấn trường hợp xấu nhất cần thiết để tìm một điểm ε-tối ưu của f. Một thuật toán của Protasov từ năm 1996 cho thấy số lần đánh giá hàm bậc d² là đủ, điều này mang lại Q(d, ε) = O(d²), một cận trên về độ phức tạp. Các cận dưới hầu như không tồn tại cho bối cảnh này, và cận mạnh nhất áp dụng được trước đây chỉ là Ω(d), kế thừa từ mô hình oracle bậc một mạnh hơn (nơi thuật toán nhận được cả giá trị hàm số và gradient). Điều đó có nghĩa là chúng ta không biết chắc chắn liệu gradient có thực sự giúp ích trong tối ưu hóa hay không, vì các mô hình oracle chỉ dựa trên giá trị hàm số và oracle bậc một đã có cùng một cận dưới này, và do đó đã tồn tại một khoảng cách tuyến tính theo d trong độ phức tạp của bối cảnh tối ưu hóa lồi cơ bản này từ năm 1996. Vậy, bạn có thể tìm ra một thuật toán tốt hơn của Protasov và chỉ cần d lần đánh giá không? Hay bạn có thể chứng minh rằng không tồn tại thuật toán như vậy, và chúng ta có thể yên tâm rằng thuật toán của Protasov sử dụng d² lần đánh giá là tốt nhất có thể? Những gì 5.6 Sol đã chứng minh chính là điều sau.

Tôi đã làm việc với bài toán này một cách không liên tục trong khoảng một năm (tôi gặp phải nhu cầu cần một cận như vậy cho một bài báo về độ phức tạp khác mà tôi đang thực hiện). Tôi có một vài ý tưởng nhưng không thành công, và cũng đã dành nhiều phiên làm việc để cố gắng giải quyết nó với GPT-5.4 và GPT-5.5 nhưng không có kết quả, sau khi đọc về những người như Ernest Ryu đã thành công với chúng trong một số công trình về các cận tối ưu hóa.

Sau khi thấy kết quả CDC của OpenAI, tôi đã viết một câu lệnh công phu hơn nhiều theo cùng một phương pháp tổng quát. Câu lệnh của tôi dài khoảng mười trang và được đính kèm ở cuối bản in thử (xem bộ sưu tập các liên kết bên dưới). Có rất nhiều thứ được tích hợp vào câu lệnh này, từ các cách tiếp cận cần thử nghiệm cho đến cách chính xác mà mô hình nên tiến hành, nhưng nó được xây dựng chính xác theo phong cách câu lệnh CDC của OpenAI. Một lưu ý là tôi đã đặt ra yêu cầu sai số tương đối nhỏ, để chứng minh cận dưới bậc hai dưới độ chính xác bậc d⁻⁴. Sau 148 phút, GPT-5.6 Sol Pro đã trả về một chứng minh đề xuất giải quyết sự phụ thuộc bậc hai vào số chiều ở độ chính xác bậc d⁻³. Sau khi tự kiểm tra, tôi đã xác thực chính thức chứng minh đó trong Lean, và nó đã vượt qua kiểm tra xác thực hình thức. Cấu trúc và bất biến chính được sử dụng cũng hoàn toàn hợp lý đối với tôi và có liên quan chặt chẽ đến một số kết quả khác trong độ phức tạp của tối ưu hóa lồi (ví dụ, cận chặt của Nemirovsky và Yudin cho tối ưu hóa lồi bậc một cũng sử dụng các cấu trúc là cực đại của các hàm affine).

Cuối cùng, một số bình luận quan trọng về công trình liên quan đến năng lực của AI: Trong nhiều trường hợp, việc chứng minh các cận dưới như kết quả này dựa vào việc tìm ra cấu trúc phù hợp (trong trường hợp này là họ các hàm khó và chiến lược để một oracle "đối nghịch" trả lời các truy vấn từ thuật toán nhằm tiết lộ thông tin tối thiểu) và sau đó chứng minh các tính chất về nó. Chỉ có một số lượng hữu hạn các lớp hàm hợp lý để xem xét (ví dụ, các hàm bậc hai ở đây cũng sẽ hợp lý với d² bậc tự do, hoặc bất kỳ biến thể nào của cực đại các họ hàm lồi đơn giản hơn), nhưng cơ chế chứng minh thực tế sau khi tìm ra lớp hàm "đúng" và chiến lược đúng cho oracle đối nghịch thường không quá phức tạp, và thường sử dụng các kết quả hiện có từ hình học lồi hoặc tương tự (đây cũng là cấu trúc của hai kết quả trước đây của tôi nhưng ở quy mô nhỏ hơn và ít quan trọng hơn). Vì vậy, tôi không thực sự nói rằng kết quả này đang sử dụng hoặc tạo ra các kỹ thuật mới cơ bản trong hình học lồi hoặc lý thuyết tối ưu hóa. Điều này có nghĩa là từ góc độ của tôi, nếu một kết quả có thể đạt được bằng các kỹ thuật hiện có, các phương pháp AI hiện đại sẽ có thể giải quyết được các bài toán đó. Tôi không nghĩ các nhà nghiên cứu toán học/TCS sẽ trở nên lỗi thời, nhưng tôi nghĩ rằng sẽ không còn ý nghĩa khi làm việc với những vấn đề dễ dàng, hoặc thậm chí là trung bình. Chúng ta sẽ cần thiết cho những bài toán đòi hỏi các cách tiếp cận thực sự mới lạ.

Liên kết:

Bản in thử, mã Lean, các câu lệnh hoàn chỉnh, sơ đồ chứng minh và hướng dẫn xây dựng có sẵn tại đây:

https://github.com/PhillipKerger/zero-order-bounds-lean-verification

ArXiv: Khép lại khoảng cách độ phức tạp Oracle trong tối ưu hóa lồi không đạo hàm: Cận dưới gần bậc hai từ các giá trị hàm số chính xác

Phiên trò chuyện gốc kéo dài 148 phút không gián đoạn đã tạo ra chứng minh ban đầu:

https://chatgpt.com/share/6a55aa50-b484-83ea-85c0-c7e7b4bda41c

Phiên trò chuyện sau đó dẫn đến sự tinh chỉnh d⁻¹ᐟ²:

https://chatgpt.com/share/6a55ad10-7644-83ea-859e-5483d2e0dff0

Câu lệnh CDC của OpenAI, mà tôi đã cấu trúc mọi thứ theo đó:

https://cdn.openai.com/pdf/04d1d1e4-bc75-476a-97cf-49055cd98d31/cdc_prompt.pdf

Và một bài viết dễ tiếp cận hơn mà tôi đã viết trên Medium:

https://medium.com/@kerger.p/an-ai-assisted-breakthrough-in-convex-optimization-an-optimization-problem-dating-back-30-years-a-db5c631119de

Chỉnh sửa: Đây là Sol PRO, không phải Ultra. Tôi đã làm việc trong codex trước đó, nơi cấp độ trên XHigh là Ultra. Nhưng tôi đã thực hiện việc này trong giao diện web, nơi cao nhất là Pro, thực tế không hoàn toàn giống với Ultra.