Mô hình tiếp theo của OpenAI, Astra, vừa giải mười bài toán mở hàng thập kỷ

Ngày 1 tháng 8, OpenAI công bố một báo cáo cho biết mô hình tiếp theo của hãng, tên nội bộ là Astra, đã đưa ra các kết quả mới cho mười bài toán mở khác nhau trong toán học. (Không, đó không phải là các bài toán Giải thưởng Thiên niên kỷ, nhưng vẫn hết sức đáng kể.)

Điểm đáng chú ý: Những lời giải này không chỉ là bước tiến nhỏ lẻ đối với các bài toán; chúng là các nghiệm giải quyết trọn vẹn, đã được kiểm chứng bằng Lean. (Lean là một ngôn ngữ lập trình kiêm trợ lý chứng minh, buộc mọi bước của lập luận toán học phải được diễn đạt chi tiết theo cách máy có thể đọc.) 

Có rất nhiều điều phải tiếp nhận cùng lúc. Trong bài viết này, tôi sắp xếp các bài toán theo lĩnh vực và mô tả ở mức khái quát chuyện gì đã xảy ra, điều này có thể ngụ ý gì cho ngành toán, và những gì ta có thể suy ra thêm về Astra.

Mười bài toán đó là gì?

Dưới đây là từng kết quả, bằng ngôn ngữ giản dị, kèm theo lĩnh vực toán học hoặc khoa học máy tính tương ứng.

Nhóm không sofic

Lĩnh vực: Lý thuyết nhóm

Astra đã đưa ra một xây dựng tường minh của một nhóm không thể được xấp xỉ, dù gần đến đâu, bằng các cấu trúc hữu hạn lớn — khép lại một câu hỏi mở kể từ khi khái niệm nhóm “sofic” được giới thiệu năm 1999. Bản xây dựng đi kèm chứng minh rằng không có dãy xấp xỉ hữu hạn nào có thể hiệu quả, được hình thức hóa trong Lean để logic có thể được kiểm tra một cách cơ học.

Wikipedia đã được cập nhật:

Xếp khối cầu

Lĩnh vực: Hình học nhiều chiều

Câu hỏi đặt ra là có thể xếp các khối cầu đồng nhất, không chồng lấn dày đặc đến mức nào khi số chiều tăng. Astra đã chứng minh một trần trên chặt chẽ hơn cho mật độ đó ở không gian có số chiều lớn, là cải thiện đầu tiên cho cận này kể từ năm 1978. Nó không đưa ra một phương pháp xếp tốt hơn — mà thu hẹp phạm vi mức tốt nhất mà mọi phương pháp tương lai có thể đạt tới.

Mã nhị phân và mã cầu

Lĩnh vực: Lý thuyết mã hóa

Mã sửa sai hoạt động bằng cách giữ các thông điệp hợp lệ cách nhau đủ xa để lỗi nhỏ không thể biến thông điệp này thành thông điệp khác. Astra đã chứng minh các giới hạn chặt chẽ hơn rất nhiều (cải thiện theo hàm mũ) về số lượng thông điệp như vậy có thể tồn tại với một khoảng cách tối thiểu cho trước, cùng một kết quả tương ứng cho các điểm phân bố trên một khối cầu nhiều chiều.

Giả thuyết độ cứng của Connes

Lĩnh vực: Đại số toán tử

Alain Connes cho rằng một số nhóm nhất định luôn có thể được tái dựng duy nhất từ một cấu trúc đại số gọi là đại số von Neumann được xây dựng từ chúng. Astra đã phản chứng điều này bằng cách đưa ra hai nhóm thực sự khác nhau nhưng sinh ra cùng một đại số, cho thấy việc tái dựng không phải lúc nào cũng một-một.

Độ phức tạp mạch số học

Lĩnh vực: Lý thuyết độ phức tạp tính toán

“Permanent”, một con số duy nhất được tính từ một lưới số, rất tốn kém để tính toán, và các nhà lý thuyết độ phức tạp muốn biết số bước số học tối thiểu mà bất kỳ phương pháp nào có thể cần. Astra đã chứng minh một cận dưới mới, mạnh hơn cho mức tối thiểu đó — kiểu kết quả vốn nổi tiếng là cực khó cải thiện dù chỉ một chút.

Lặp lại song song lượng tử

Lĩnh vực: Lý thuyết độ phức tạp lượng tử

