Một mô hình OpenAI đã bác bỏ một giả thuyết trọng tâm trong lĩnh vực hình học rời rạc

Trong gần 80 năm, các nhà toán học đã nghiên cứu một câu hỏi tưởng đơn giản mà không hề đơn giản: nếu đặt $n$ điểm trên mặt phẳng, có bao nhiêu cặp điểm có thể cách nhau đúng $1$ đơn vị?

Đây là bài toán khoảng cách đơn vị trên mặt phẳng, lần đầu tiên được Paul Erdős nêu ra vào năm 1946. Đây là một trong những câu hỏi nổi tiếng nhất trong hình học tổ hợp, dễ nêu ra nhưng lại vô cùng khó giải quyết. Cuốn sách "Các vấn đề nghiên cứu trong hình học rời rạc" năm 2005 của Brass, Moser và Pach gọi nó là "có lẽ là vấn đề được biết đến nhiều nhất (và dễ giải thích nhất) trong hình học tổ hợp." Noga Alon, một nhà tổ hợp học hàng đầu tại Princeton, mô tả nó là “một trong những bài toán yêu thích của Erdős”. Erdős thậm chí còn đưa ra một giải thưởng tiền tệ để giải quyết vấn đề này.

Hôm nay, chúng tôi chia sẻ một đột phá về bài toán khoảng cách đơn vị. Kể từ công trình gốc của Erdős, niềm tin phổ biến là các cấu trúc “lưới vuông” được minh họa ở phần dưới về cơ bản là tối ưu để tối đa hóa số cặp cách nhau một đơn vị. Một mô hình nội bộ của OpenAI đã bác bỏ giả thuyết tồn tại lâu nay này, bằng cách cung cấp một tập hợp vô hạn các ví dụ cho cải thiện bậc đa thức. Chứng minh đã được một nhóm các nhà toán học bên ngoài kiểm tra. Họ cũng đã viết một bài báo đi kèm giải thích lập luận và cung cấp thêm nền tảng cũng như bối cảnh về ý nghĩa của kết quả.

Điều đáng chú ý khác là cách kết quả được tìm ra. Chứng minh đến từ một mô hình suy luận đa dụng mới, chứ không phải từ một hệ thống được huấn luyện riêng cho toán học, được dựng khung để tìm kiếm các chiến lược chứng minh, hay nhắm riêng vào bài toán khoảng cách đơn vị. Là phần của nỗ lực rộng lớn nhằm kiểm tra xem các mô hình cao cấp có thể góp phần vào nghiên cứu tiên phong hay không, chúng tôi đã đánh giá nó trên bộ sưu tập các bài toán Erdős. Trong trường hợp này, nó đã tạo ra một chứng minh giải quyết bài toán mở.

Chứng minh này là một cột mốc quan trọng đối với cộng đồng toán học và AI. Đây là lần đầu tiên một bài toán mở nổi bật, giữ vai trò trung tâm trong một phân ngành toán học, được AI giải một cách tự chủ. Nó cũng cho thấy chiều sâu suy luận mà các hệ thống này hiện nay hỗ trợ. Toán học là một môi trường thử nghiệm đặc biệt rõ ràng cho suy luận: các bài toán có tính chính xác, các chứng minh tiềm năng có thể được kiểm tra, và một lập luận dài chỉ có tác dụng nếu suy luận giữ được tính nhất quán từ đầu đến cuối. Phương pháp mà bài toán được giải cũng rất đáng chú ý. Chứng minh đưa những ý tưởng tinh vi, và bất ngờ từ lý thuyết số đại số vào một câu hỏi hình học sơ cấp.

Tim Gowers, người đoạt Huy chương Fields, viết trong bài báo đi kèm, gọi kết quả này là “một cột mốc của toán học AI”. Theo nhà lý thuyết số hàng đầu Arul Shankar, “Theo tôi, bài báo này cho thấy các mô hình AI hiện tại không chỉ là trợ thủ cho các nhà toán học con người – chúng có khả năng nảy ra những ý tưởng nguyên bản, tài tình, rồi triển khai chúng đến kết quả cuối cùng”.

Chứng minh có tại đây⁠(mở trong cửa sổ mới). Bài báo đi kèm của các nhà toán học bên ngoài hàng đầu có tại đây⁠(mở trong cửa sổ mới). Bạn có thể tìm thấy phiên bản rút gọn chuỗi suy nghĩ của mô hình tại đây⁠(mở trong cửa sổ mới).

