💡 Theo đánh giá của RetroLab, đây là một minh chứng rõ ràng cho thấy AI không chỉ hỗ trợ mà còn có thể chủ động tạo ra các chứng minh toán học có giá trị. Tuy nhiên, cần thận trọng: kết quả chưa qua bình duyệt và vẫn dựa trên các kỹ thuật đã biết – AI chưa thực sự 'sáng tạo' ra phương pháp mới.
Trong một phiên làm việc kéo dài 148 phút, mô hình GPT-5.6 Sol Pro của OpenAI đã tạo ra một chứng minh toán học giúp đóng khoảng trống phức tạp trong lĩnh vực tối ưu lồi (convex optimization) – một bài toán tồn tại từ năm 1996. Kết quả sau đó đã được xác thực chính thức bằng công cụ kiểm chứng hình thức Lean, đánh dấu một bước tiến mới trong khả năng của AI đối với nghiên cứu toán học thuần túy.
Tác giả của nghiên cứu này, Phillip Kerger – tiến sĩ toán ứng dụng và giảng viên tại khoa Kỹ thuật Công nghiệp & Nghiên cứu Vận hành (IEOR) của Đại học California, Berkeley – đã công bố bản thảo và mã nguồn Lean trên GitHub. Công trình chưa được bình duyệt chính thức, nhưng đã gây chú ý trong cộng đồng khoa học máy tính.
Bài toán tối ưu lồi không sử dụng đạo hàm
Vấn đề trọng tâm thuộc về lĩnh vực tối ưu lồi deterministic zeroth-order (chỉ sử dụng giá trị hàm số, không có gradient). Cụ thể: xét một hàm lồi, 1-Lipschitz trên hình cầu đơn vị Euclid trong không gian ℝᵈ. Một thuật toán có thể truy vấn bất kỳ điểm nào và chỉ nhận lại giá trị chính xác của hàm tại điểm đó – không có thông tin về đạo hàm hay gradient. Đây là tình huống thực tế khi đánh giá một hàm mục tiêu thông qua mô phỏng vật lý hoặc thí nghiệm, nơi mỗi lần đánh giá tốn kém.
Năm 1996, nhà toán học Protasov đã đưa ra một thuật toán chứng minh rằng cần khoảng d² lần đánh giá hàm là đủ, tức Q(d, ε) = O(d²). Tuy nhiên, cận dưới (lower bound) cho bài toán này hầu như không tồn tại. Kết quả mạnh nhất trước đó chỉ là Ω(d) – một cận thừa hưởng từ mô hình first-order (có cả gradient). Điều này đồng nghĩa với việc suốt 30 năm, giới nghiên cứu không biết liệu gradient có thực sự giúp ích hay không, vì cận dưới của cả hai mô hình là như nhau.
GPT-5.6 Sol Pro và chứng minh mang tính đột phá
Kerger đã làm việc rải rác trong khoảng một năm với bài toán này, thử nghiệm với GPT-5.4 và GPT-5.5 nhưng không thành công. Sau khi OpenAI công bố chứng minh Giả thuyết Phủ Chu trình Kép (Cycle Double Cover Conjecture) bằng GPT-5.6 Sol Pro, Kerger quyết định áp dụng cùng một phương pháp luận. Ông viết một prompt dài khoảng 10 trang, mô phỏng theo phong cách prompt của OpenAI cho CDC, và để mô hình làm việc liên tục trong 148 phút.
Kết quả: GPT-5.6 Sol Pro đã đưa ra một chứng minh cho cận dưới bậc hai (Ω(d²)) với độ chính xác cỡ d⁻³ – thậm chí tốt hơn yêu cầu ban đầu là d⁻⁴. Sau khi tự kiểm tra, Kerger đã xác thực chứng minh này trong Lean, và nó vượt qua tất cả các kiểm tra hình thức. Cấu trúc chứng minh sử dụng các hàm affine tối đa (max of affine functions) – một kỹ thuật quen thuộc trong các kết quả kinh điển của Nemirovsky và Yudin về tối ưu lồi first-order.
Ý nghĩa và góc nhìn về năng lực AI
Theo Kerger, việc tìm ra lớp hàm phù hợp và chiến lược đối phó (adversarial oracle) là chìa khóa. Một khi đã xác định được hướng đi, các bước chứng minh còn lại thường không quá phức tạp và dựa trên các kết quả có sẵn trong hình học lồi. Ông nhận xét: "Tôi sẽ không nói rằng kết quả này sử dụng hay tạo ra những kỹ thuật hoàn toàn mới trong lý thuyết tối ưu. Điều này cho thấy nếu một bài toán có thể giải được bằng các phương pháp hiện có, thì AI hiện đại có thể giải nó."
Kerger tin rằng các nhà nghiên cứu toán học và khoa học máy tính lý thuyết sẽ không bị thay thế, nhưng những bài toán 'trái cây thấp' hay thậm chí 'trái cây tầm trung' sẽ không còn đáng để đầu tư công sức. Công việc thực sự có giá trị sẽ là những bài toán đòi hỏi cách tiếp cận hoàn toàn mới.
Tài liệu tham khảo
- Bản thảo, mã Lean, prompt đầy đủ và hướng dẫn: GitHub
- Bản in trên arXiv: Closing the Oracle-Complexity Gap in Derivative-Free Convex Optimization: A Near-Quadratic Lower Bound from Exact Function Values
- Phiên chat 148 phút gốc: ChatGPT share
- Phiên chat dẫn đến cải tiến d⁻¹ᐟ²: ChatGPT share
- Prompt CDC của OpenAI: PDF
- Bài viết trên Medium của tác giả: Medium
Lưu ý: Phiên bản sử dụng là Sol Pro, không phải Ultra. Trong Codex, cấp trên XHigh là Ultra, nhưng trên giao diện web, cấp cao nhất là Pro – không hoàn toàn tương đương.
Nguồn: Hacker News - https://old.reddit.com/r/math/comments/1uxj3cy/after_openais_cdc_proof_announcement_gpt56_used_a/