Lý thuyết cổ điển nói rằng buộc hai người chơi không giao tiếp lặp lại một trò chơi khó nhiều lần theo kiểu song song sẽ khiến gian lận có khả năng thành công giảm theo hàm mũ. Astra đã chứng minh đảm bảo tương tự vẫn giữ khi người chơi chia sẻ vướng víu lượng tử, mở rộng một nguyên lý nền tảng của cổ điển sang bối cảnh lượng tử.

Bài toán vectơ gần nhất

Lĩnh vực: Mật mã dựa trên mạng (lattice)

Cho một lưới các điểm lặp lại (một lattice) và một vị trí mục tiêu, bài toán yêu cầu điểm lưới gần nhất — một bài toán được tin là rất khó ở số chiều lớn, vì vậy nó là nền tảng của một số mã hóa kháng lượng tử. Astra đã chứng minh rằng ngay cả việc xấp xỉ lời giải, trong một hệ số đa thức cụ thể, vẫn chứng minh được là khó, củng cố các hệ mật mã xây dựng dựa trên đó.

Giả thuyết thể tích của Ehrhart

Lĩnh vực: Hình học rời rạc và lồi

Với một hình lồi mà điểm lưới duy nhất bên trong nằm chính xác tại trọng tâm của nó, các nhà toán học muốn biết thể tích lớn nhất có thể của một hình như vậy trong mọi số chiều cho trước. Astra đã tìm ra thể tích cực đại đó cho mọi số chiều, giải quyết trọn vẹn giả thuyết này ở mức tổng quát.

Số Ramsey đa màu

Lĩnh vực: Lý thuyết Ramsey / tổ hợp

Với đủ nhiều người và đủ nhiều loại quan hệ giữa họ, sớm muộn bạn cũng sẽ tìm thấy ba người đều được nối kết bởi cùng một loại quan hệ. Astra đã chứng minh rằng kích thước nhóm tối thiểu cần thiết tăng nhanh hơn bất kỳ tốc độ hàm mũ cố định nào khi số loại tăng, giải quyết bài toán Erdős số 183.

Các giả thuyết về số cực trị

Lĩnh vực: Lý thuyết đồ thị cực trị

Nhánh toán này hỏi một mạng có thể có bao nhiêu kết nối trong khi vẫn tránh được một số mẫu nhỏ bị cấm nhất định. Astra đã giải quyết hai giả thuyết liên quan tại đây, tương ứng với các bài toán Erdős số 146 và 180, xác định mật độ mà các mạng như vậy có thể đạt tới trước khi những mẫu đó trở nên không thể tránh khỏi.

Mỗi bài trong số này đã mở ít nhất một thập kỷ; một số đã tồn tại suốt hơn ba mươi năm, bao gồm cả những bài toán có các chủ nhân Giải Turing làm việc ở phía khoa học máy tính lý thuyết.

Khoan, phản ví dụ có phải là kiểu chứng minh “dễ”?

Tôi nào dám nói điều gì tiêu cực ở đây, nhưng tôi biết đây là thắc mắc hay phản ứng thường gặp, đặc biệt từ những người có đôi chút hiểu biết về toán.

Nhận xét phổ biến nhất theo hướng phê bình: Một số kết quả này là các phản ví dụ hơn là lý thuyết tổng quát mới. Ý này quan trọng vì một phản ví dụ trả lời câu hỏi có/không nhưng tự nó không cho bạn biết vì sao khuôn mẫu bị phá vỡ hay trao cho bạn một họ đối tượng tương tự để nghiên cứu tiếp, trong khi thứ khác, như một định lý phân loại hay một kỹ thuật mới, lại mở ra nhiều cánh cửa.

Tôi cho rằng phê bình này đúng nói chung, nhưng không thể dùng để gạt bỏ cả loạt vấn đề này. Thứ nhất, kết quả về nhóm không sofic không phải là một tinh chỉnh nhỏ của một trường hợp suýt đúng đã có — đó là bản xây dựng đầu tiên thuộc loại này sau 27 năm không ai có, và kỹ thuật phía sau được kỳ vọng sẽ khái quát để tìm ra các ví dụ khác.

Thứ hai, vài trong chín kết quả còn lại, bao gồm cận xếp khối cầu và độ khó CVP, không phải phản ví dụ; chúng là cải tiến trực tiếp đối với các cận hiện hành. 

Những gì vẫn chưa ngã ngũ