Gọi $u(n)$ là số lượng lớn nhất có thể của các cặp cách nhau một đơn vị trong số $n$ điểm trên mặt phẳng. Các ví dụ đạt tốc độ tăng trưởng tuyến tính rất dễ xây dựng: đặt $n$ điểm trên một đường thẳng cho $n-1$ cặp, còn một lưới vuông cho khoảng $2n$ cặp. Cấu trúc tốt nhất từng được biết trước đây, đến từ một lưới vuông được co giãn lại, hóa ra còn cho nhiều hơn: $n^{1 + C / \log \log(n)}$ với một hằng số $C$. Vì $\log \log(n)$ tiến tới vô hạn khi $n$ tăng, hạng bổ sung trong số mũ tiến tới $0$, nghĩa là các cấu trúc này chỉ đạt tăng trưởng nhanh hơn tuyến tính một chút. Trong nhiều thập kỷ, người ta tin rộng rãi rằng tốc độ này về cơ bản là tối ưu, và không cấu trúc nào có thể cải thiện đáng kể so với lưới vuông. Về mặt kỹ thuật, Erdős phỏng đoán một giới hạn trên của $n^{1+o(1)}$ trong đó $o(1)$ bổ sung cho biết một thuật ngữ có xu hướng $0$ với $n$.

Kết quả mới của chúng tôi bác bỏ giả thuyết này. Cụ thể hơn, với vô số giá trị của $n$, chứng minh này xây dựng các cấu hình gồm $n$ điểm với ít nhất $n^{1+\delta}$ cặp khoảng cách đơn vị, cho một số mũ cố định $\delta > 0$. (Chứng minh AI ban đầu không cho ra một $\delta$ tường minh, nhưng một bản tinh chỉnh sắp công bố do giáo sư toán Princeton Will Sawin thực hiện đã cho thấy có thể lấy $\delta=0.014$.)

Lịch sử của bài toán giúp ta hiểu tại sao kết quả này lại gây ngạc nhiên. Cận dưới tốt nhất từng biết về cơ bản không thay đổi kể từ cấu trúc gốc năm 1946 của Erdős. Cận trên tốt nhất, $O(n^{4/3})$, bắt nguồn từ công trình của Spencer, Szemerédi và Trotter năm 1984, và bất chấp các tinh chỉnh sau đó cùng các công trình cấu trúc liên quan của Székely, Katz và Silier, Pach, Raz và Solymosi cùng nhiều người khác, cận trên này về cơ bản vẫn không thay đổi. Để hỗ trợ cho giả thuyết, Matoušek và Alon-Bucić-Sauermann đã nghiên cứu bài toán với các khoảng cách phi Euclid trên mặt phẳng, và chứng minh rằng “phần lớn” các khoảng cách phi Euclid này tuân theo giả thuyết theo một nghĩa nào đó.

Ngạc nhiên thay, các thành phần chính của cấu trúc này xuất phát từ một lĩnh vực toán học rất khác biệt được gọi là lý thuyết số đại số, lĩnh vực nghiên cứu các khái niệm như phân tích thừa số trong các mở rộng của tập số nguyên được gọi là các trường số đại số.

Nhìn tổng quát, lời chứng minh bắt đầu từ một ý tưởng hình học quen thuộc và đưa nó theo một hướng hoàn toàn bất ngờ.

Cận dưới ban đầu của Erdős có thể được hiểu thông qua các số nguyên Gauss: các số có dạng $a+bi$, trong đó $a$ và $b$ là số nguyên còn $i$ là căn bậc hai của $-1$. Các số nguyên Gaussian là phần mở rộng của số nguyên thông thường và cũng sở hữu tính chất phân tích duy nhất thành các số nguyên tố, giống như số nguyên thông thường. Những phần mở rộng như vậy của tập số nguyên hoặc số hữu tỷ thông thường được gọi là các trường số đại số. Lập luận mới thay thế các số nguyên Gaussian bằng những khái quát phức tạp hơn từ lý thuyết số đại số, với các đối xứng phong phú hơn có thể tạo ra nhiều sự khác biệt có độ dài đơn vị hơn nữa.

Lập luận chính xác sử dụng các công cụ như tháp trường lớp vô hạn và lý thuyết Golod–Shafarevich để chỉ ra rằng các trường số cần cho lập luận thực sự tồn tại. Những ý tưởng này vốn đã quen thuộc với các nhà lý thuyết số đại số, nhưng việc các khái niệm này có hệ quả đối với các câu hỏi hình học trên mặt phẳng Euclid là một bất ngờ lớn.

Kết quả này đánh dấu một cột mốc quan trọng trong mối quan hệ giữa AI và toán học: một hệ thống AI đã tự mình giải quyết được một bài toán mở tồn tại nhiều năm, nằm ngay trung tâm của một lĩnh vực nghiên cứu sôi nổi. Kết qủa cũng mở ra cái nhìn sơ khởi về một kiểu hợp tác mới giữa AI và các nhà toán học con người. Trong trường hợp này, công trình đi kèm của các nhà toán học bên ngoài vẽ nên một bức tranh phong phú hơn đáng kể so với chỉ riêng lời giải ban đầu.

