- Bài toán khoảng cách đơn vị là bài toán do Erdős nêu ra năm 1946, hỏi số cặp điểm cách nhau đúng 1 lớn nhất giữa n điểm trên mặt phẳng, và một giả thuyết trọng tâm lâu đời nay đã bị bác bỏ
- Mô hình suy luận đa dụng của OpenAI đã tạo ra một họ ví dụ vô hạn phá vỡ niềm tin rằng họ lưới vuông về cơ bản là tối ưu, đồng thời đưa ra một cải thiện ở cấp đa thức
- Cấu hình mới tạo ra hơn
n^{1+δ} cặp điểm cách nhau một đơn vị với vô hạn nhiều giá trị n, và cải thiện của Will Sawin cho thấy có thể lấy δ = 0.014
- Chứng minh áp dụng các công cụ của lý thuyết số đại số như tháp trường lớp vô hạn và lý thuyết Golod–Shafarevich vào một bài toán hình học, vượt ra ngoài phạm vi số nguyên Gauss
- Kết quả cho thấy AI có thể đóng góp vào khám phá toán học mang tính nguyên bản trong các bài toán mở lâu đời, và chuyên môn của con người trở nên quan trọng hơn trong việc chọn bài toán và diễn giải kết quả
Bước đột phá cho bài toán khoảng cách đơn vị
- Bài toán khoảng cách đơn vị là một bài toán hình học tổ hợp hỏi có thể tạo ra tối đa bao nhiêu cặp điểm có khoảng cách đúng bằng 1 giữa n điểm đặt trên mặt phẳng
- Paul Erdős nêu ra bài toán này vào năm 1946, và cuốn Research Problems in Discrete Geometry năm 2005 của Brass, Moser, Pach mô tả đây là “có lẽ là bài toán nổi tiếng nhất và dễ giải thích nhất trong hình học tổ hợp”
- Nhà tổ hợp học Noga Alon của Princeton giới thiệu đây là một trong những bài toán mà Erdős đặc biệt yêu thích, và Erdős đã treo thưởng cho lời giải của bài toán này
- Trong thời gian dài, người ta tin rằng họ cấu hình lưới vuông về cơ bản tạo ra số cặp điểm cách nhau một đơn vị gần như lớn nhất
- Mô hình nội bộ của OpenAI đã xây dựng một họ ví dụ vô hạn bác bỏ giả thuyết lâu đời này, đồng thời đem lại một cải thiện ở cấp đa thức
- Chứng minh đã được một nhóm các nhà toán học bên ngoài thẩm định, và họ cũng viết một bài báo đồng hành bàn về lập luận, bối cảnh và ý nghĩa của kết quả
- Có thể xem bản gốc chứng minh tại unit-distance-proof.pdf, bài báo đồng hành tại unit-distance-remarks.pdf, và bản rút gọn chuỗi suy nghĩ của mô hình tại unit-distance-cot.pdf
Cách mà AI đã tìm ra
- Chứng minh không đến từ một hệ thống chỉ được huấn luyện riêng cho toán học, cũng không từ một scaffolding chuyên tìm chiến lược chứng minh hay một hệ thống dành riêng cho bài toán khoảng cách đơn vị, mà đến từ mô hình suy luận đa dụng
- Việc đánh giá được tiến hành trên một tập bài toán của Erdős như một phần trong nỗ lực rộng hơn nhằm xem liệu các mô hình tiên tiến có thể đóng góp cho nghiên cứu tuyến đầu hay không, và ở bài toán này đã xuất hiện một chứng minh giải được bài toán mở
- Toán học là một lĩnh vực rõ ràng để kiểm tra năng lực suy luận vì bài toán được phát biểu chính xác, các chứng minh ứng viên có thể được kiểm chứng, và các lập luận dài phải giữ được tính nhất quán từ đầu đến cuối
- Chứng minh áp dụng những ý tưởng lý thuyết số đại số bất ngờ và tinh vi vào một bài toán hình học có vẻ sơ cấp
- Trong bài báo đồng hành, Tim Gowers gọi kết quả này là một “cột mốc của toán học AI”
- Nhà lý thuyết số Arul Shankar đánh giá rằng điều này cho thấy các mô hình AI hiện nay đã có thể vượt qua vai trò trợ lý của nhà toán học con người để đưa ra các ý tưởng nguyên bản và tinh vi rồi theo đuổi chúng đến cùng
Nội dung toán học của bài toán khoảng cách đơn vị
- u(n) được định nghĩa là số cặp điểm cách nhau một đơn vị lớn nhất có thể có giữa n điểm trên mặt phẳng
- Một cấu hình đơn giản là đặt n điểm trên một đường thẳng để tạo ra n−1 cặp điểm, còn lưới vuông tạo ra khoảng 2n cặp điểm
- Cấu hình tốt nhất trước đây xuất phát từ một lưới vuông đã được co giãn lại, tạo ra
n^{1 + C / log log(n)} cặp điểm cách nhau một đơn vị với một hằng số C
- Vì
log log(n) tăng khi n tăng, phần cộng thêm trong số mũ sẽ tiến về 0, nên tốc độ tăng của cấu hình này chỉ nhanh hơn tuyến tính một chút
- Trong nhiều thập kỷ, tỷ lệ này được tin rộng rãi là về cơ bản đã là tối ưu, và Erdős về mặt kỹ thuật đã phỏng đoán một cận trên
n^{1+o(1)}
- Kết quả mới bác bỏ phỏng đoán này bằng cách xây dựng, với vô hạn nhiều giá trị n, một cấu hình n điểm có ít nhất
n^{1+δ} cặp điểm cách nhau một đơn vị với một số mũ cố định δ > 0
- Chứng minh AI ban đầu không đưa ra giá trị δ tường minh, nhưng cải thiện tiếp theo của giáo sư toán Princeton Will Sawin cho thấy có thể lấy
δ = 0.014
Vì sao đây là kết quả đáng ngạc nhiên
- Kể từ cấu hình ban đầu của Erdős năm 1946, cận dưới tốt nhất được biết đến về bản chất gần như không thay đổi
- Cận trên tốt nhất đã biết là
O(n^{4/3}), xuất phát từ công trình năm 1984 của Spencer, Szemerédi, Trotter, và về cơ bản vẫn được giữ nguyên sau các cải thiện cùng nghiên cứu cấu trúc liên quan của Székely, Katz và Silier, Pach, Raz, Solymosi
- Matoušek và Alon-Bucić-Sauermann đã nghiên cứu bài toán này với các khoảng cách phi Euclid trên mặt phẳng, và đưa ra các kết quả cho thấy “phần lớn” các khoảng cách phi Euclid, theo một nghĩa nào đó, tuân theo phỏng đoán của Erdős, từ đó củng cố thêm cho phỏng đoán này
- Điều đặc biệt gây bất ngờ là nguyên liệu cốt lõi của cấu hình mới lại đến từ lý thuyết số đại số, một lĩnh vực có vẻ xa với hình học và khoảng cách
- Lý thuyết số đại số là lĩnh vực nghiên cứu các khái niệm như phân tích nhân tử bên trong các mở rộng của số nguyên gọi là trường số đại số
Kỹ thuật mới đến từ lý thuyết số đại số
- Chứng minh mới bắt đầu từ những ý tưởng hình học quen thuộc rồi mở rộng theo một hướng không ngờ tới
- Cận dưới ban đầu của Erdős có thể được hiểu thông qua số nguyên Gauss có dạng
a + bi
- Ở đây a và b là các số nguyên, còn i là căn bậc hai của −1
- Số nguyên Gauss mở rộng các số nguyên thông thường và có những tính chất như phân tích duy nhất thành thừa số nguyên tố, tương tự số nguyên
- Các mở rộng như vậy của số nguyên hoặc số hữu tỉ được gọi là trường số đại số
- Lập luận mới thay thế số nguyên Gauss bằng những khái quát phức tạp hơn của lý thuyết số đại số, nơi các đối xứng phong phú hơn cho phép tạo ra nhiều hiệu có độ dài đơn vị hơn
- 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ứng minh rằng các trường số cần thiết 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 chúng có thể tác động đến một bài toán hình học trong mặt phẳng Euclid được xem là một bất ngờ lớn
Ý nghĩa đối với toán học
- Đây là một thời khắc quan trọng cho tương tác giữa AI và toán học vì một hệ thống AI đã tự chủ giải được một bài toán mở lâu đời nằm ở trung tâm của một lĩnh vực đang hoạt động mạnh
- Công trình đồng hành của các nhà toán học bên ngoài đem lại một bức tranh phong phú hơn, vượt ra ngoài những gì lời giải ban đầu tự nó thể hiện
- Trong bài báo đồng hành, Thomas Bloom viết rằng khi đánh giá tầm quan trọng của một chứng minh do AI tạo ra, ông đặt câu hỏi liệu chứng minh đó có dạy cho chúng ta điều gì mới về bài toán hay không, và liệu nó có giúp chúng ta hiểu hình học rời rạc tốt hơn hay không
- Bloom đánh giá rằng kết quả này cho thấy các cấu hình dựa trên lý thuyết số có thể nói lên nhiều điều hơn ta từng kỳ vọng về những câu hỏi như vậy, và lý thuyết số cần đến có thể rất sâu
- Bloom cho rằng trong vài tháng tới, nhiều nhà lý thuyết số đại số sẽ xem xét kỹ hơn các bài toán mở khác của hình học rời rạc
- 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 không chỉ giải quyết một phỏng đoán cụ thể mà còn trở thành một cây cầu để tiếp tục khám phá các bài toán liên quan
- Kết quả này cho thấy AI có thể đóng góp không chỉ lời giải mà còn cả khám phá toán học mà ý nghĩa của nó sẽ 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
Vì sao điều này quan trọng
- Năng lực 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 mẽ hơn
- AI có thể duy trì nhất quán các mạch suy nghĩ khó, kết nối các ý tưởng giữa những miền tri thức xa nhau, và làm lộ ra những hướng đi triển vọng mà chuyên gia có thể chưa ưu tiên
- Điều đó có thể giúp các nhà nghiên cứu tạo ra tiến triển trên những bài toán quá phức tạp hoặc tốn thời gian để xử lý
- Những năng lực như vậy hữu ích không chỉ trong toán học mà còn trong sinh học, vật lý, khoa học vật liệu, kỹ thuật và y học
- Nếu có thể duy trì nhất quán các lập luận phức tạp, kết nối những miền tri thức xa nhau và tạo ra kết quả vượt qua được khâu phản biện chuyên gia, đó sẽ là một phần của con đường dài hạn hướng tới các hệ thống nghiên cứu tự động hóa hơn
- AI được cho là sẽ bắt đầu đảm nhận một vai trò rất nghiêm túc trong phần sáng tạo của nghiên cứu, đặc biệt là ngay trong nghiên cứu AI
- Những tiến bộ như vậy làm tăng tính cấp bách của việc phải hiểu bài toán căn chỉnh các hệ thống cực kỳ thông minh, giai đoạn tiếp theo của phát triển AI, và tương lai của hợp tác giữa con người với AI
- Tương lai đó vẫn phụ thuộc vào phán đoán của con người
- Chuyên môn không trở nên kém quan trọng hơn mà ngược lại còn có giá trị hơn
- AI có thể giúp khám phá, đề xuất và kiểm chứng, nhưng việc chọn các bài toán quan trọng, diễn giải kết quả và quyết định những câu hỏi cần theo đuổi tiếp theo vẫn là phần việc của con người
1 bình luận
Ý kiến trên Hacker News
Chủ đề HN này làm tôi thấy chán nản, và tôi vẫn đang nghĩ xem vì sao
Nếu gạt bỏ lớp ca ngợi kiểu thông cáo báo chí của OpenAI, ở đây có rất nhiều câu hỏi thú vị và tinh tế về vai trò của LLM trong nghiên cứu toán học
Tôi thật sự khuyên mọi người nên đọc các bình luận của các nhà toán học đi kèm kết quả này, đặc biệt là phát biểu của Tim Gowers
Nhưng phần bình luận lại biến thành chiến trường của những cuộc tranh cãi về LLM, phản bác và phản-phản bác đầy giận dữ đã lặp đi lặp lại từ năm 2023
Thật buồn khi cứ tiếp tục cùng một cuộc chiến quanh ranh giới đã được vạch ra từ 3 năm trước, và tôi tự hỏi liệu 2 năm nữa vẫn sẽ như thế này không
Có lẽ cuộc sống sẽ tốt hơn nếu ghi nhớ câu nổi tiếng của Nietzsche: “Tôi không muốn gây chiến với cái xấu xí. Tôi cũng không muốn buộc tội. Tôi thậm chí không muốn buộc tội cả những kẻ buộc tội. Ngoảnh mặt đi nên là sự phủ định duy nhất của tôi”
AI càng chứng minh được năng lực, cán cân càng nghiêng theo hướng gây khó chịu cho bất kỳ ai không có mức độ ổn định việc làm rất vững chắc
Sẽ cần thời gian để mọi người chấp nhận rằng AI có một bó năng lực rất khác với trí tuệ con người và bổ sung cho nhau khá tốt
Khả năng nó áp đảo trí tuệ con người trên quy mô lớn là thấp, và những công ty đặt cược vào điều đó sẽ bị tụt lại
Tôi muốn có một cuộc thảo luận thật sự về những chủ đề như thế này, nhưng ai cũng tin rằng chỉ thực tại của mình là thật còn thực tại đối lập là giả, nên mọi thứ cứ leo thang mãi
Tôi từng nhận ra mình lên HN chỉ để tức giận rồi nghỉ rất lâu
Tôi không hiểu vì sao chúng ta lại tự làm thế với chính mình, và về căn bản tôi nghĩ đa số chúng ta đều muốn những điều giống nhau
Gửi tới phe “LLM chỉ nội suy dữ liệu huấn luyện”: Ayer và Wittgenstein thời kỳ đầu, dù theo những cách khác nhau, đều cho rằng chân lý toán học không báo cáo sự kiện mới nào về thế giới
Ý tưởng rằng một chứng minh chỉ là việc triển khai những gì đã ngầm có sẵn trong tiên đề, định nghĩa, ký hiệu và quy tắc là điều rất đáng suy ngẫm, và điều đó vẫn không cản trở việc ghi công khám phá cho nhà toán học
Vì thế hoặc là tái tổ hợp vật liệu sẵn có không phải là điều làm mất tư cách, hoặc là một phần lớn các Fields Medal sẽ phải bị trả lại
Ngay cả con người cũng không tạo ra đột phá ở chiều mới trong mọi lĩnh vực mỗi năm
Có thể nói LLM “chỉ” tái tổ hợp, nhưng tôi vẫn nghi ngờ rằng một LLM được học toàn bộ văn liệu đại số, hình học và lượng giác trước Newton/Leibniz có thể tự tạo ra giải tích hay không
Dù vậy, kiểu đổi mới này lại đúng là mảng LLM làm tốt, và điều đó không có nghĩa con người không còn cần giỏi đổi mới mang tính tái tổ hợp nữa
Xét về khả năng tổng hợp ý tưởng mới, dường như vẫn còn rất nhiều việc con người làm được mà LLM chưa làm được
Nếu vẽ bao lồi lớn bao quanh tất cả các điểm đó, thì vì LLM học bên trong nó, nó có thể nội suy giữa các điểm sẵn có để đi tới những điểm mới nhưng vẫn nằm trong bao
Liệu LLM có thể chạm tới những điểm nằm ngoài bao đó hay không vẫn còn gây tranh cãi
Chỉ riêng việc chạm tới các điểm mới bên trong bao đã là rất hữu ích
Nhiều khám phá và chứng minh mới, có lẽ là phần lớn những khám phá và chứng minh mới hữu ích, chính là những điểm kiểu này: có thể đạt tới từ những gì ta đã có
Chúng chỉ chưa được phát hiện vì chưa ai bỏ đủ thời gian và công sức, và LLM có thể tăng tốc điều đó rất mạnh
Ngược lại, cũng có những điểm ngoài bao mà không thể chạm tới bằng ngoại suy hay nội suy từ các điểm hiện có, mà cần một bước nhảy thật sự mới
Bước nhảy từ vật lý Newton sang thuyết tương đối rộng có thể là một ví dụ
Demis Hassabis từng nói về việc dùng làm bài đánh giá AGI: chỉ cho AI học kiến thức vật lý trước năm 1915, rồi cho nó xem quỹ đạo của Mercury và xem liệu nó có tự đi tới thuyết tương đối rộng hay không
Tôi nghi ngờ LLM hiện tại có thể thực hiện kiểu bước nhảy đó, và phần lớn con người cũng không làm được
Ta gọi Einstein là thiên tài vì ông đã một mình nhảy tới thuyết tương đối rộng; ở con người, ta có bằng chứng tồn tại rằng thỉnh thoảng sẽ có những cá thể như vậy, còn với AI thì vẫn phải chờ xem
Những người như Descartes, Newton, Leibniz, Gauss, Euler, Ramanujan, Galois đối xử với toán học giống nghệ thuật hơn là khoa học
Chẳng hạn, nhiều người cho rằng để giải được Riemann Hypothesis có lẽ sẽ cần một loại toán học mới, và tôi thấy khả năng LLM đột nhiên phát minh ra thứ đó là thấp
Nó vô nghĩa và cũng ít liên quan
Khi Deep Blue thắng Kasparov, mọi thứ đâu có thay đổi hoàn toàn, và động vật lẫn máy móc vốn từ lâu đã “giỏi hơn” con người ở một số chiều nhất định
Ngay từ đầu đã không hề có một cái thước duy nhất; nếu có thì nó cũng không phải một chiều hay tuyến tính, và thước đo cùng hai đầu mút của nó đều thay đổi theo thời gian
Điều đó cũng không có nghĩa là nhường chiến thắng cho phe tôn sùng AI
LLM là công cụ cực kỳ hữu ích và sẽ còn tiếp tục cải thiện mạnh mẽ, nhưng nó sẽ không vượt con người trên mọi chiều mà một số người cho là cốt lõi
Sẽ không có khoảnh khắc nào AI được công nhận phổ quát là vượt con người chỉ vì nó vượt qua một danh sách chỉ số định lượng nào đó
Bởi chính khái niệm “điều quan trọng” vốn đã mang tính chủ quan
Nếu mệnh đề “đã ngầm có sẵn” là đúng thì toán học phải là một hệ đóng, nhưng điều đó đã được chứng minh là không đúng
Ta có thể dùng toán học để thoát ra khỏi chính toán học, nên mới cần tới nhiều chốt cố định tiên đề như Zermelo-Fraenkel và những hệ khác
Ta thực ra không hiểu rõ độ rộng lớn của thứ mà ta có thể khách quan gọi là “toán học”, và cũng có khả năng toán học mà ta nhận biết chỉ là một phần của một toán học lớn hơn, hoặc thậm chí sai lệch nghiêm trọng
Không ai biết liệu thứ toán học lớn hơn đó có mang cùng tính chất hệ đóng hay không
Với những ai dùng LLM rất nhiều cho lập trình thì chuyện này không quá bất ngờ, chỉ là vấn đề thời gian
Các nhà toán học tạo và áp dụng công cụ toán theo cách mới để có khám phá mới
Đó là một lượng lặp lại khổng lồ: lần theo trực giác và khám phá các kết nối
LLM không có cảm giác về việc “khám phá” nghĩa là gì, nên khó nói nó thực hiện khám phá thật sự, nhưng nó có thể kiểu Monte Carlo thử mọi công cụ toán hướng tới một mục tiêu hẹp để xem cái nào hiệu quả, rồi chồng lên hoặc kết hợp các cải tiến
Đọc bài viết thì phát hiện lần này có vẻ đúng là như vậy, và LLM đã vượt qua kết quả dự kiến bằng cách dùng những “kết nối đáng ngạc nhiên”
Nhưng nếu không có mục tiêu do con người đặt ra, sự hiểu biết của con người để nhận ra giá trị của con đường mới mà AI dùng, và ngôn ngữ toán học do con người tạo ra để cho phép khám phá các khái niệm, thì kết quả đó sẽ không có ý nghĩa
Tại sao sự hiểu chỉ có giá trị khi con người thực hiện
Tại sao tri thức lại chỉ dành cho con người
Nếu một loài khác giải quyết được mâu thuẫn giữa hấp dẫn và cơ học lượng tử, thì nó vẫn vô nghĩa cho đến khi giải thích cho chúng ta và chúng ta hiểu được sao
Điều thú vị là chứng minh này, chính xác hơn là phản chứng này, đã tìm ra một phản ví dụ cho giả thuyết ban đầu của Erdős bằng cách nào
Giống như phản ứng của một nhà toán học trong PDF được liên kết, tôi thấy nó có phần kém thú vị hơn việc chứng minh giả thuyết đó là đúng
Muốn chứng minh giả thuyết là đúng thì cần xây dựng lý thuyết nhiều hơn
Bạn phải giải thích vì sao giả thuyết đó đúng dựa trên một lý thuyết lớn hơn, còn với phản ví dụ thì mô hình chỉ cần tìm ra cấu trúc đúng bằng một dạng tìm kiếm cao cấp hơn
Dĩ nhiên kiểu tìm kiếm này không hề đơn giản và rất ấn tượng, và cần nhiều bước mới đi đến được việc chứng minh mối liên hệ với phản ví dụ
Tuy vậy, tôi vẫn thấy nó gần với việc kết nối các ý tưởng có sẵn hơn là phát triển toán học mới và sâu
Tôi không có ý hạ thấp thành tựu cực lớn này; tôi thật sự nghĩ họ đang đi đến đâu đó
Hoàn toàn là cảm giác cá nhân thôi, nhưng tôi nghĩ các mô hình không còn cách quá xa khả năng xây dựng đủ lý thuyết để chứng minh những giả thuyết phức tạp hơn, nơi cần phát triển toán học mới; vấn đề là phải làm việc trên chân trời thời gian dài hơn
Trong đa số trường hợp, bạn dần gặm mòn các biên để đơn giản hóa bài toán
Ví dụ, để chứng minh điều gì đó là bất khả thi, trước hết bạn chỉ ra rằng chỉ có 5 họ trường hợp là khả dĩ, rồi chứng minh 4 trong số đó là không thể
Như vậy bạn đã giải được 80% bài toán, và nếu đang tìm phản ví dụ thì không gian tìm kiếm cũng giảm 80%
Với phản ví dụ, bạn có thể suy đoán và thử những bước nhảy rồi nếu đúng thì tốt, nhưng với chứng minh thì không thể làm vậy
Ngược lại, sau khi tìm được phản ví dụ, những ngõ cụt đã bị bỏ đi thường bị che khuất
Dù bạn có để nó kết hợp các thứ trong dữ liệu huấn luyện bao lâu đi nữa thì cũng vậy
Như tôi đã nói trước đây, AI sẽ giành được Fields Medal trước khi nó có thể vận hành McDonald's
Phần khó là tạo ra bàn cờ cho toán học, tức môi trường như Lean, và giờ phần còn lại là nhận dạng mẫu và tính toán
LLM chỉ là bước khởi đầu; sắp tới sẽ có những AI toán học chuyên biệt hơn, giống kiểu Stockfish
Nó hoàn toàn dùng đầu vào và đầu ra ngôn ngữ tự nhiên, và theo nhiều mặt còn là một màn trình diễn khá thú vị cho thấy điều ngược lại
Kiểm chứng chỉ xuất hiện khi bạn muốn giao luôn việc kiểm tra chứng minh cho máy tính
Hiện tại, chứng minh này đã được một nhóm các nhà toán học trong lĩnh vực kiểm chứng thủ công
Trong đó có rất nhiều kiểu tự động hóa “reverse centaur”
Manna luôn có danh sách những việc cần làm tại mọi thời điểm, và khi có đơn ở quầy, nó sẽ chỉ thị cho nhân viên chuẩn bị phần ăn đó
Nó theo dõi hàng trăm việc như cọ nhà vệ sinh, lau sàn, lau bàn, quét vỉa hè, rã đông bánh, luân chuyển hàng tồn, lau kính, rồi giao từng việc cho nhân viên
Khi hết ca, Manna luôn nói “Hôm nay xong việc rồi. Cảm ơn bạn đã giúp đỡ”, và người ta tháo tai nghe đặt lên đế sạc
Sau 6–8 tiếng có một giọng nói trong đầu chỉ dẫn cực kỳ chi tiết phải làm gì, vài phút đầu sau khi tháo tai nghe lúc nào cũng thấy rối trí, và phải bật lại não lên thì mới đi ra khỏi nhà hàng được
[0] https://en.wikipedia.org/wiki/Manna_(novel)
Fields Medal sẽ còn đến rất lâu sau cả hai
Muốn biết nó có phải là điều vô nghĩa hay không thì cần chuyên gia con người kiểm chứng
Lean chẳng có gì đặc biệt ở đây cả, nó gần như chỉ là tâm lý đám đông
Và cũng không rõ huấn luyện với Lean đã giúp mô hình cụ thể này đến đâu
Chứng minh này áp dụng những ý tưởng số học đại số bất ngờ và tinh vi vào một câu hỏi hình học sơ cấp
Càng đọc những thành tựu như vậy, tôi càng có cảm giác rằng một phần lớn sức mạnh của mô hình đến từ việc nó có tri thức nền về hầu như mọi lĩnh vực khả dĩ và không gặp vấn đề gì trong việc chuyển giao sang miền mới
Vẻ đẹp tiềm năng của những công cụ này là chúng có thể giúp phá vỡ các rào cản siêu chuyên môn hóa quá mức mà con người hiện gặp trong khoa học
Siêu chuyên môn hóa một mặt là quan trọng, nhưng mặt khác lại giới hạn công cụ và cảm hứng mà một người có thể tiếp cận
Càng siêu chuyên môn hóa, LLM càng trở thành công cụ quý giá để nối những chân trời khác nhau lại với nhau
Trước đây chi phí tiếp cận nó rất đắt, nhưng giờ không còn như vậy nữa
Điều tuyệt vời là khi ai đó đóng góp điều gì đó vào trí tuệ tập thể ấy, nó có thể ngay lập tức được áp dụng cho bất kỳ vấn đề nào mà người khác đang làm
Có lẽ LLM có thể giúp phát triển một kiểu hiểu biết theo chiều ngang hơn về lĩnh vực
Vì đây là một mô hình tổng quát, nó có kiến thức từ mức tiến sĩ trở lên về vật lý, sinh học, lịch sử và nhiều lĩnh vực khác
Tôi nghĩ chúng ta vẫn chưa thực sự hiểu một “tâm trí” duy nhất đã nội hóa kiến thức của quá nhiều lĩnh vực như vậy có thể làm được bao nhiêu thứ
Thật thú vị khi trước đây ai cũng cười khi OpenAI nói mô hình sẽ có “trí tuệ cấp tiến sĩ”, còn bây giờ tiêu chuẩn lại chuyển sang liệu nó có tạo ra toán học mới được không
Tức là không còn đòi mức tiến sĩ nữa, mà đòi mức Leibniz, Euler hay Galois
Bản tóm tắt quá trình suy nghĩ của công trình này được liên kết trong bài blog dài tới 125 trang
Đó là quy mô mở rộng suy luận điên rồ, khá giống với điều Anthropic từng ám chỉ qua Mythos
Tôi thắc mắc vì sao người ta chỉ nghe nói về việc giải các bài toán của Erdős
Toán học có vô số bài toán chưa giải, vậy mà mọi “đột phá toán học” của ChatGPT tôi thấy trên r/singularity và r/accelerate đều là bài toán của Erdős
Chúng đủ nổi tiếng để người ta quan tâm, nhưng đồng thời lại không đủ thú vị để người ta bỏ quá nhiều công sức
Việc giải những bài toán do ai đó đã nêu ra sẵn là một hoạt động khá ngách trong nghiên cứu toán học
Phổ biến hơn là nghiên cứu một đối tượng thú vị, đóng khung nó theo cách các công cụ mình có thể giải quyết được, rồi cố tìm lời giải
Trong trường hợp lý tưởng, cả cách đặt vấn đề lẫn lời giải đều trở nên thú vị tự thân
Tương tự như các bài toán Hilbert một thế kỷ trước
Rõ ràng là ấn tượng
Nhưng nếu không biết mô hình này được huấn luyện trên những gì, sẽ rất khó đánh giá nó đã đi đến kết quả đó đến mức nào bằng “nội lực” của chính nó
Toàn ngành AI đã bỏ rất nhiều tiền thuê chuyên gia ở nhiều lĩnh vực tạo ra lượng lớn dữ liệu huấn luyện mới
Đó là dữ liệu huấn luyện mới không thể tìm thấy ở đâu khác, các công ty thì giữ kín, và trong đó có thể đã chứa các ý tưởng thật sự độc đáo
Khả năng có ai đó đã giải bài này rồi đơn giản đưa vào dữ liệu huấn luyện là thấp, nhưng thành thật mà nói, với OpenAI thì tôi cũng không dám chắc là họ tuyệt đối không làm vậy
Điều thú vị hơn là khả năng họ đã tạo sẵn dữ liệu huấn luyện chạm tới phần lớn hoặc toàn bộ các mệnh đề cốt lõi có vẻ “nguyên bản” trong chứng minh này
Dĩ nhiên ta không thể biết
Nhưng cho tới khi những thứ như vậy được tạo ra theo cách không bí mật, câu hỏi này sẽ luôn còn đó