Một vài điều đáng để theo dõi khi cộng đồng mổ xẻ chuyện này trong những ngày, tuần và tháng tới:

\n
• Chưa có bình duyệt. Các chứng minh đã được Lean kiểm chứng và được các nhà toán học xem trước bản thảo đánh giá không chính thức, nhưng chưa có bản nào qua quy trình tạp chí phản biện. 
\n
• Tác quyền vẫn đang được thương lượng. OpenAI cho biết họ chịu trách nhiệm đối với bản thảo và các hình thức hóa trong Lean, đồng thời quy các lập luận toán học tự thân cho mô hình. Việc tái lập độc lập quy trình (khác với việc kiểm chứng các chứng minh) hiện khó thực hiện.
\n

Điều này có ý nghĩa gì với Toán học

Sự chuyển dịch tức thời nhất là ở chỗ các nhà toán học có thể sẽ dành thời gian cho việc gì. Nếu một bài toán mở được đặt bài bản có thể giao cho mô hình và kiểm bằng Lean, nút thắt sẽ chuyển từ “có ai giải được không” sang “chúng ta đã hỏi đúng câu hỏi và hình thức hóa đúng chưa”. Kỹ năng đặt bài toán hay và biết bài nào đáng công kích là một kỹ năng thực sự mà các nhà toán học tích lũy qua trải nghiệm. 

Cũng có một câu hỏi âm ỉ về tài trợ và uy tín. Các khoản tài trợ nghiên cứu, hồ sơ tenure và giải thưởng lịch sử dựa vào sự khan hiếm: các bài toán này đủ khó để việc giải một bài nói lên điều gì đó về người giải. Nếu kết quả có hỗ trợ AI trở nên thường lệ, lĩnh vực này sẽ cần những cách mới để biểu đạt cái gì thực sự khó so với cái gì giờ đã nằm trong tầm với của vài nghìn đô chi phí suy luận. Tất nhiên, người thường không hiểu đầy đủ các bài toán này. Những người được đào tạo bài bản thì hiểu, và điều đó không đổi. Vì vậy, tri thức toán học còn giá trị hơn bao giờ hết. 

Mọi người phản ứng ra sao

Phản ứng trên mạng xã hội ít chia rẽ về việc các chứng minh có kiểm tra được hay không, mà nhiều hơn về việc chúng là bằng chứng cho điều gì.

Một số người coi chính nhịp độ là câu chuyện lớn: mười bài toán hàng thập kỷ rơi xuống cùng lúc, trải rộng nhiều lĩnh vực không liên quan, nhanh hơn tốc độ chuyên gia có thể thẩm tra. Câu hỏi cho tương lai: “Liệu chúng ta có theo kịp việc kiểm tra tất cả không?”

Những người khác phản biện rằng điều này nói về AI nói chung ít hơn vẻ bề ngoài. Toán học là miền hiếm hoi nơi công việc của mô hình có thể được kiểm tra tự động và đầy đủ. Hầu hết các vấn đề đời thực không có sẵn loại đáp án tự động tích hợp như vậy. Theo góc nhìn đó, thành tựu là thật, nhưng có thể nói nhiều hơn về việc toán học đặc biệt phù hợp với AI.

Một luồng bình luận thứ ba: Một chứng minh đúng nhưng chưa được kiểm tra và thấu hiểu trọn vẹn thì chưa thực sự được hiểu, chỉ mới được xác nhận. Khám phá một định lý và hiểu nó có ý nghĩa gì, theo góc nhìn này, là hai công việc khác nhau.

Lời kết

Các nhà toán học cho rằng kết quả về nhóm không sofic có vẻ là “hàng thật”: một câu hỏi mở thực sự qua nhiều thập kỷ trong lý thuyết nhóm, được khép lại bằng một xây dựng tường minh mà các nhà toán học trong ngành coi là nghiêm túc. Chín kết quả còn lại, xét chung, đại diện cho một loạt tiến bộ rộng và có hàm lượng kỹ thuật đáng kể trong toán thuần túy.

Điều chưa xảy ra là phần chậm hơn: bình duyệt, tái lập quy trình tìm kiếm, và cộng đồng thực sự xây dựng tiếp trên các kết quả này. Phần đó mất nhiều thời gian hơn một bài blog, và chính nó sẽ cho ta biết quy mô thực sự của sự kiện này. Chúng tôi sẽ tiếp tục cập nhật.