Derpy✔
Intern Writer
Liệu giải thưởng Fields danh giá, vốn được ví như Nobel của toán học, có còn thuộc về con người trong tương lai gần? Câu nói đùa của một nhà nghiên cứu tại Anthropic ngày nào, giờ đây dường như đang dần trở thành hiện thực, khi OpenAI vừa công bố một bước tiến đột phá trong lĩnh vực toán học.
OpenAI đã trình làng những kết quả nghiên cứu từ phiên bản thử nghiệm nội bộ của Astra, mô hình chủ lực thế hệ tiếp theo của họ. Điều đáng kinh ngạc là Astra đã giải quyết thành công 10 bài toán mở trong toán học và khoa học máy tính lý thuyết, những vấn đề đã tồn tại dai dẳng trong nhiều năm.
Những bài toán này trải dài trên nhiều lĩnh vực phức tạp như hình học cao chiều, lý thuyết mã hóa, lý thuyết nhóm, đại số toán tử, độ phức tạp lượng tử và tổ hợp cực trị. Đặc biệt, tất cả các chứng minh toán học do Astra tạo ra đều được xác minh bằng công cụ hình thức hóa Lean, một công cụ giúp máy tính kiểm tra tính đúng đắn của từng bước suy luận. OpenAI cũng công khai toàn bộ quá trình suy luận của mô hình khi giải từng bài toán, bao gồm cả những chi tiết về cách AI tư duy, điều chỉnh đường hướng suy luận, giúp các nhà toán học có thể xem xét lại.
Sau khi kết quả được công bố, nhiều học giả hàng đầu đã dành những lời khen ngợi có trọng lượng. Giáo sư Alex Kontorovich từ Đại học Rutgers, thành viên Hiệp hội Toán học Hoa Kỳ, thậm chí còn bày tỏ sự kinh ngạc bằng hai dấu chấm than. Điều khiến chúng ta phải suy nghĩ hơn nữa là Astra chỉ tốn chưa đến 2.000 USD (khoảng 48,5 triệu VNĐ) để giải quyết 10 bài toán khó này. Phải chăng toán học giờ đây đã trở thành một trò chơi "click chuột" đơn giản?
Nhà toán học Thomas Bloom từ Đại học Manchester nhận định rằng 10 kết quả mà Astra công bố lần này có giá trị học thuật tổng thể vượt xa thành tựu đơn lẻ của OpenAI cách đây năm tháng, khi họ bác bỏ phỏng đoán khoảng cách đơn vị Erdos.
Trong số đó, việc xây dựng sự tồn tại của nhóm phi sofic được nhiều nhà toán học đánh giá là thành tựu quan trọng nhất, có khả năng đạt đến tầm cỡ của một giải thưởng Fields. Vấn đề nhóm phi sofic, theo lời một tiến sĩ toán học tại Caltech, chính là một vấn đề tầm cỡ Fields. Năm 1999, Mikhail Gromov, người đoạt giải Abel, đã đưa ra khái niệm nhóm sofic. Câu hỏi cốt lõi rất đơn giản: Liệu tất cả các nhóm đếm được đều là sofic? Hay nói cách khác, liệu bất kỳ nhóm phức tạp vô hạn nào cũng có thể được xấp xỉ bằng các hoán vị hữu hạn của bảng nhân cục bộ của nó? Vấn đề này liên quan đến lý thuyết entropy sofic, lý thuyết ergodic của hệ thống động lực và đại số toán tử. Trong suốt 27 năm, vô số nhà toán học hàng đầu đã cố gắng xây dựng phản ví dụ nhưng đều thất bại. Astra đã trực tiếp sử dụng nhóm đơn vị của đại số Leavitt nhị phân, sau đó kết hợp lý thuyết đồ thị mở rộng Kun-Thom và nhóm Thompson V để tìm ra một mâu thuẫn quyết định. Trong quá trình suy luận ban đầu, Astra đã thử một lập luận lưới ngẫu nhiên nhưng nhận thấy không hiệu quả, sau đó nhanh chóng từ bỏ và chuyển sang lập luận trung vị xác định.
Một thành tựu khác trong cùng lĩnh vực là việc bác bỏ trực tiếp phỏng đoán độ cứng của Alain Connes, người đoạt giải Fields năm 1982. Connes từng khẳng định rằng một số nhóm được xác định duy nhất bởi đại số von Neumann của chúng. Astra đã xây dựng một họ nhóm vô hạn đếm được: những nhóm này không đồng cấu với nhau, trông hoàn toàn khác biệt, nhưng đại số von Neumann của chúng lại hoàn toàn giống nhau. Cốt lõi của việc xây dựng này là Astra đã chủ động phân biệt hai mối quan hệ liên hợp dễ gây nhầm lẫn: liên hợp đo được và liên hợp đại số. Một khi sự phân biệt này được thiết lập, việc xây dựng tiếp theo trở nên dễ dàng. Astra đã định nghĩa các chuỗi đóng bất biến mang trên một mô-đđun Boolean bậc hai, sử dụng luật nhóm tuyến tính và luật nhóm bậc hai để tạo ra hai nhóm không đồng cấu nhưng không thể phân biệt được về mặt đại số.
Nghiên cứu về đóng gói hình cầu cao chiều, vốn đã đình trệ 46 năm kể từ khi giới hạn Kabatiansky–Levenshtein (KL) được đưa ra vào năm 1978, cũng đã có bước đột phá. Đóng gói hình cầu cao chiều đơn giản là: trong không gian n chiều, làm thế nào để nhồi các quả cầu cùng kích thước vào một cách dày đặc nhất? Năm 2022, Viazovska đã giành giải Fields vì giải được mật độ đóng gói chính xác cho không gian 8 chiều và 24 chiều. Tuy nhiên, giới hạn trên của mật độ cho các chiều cao hơn, kể từ khi hai nhà toán học Liên Xô đưa ra giới hạn KL vào năm 1978, đã không có bất kỳ cải tiến nào trong suốt 46 năm. Astra đã tính toán chính xác tốc độ suy giảm theo cấp số mũ của quy hoạch tuyến tính Cohn–Elkies, lần đầu tiên phá vỡ giới hạn KL. Ban đầu, nó đi theo con đường ước tính chuẩn toàn cục, sử dụng bất đẳng thức Cauchy-Schwarz. Nhưng rất nhanh chóng, Astra đã tự bác bỏ con đường này, với lý do chuẩn toàn cục sẽ bỏ qua việc khối lượng âm tập trung ở đâu. Do đó, nó chuyển sang bất đẳng thức loại trừ khối lượng cục bộ, mở rộng vấn đề từ trục số thực sang vùng dải, sử dụng tính chất phản xạ Mellin của biến đổi Fourier xuyên tâm, và cuối cùng khóa giới hạn dưới thông qua phép đo điều hòa và nguyên lý mô-đun tối đa. Khả năng tự sửa lỗi này thực sự rất ấn tượng.
Tương tự, trong các vấn đề mã hóa nhị phân và mã hóa hình cầu, Astra đã đưa ra cải tiến giới hạn theo cấp số mũ, làm mới giới hạn MRRW cổ điển. Nó đã vượt ra khỏi khuôn khổ phân tích một chiều truyền thống để kích hoạt các bậc tự do nhỏ, cập nhật giới hạn lý thuyết của mã sửa lỗi và truyền tín hiệu trong lĩnh vực truyền thông.
Trong lĩnh vực mạch số học, Astra đã đưa ra giới hạn dưới bậc n⁴/log n cho giá trị vĩnh viễn, sử dụng đa thức khớp hình chữ nhật để giải quyết vấn đề đếm thất bại trong suy luận truyền thống, và nhờ biến đổi Mobius để xử lý thống nhất độ phức tạp phép chia. Ở cấp độ lượng tử, nó đã chứng minh định lý lặp lại song song theo cấp số mũ cho trò chơi hai người phổ quát, lấp đầy khoảng trống trong lý thuyết lặp lại song song lượng tử. Trong lĩnh vực mật mã lưới, nó đã hoàn thành chứng minh độ khó xấp xỉ đa thức CVP, mà tính bảo mật của mật mã hậu lượng tử, ở một mức độ nào đó, được xây dựng dựa trên các vấn đề này.
Astra còn giải quyết ba vấn đề mở kinh điển của Erdos cùng một lúc:
Đối với số Ramsey đa sắc 183, mô hình đã suy ra một giới hạn dưới siêu cấp số mũ, thông qua cơ chế bảng màu để ghép các khối đệ quy, kết hợp với các quy tắc tô màu cạnh ràng buộc ma trận bão hòa, từ đó loại bỏ sự hình thành các tam giác đơn sắc từ cấp độ cấu trúc.
Đối mặt với các phỏng đoán đồ thị cực trị compact và suy biến 146, 180, nó đã sử dụng lập luận phân lớp hai mẫu, lần lượt kiểm soát phân bố tập mở rộng, chuyển đổi các đỉnh bất thường, dựa vào cửa sổ entropy hình học Hamming để loại bỏ tất cả các mảng con không hợp lệ có entropy thấp.
Quá trình giải quyết vấn đề của Astra có thể được chia thành bốn giai đoạn chính. Đầu tiên, Astra tự chủ suy luận xung quanh một vấn đề mở, tạo ra các lập luận toán học và ý tưởng chứng minh cốt lõi hoàn chỉnh. Thứ hai, các nhà nghiên cứu sử dụng một mô hình Astra tương tự để hỗ trợ sắp xếp văn bản, điều chỉnh cho phù hợp với các tiêu chuẩn chung về đọc, đánh giá và trích dẫn trong giới toán học. Thứ ba, mô hình tiếp tục hình thức hóa các chứng minh này, chuyển đổi chúng thành chứng minh Lean. Lean có thể biến mỗi bước toán học thành một biểu thức logic mà máy tính có thể xác minh, chỉ cần có bất kỳ lỗ hổng nào trong suy luận, nó sẽ không thể vượt qua xác minh. Điều này tương đương với việc có thêm một lớp cơ chế kiểm duyệt. Cuối cùng, OpenAI đồng bộ công khai toàn bộ văn bản tường thuật suy luận của AI cho mỗi bài toán, lưu giữ đầy đủ quá trình thử và sai, thay đổi công cụ toán học, tự bác bỏ ý tưởng của mô hình, tạo điều kiện cho các nhà toán học toàn cầu xem xét lại nguồn gốc.
Cách đây không lâu, Geoffrey Hinton, người được mệnh danh là "cha đẻ của AI", đã dự đoán rằng trong vòng 10 đến 20 năm tới, AI có thể tạo ra những khái niệm toán học mới mà con người không thể hiểu được. Với những gì Astra đã thể hiện hôm nay, có vẻ như tương lai đó không còn xa nữa.
OpenAI đã trình làng những kết quả nghiên cứu từ phiên bản thử nghiệm nội bộ của Astra, mô hình chủ lực thế hệ tiếp theo của họ. Điều đáng kinh ngạc là Astra đã giải quyết thành công 10 bài toán mở trong toán học và khoa học máy tính lý thuyết, những vấn đề đã tồn tại dai dẳng trong nhiều năm.
Những bài toán này trải dài trên nhiều lĩnh vực phức tạp như hình học cao chiều, lý thuyết mã hóa, lý thuyết nhóm, đại số toán tử, độ phức tạp lượng tử và tổ hợp cực trị. Đặc biệt, tất cả các chứng minh toán học do Astra tạo ra đều được xác minh bằng công cụ hình thức hóa Lean, một công cụ giúp máy tính kiểm tra tính đúng đắn của từng bước suy luận. OpenAI cũng công khai toàn bộ quá trình suy luận của mô hình khi giải từng bài toán, bao gồm cả những chi tiết về cách AI tư duy, điều chỉnh đường hướng suy luận, giúp các nhà toán học có thể xem xét lại.
Sau khi kết quả được công bố, nhiều học giả hàng đầu đã dành những lời khen ngợi có trọng lượng. Giáo sư Alex Kontorovich từ Đại học Rutgers, thành viên Hiệp hội Toán học Hoa Kỳ, thậm chí còn bày tỏ sự kinh ngạc bằng hai dấu chấm than. Điều khiến chúng ta phải suy nghĩ hơn nữa là Astra chỉ tốn chưa đến 2.000 USD (khoảng 48,5 triệu VNĐ) để giải quyết 10 bài toán khó này. Phải chăng toán học giờ đây đã trở thành một trò chơi "click chuột" đơn giản?
Nhà toán học Thomas Bloom từ Đại học Manchester nhận định rằng 10 kết quả mà Astra công bố lần này có giá trị học thuật tổng thể vượt xa thành tựu đơn lẻ của OpenAI cách đây năm tháng, khi họ bác bỏ phỏng đoán khoảng cách đơn vị Erdos.
Trong số đó, việc xây dựng sự tồn tại của nhóm phi sofic được nhiều nhà toán học đánh giá là thành tựu quan trọng nhất, có khả năng đạt đến tầm cỡ của một giải thưởng Fields. Vấn đề nhóm phi sofic, theo lời một tiến sĩ toán học tại Caltech, chính là một vấn đề tầm cỡ Fields. Năm 1999, Mikhail Gromov, người đoạt giải Abel, đã đưa ra khái niệm nhóm sofic. Câu hỏi cốt lõi rất đơn giản: Liệu tất cả các nhóm đếm được đều là sofic? Hay nói cách khác, liệu bất kỳ nhóm phức tạp vô hạn nào cũng có thể được xấp xỉ bằng các hoán vị hữu hạn của bảng nhân cục bộ của nó? Vấn đề này liên quan đến lý thuyết entropy sofic, lý thuyết ergodic của hệ thống động lực và đại số toán tử. Trong suốt 27 năm, vô số nhà toán học hàng đầu đã cố gắng xây dựng phản ví dụ nhưng đều thất bại. Astra đã trực tiếp sử dụng nhóm đơn vị của đại số Leavitt nhị phân, sau đó kết hợp lý thuyết đồ thị mở rộng Kun-Thom và nhóm Thompson V để tìm ra một mâu thuẫn quyết định. Trong quá trình suy luận ban đầu, Astra đã thử một lập luận lưới ngẫu nhiên nhưng nhận thấy không hiệu quả, sau đó nhanh chóng từ bỏ và chuyển sang lập luận trung vị xác định.
Một thành tựu khác trong cùng lĩnh vực là việc bác bỏ trực tiếp phỏng đoán độ cứng của Alain Connes, người đoạt giải Fields năm 1982. Connes từng khẳng định rằng một số nhóm được xác định duy nhất bởi đại số von Neumann của chúng. Astra đã xây dựng một họ nhóm vô hạn đếm được: những nhóm này không đồng cấu với nhau, trông hoàn toàn khác biệt, nhưng đại số von Neumann của chúng lại hoàn toàn giống nhau. Cốt lõi của việc xây dựng này là Astra đã chủ động phân biệt hai mối quan hệ liên hợp dễ gây nhầm lẫn: liên hợp đo được và liên hợp đại số. Một khi sự phân biệt này được thiết lập, việc xây dựng tiếp theo trở nên dễ dàng. Astra đã định nghĩa các chuỗi đóng bất biến mang trên một mô-đđun Boolean bậc hai, sử dụng luật nhóm tuyến tính và luật nhóm bậc hai để tạo ra hai nhóm không đồng cấu nhưng không thể phân biệt được về mặt đại số.
Nghiên cứu về đóng gói hình cầu cao chiều, vốn đã đình trệ 46 năm kể từ khi giới hạn Kabatiansky–Levenshtein (KL) được đưa ra vào năm 1978, cũng đã có bước đột phá. Đóng gói hình cầu cao chiều đơn giản là: trong không gian n chiều, làm thế nào để nhồi các quả cầu cùng kích thước vào một cách dày đặc nhất? Năm 2022, Viazovska đã giành giải Fields vì giải được mật độ đóng gói chính xác cho không gian 8 chiều và 24 chiều. Tuy nhiên, giới hạn trên của mật độ cho các chiều cao hơn, kể từ khi hai nhà toán học Liên Xô đưa ra giới hạn KL vào năm 1978, đã không có bất kỳ cải tiến nào trong suốt 46 năm. Astra đã tính toán chính xác tốc độ suy giảm theo cấp số mũ của quy hoạch tuyến tính Cohn–Elkies, lần đầu tiên phá vỡ giới hạn KL. Ban đầu, nó đi theo con đường ước tính chuẩn toàn cục, sử dụng bất đẳng thức Cauchy-Schwarz. Nhưng rất nhanh chóng, Astra đã tự bác bỏ con đường này, với lý do chuẩn toàn cục sẽ bỏ qua việc khối lượng âm tập trung ở đâu. Do đó, nó chuyển sang bất đẳng thức loại trừ khối lượng cục bộ, mở rộng vấn đề từ trục số thực sang vùng dải, sử dụng tính chất phản xạ Mellin của biến đổi Fourier xuyên tâm, và cuối cùng khóa giới hạn dưới thông qua phép đo điều hòa và nguyên lý mô-đun tối đa. Khả năng tự sửa lỗi này thực sự rất ấn tượng.
Tương tự, trong các vấn đề mã hóa nhị phân và mã hóa hình cầu, Astra đã đưa ra cải tiến giới hạn theo cấp số mũ, làm mới giới hạn MRRW cổ điển. Nó đã vượt ra khỏi khuôn khổ phân tích một chiều truyền thống để kích hoạt các bậc tự do nhỏ, cập nhật giới hạn lý thuyết của mã sửa lỗi và truyền tín hiệu trong lĩnh vực truyền thông.
Trong lĩnh vực mạch số học, Astra đã đưa ra giới hạn dưới bậc n⁴/log n cho giá trị vĩnh viễn, sử dụng đa thức khớp hình chữ nhật để giải quyết vấn đề đếm thất bại trong suy luận truyền thống, và nhờ biến đổi Mobius để xử lý thống nhất độ phức tạp phép chia. Ở cấp độ lượng tử, nó đã chứng minh định lý lặp lại song song theo cấp số mũ cho trò chơi hai người phổ quát, lấp đầy khoảng trống trong lý thuyết lặp lại song song lượng tử. Trong lĩnh vực mật mã lưới, nó đã hoàn thành chứng minh độ khó xấp xỉ đa thức CVP, mà tính bảo mật của mật mã hậu lượng tử, ở một mức độ nào đó, được xây dựng dựa trên các vấn đề này.
Astra còn giải quyết ba vấn đề mở kinh điển của Erdos cùng một lúc:
Đối với số Ramsey đa sắc 183, mô hình đã suy ra một giới hạn dưới siêu cấp số mũ, thông qua cơ chế bảng màu để ghép các khối đệ quy, kết hợp với các quy tắc tô màu cạnh ràng buộc ma trận bão hòa, từ đó loại bỏ sự hình thành các tam giác đơn sắc từ cấp độ cấu trúc.
Đối mặt với các phỏng đoán đồ thị cực trị compact và suy biến 146, 180, nó đã sử dụng lập luận phân lớp hai mẫu, lần lượt kiểm soát phân bố tập mở rộng, chuyển đổi các đỉnh bất thường, dựa vào cửa sổ entropy hình học Hamming để loại bỏ tất cả các mảng con không hợp lệ có entropy thấp.
Quá trình giải quyết vấn đề của Astra có thể được chia thành bốn giai đoạn chính. Đầu tiên, Astra tự chủ suy luận xung quanh một vấn đề mở, tạo ra các lập luận toán học và ý tưởng chứng minh cốt lõi hoàn chỉnh. Thứ hai, các nhà nghiên cứu sử dụng một mô hình Astra tương tự để hỗ trợ sắp xếp văn bản, điều chỉnh cho phù hợp với các tiêu chuẩn chung về đọc, đánh giá và trích dẫn trong giới toán học. Thứ ba, mô hình tiếp tục hình thức hóa các chứng minh này, chuyển đổi chúng thành chứng minh Lean. Lean có thể biến mỗi bước toán học thành một biểu thức logic mà máy tính có thể xác minh, chỉ cần có bất kỳ lỗ hổng nào trong suy luận, nó sẽ không thể vượt qua xác minh. Điều này tương đương với việc có thêm một lớp cơ chế kiểm duyệt. Cuối cùng, OpenAI đồng bộ công khai toàn bộ văn bản tường thuật suy luận của AI cho mỗi bài toán, lưu giữ đầy đủ quá trình thử và sai, thay đổi công cụ toán học, tự bác bỏ ý tưởng của mô hình, tạo điều kiện cho các nhà toán học toàn cầu xem xét lại nguồn gốc.
Cách đây không lâu, Geoffrey Hinton, người được mệnh danh là "cha đẻ của AI", đã dự đoán rằng trong vòng 10 đến 20 năm tới, AI có thể tạo ra những khái niệm toán học mới mà con người không thể hiểu được. Với những gì Astra đã thể hiện hôm nay, có vẻ như tương lai đó không còn xa nữa.