Như Thomas Bloom viết trong ghi chú đi kèm:

“Khi đánh giá tầm quan trọng và ảnh hưởng của một chứng minh do AI tạo ra, câu hỏi tôi tự đặt ra là: điều này có dạy cho chúng ta điều gì mới về bài toán không? Giờ đây chúng ta có hiểu hình học rời rạc rõ hơn không? Tôi nghĩ câu trả lời là có, nhưng ở mức vừa phải: điều này cho thấy các cấu trúc từ lý thuyết số còn có nhiều điều để nói về những loại câu hỏi này hơn chúng ta từng nghi ngờ; hơn nữa, lý thuyết số cần đến có thể rất sâu. Chắc chắn nhiều nhà lý thuyết số đại số sẽ xem xét kỹ các bài toán mở khác trong lĩnh vực hình học rời rạc trong những tháng tới.”

Mối liên hệ bất ngờ giữa lý thuyết số đại số và hình học rời rạc mà lời giải hé lộ là một phần khiến kết quả này đáng chú ý. Kết quả này không chỉ dừng lại ở việc giải quyết một giả thuyết cụ thể, mà còn có thể trở thành cây cầu giúp các nhà toán học khám phá thêm nhiều vấn đề liên quan khác.

Bloom cũng chỉ ra một khả năng lớn hơn:

“Các ranh giới của tri thức rất gồ ghề và nhọn sắc, và không nghi ngờ gì rằng những tháng và năm tới sẽ chứng kiến những thành công tương tự trong nhiều lĩnh vực toán học khác, nơi mà các bài toán mở tồn tại lâu năm được giải quyết nhờ AI phát hiện ra những kết nối bất ngờ và đẩy giới hạn của các công cụ kỹ thuật hiện có lên đến cực đại. AI đang giúp chúng ta khám phá đầy đủ hơn ngôi thánh đường toán học mà chúng ta đã xây dựng qua hàng thế kỷ; còn những kỳ quan ẩn giấu nào khác đang chờ đợi sau cánh gà?”

Kết quả này mang đến một ví dụ đầy hứa hẹn: AI đóng góp không chỉ một lời giải, mà còn một khám phá toán học mà ý nghĩa của nó trở nên rõ ràng và phong phú hơn nhờ sự thấu hiểu tiếp theo của con người.

Ý nghĩa quan trọng của sự việc này lớn hơn nhiều so với chính kết quả cụ thể ấy. Khả năng suy luận toán học tốt hơn có thể biến AI thành một đối tác nghiên cứu mạnh hơn: một thứ có thể giữ vững các mạch suy nghĩ khó, kết nối ý tưởng giữa những lĩnh vực tri thức xa nhau, làm lộ ra các hướng đi hứa hẹn mà chuyên gia có thể chưa ưu tiên, và giúp các nhà nghiên cứu tiến bộ trên những bài toán vốn quá phức tạp hoặc tốn thời gian để xử lý.

Những năng lực đó quan trọng vượt ra ngoài toán học. Nếu một mô hình có thể giữ cho một lập luận phức tạp mạch lạc, kết nối ý tưởng giữa các lĩnh vực tri thức xa nhau và tạo ra công trình vượt qua được sự thẩm định của chuyên gia, thì đó cũng là những năng lực hữu ích trong sinh học, vật lý, khoa học vật liệu, kỹ thuật và y học, và chúng là một phần trong con đường dài hạn của chúng tôi hướng tới nghiên cứu tự động hóa hơn: các hệ thống có thể giúp nhà khoa học và kỹ sư khám phá nhiều ý tưởng hơn và theo đuổi những câu hỏi kỹ thuật khó hơn.

AI sắp bắt đầu đảm nhận một vai trò rất nghiêm túc trong các phần sáng tạo của nghiên cứu, và quan trọng nhất là chính nghiên cứu AI. Dù tiến bộ này không phải là điều bất ngờ, nó càng nhấn mạnh tính cấp bách mà chúng tôi cảm nhận trong việc hiểu giai đoạn tiếp theo của phát triển AI, những thách thức của việc căn chỉnh các hệ thống rất thông minh, và tương lai của hợp tác giữa con người và AI.

Tương lai đó vẫn phụ thuộc vào phán đoán của con người. Chuyên môn trở nên có giá trị hơn, chứ không hề bớt đi. AI có thể giúp tìm kiếm, gợi ý và xác minh. Con người chọn những bài toán quan trọng, diễn giải kết quả và quyết định nên theo đuổi câu hỏi nào tiếp theo.