AI của Google giải các bài toán bỏ ngỏ suốt 56 năm với chỉ vài trăm đô la

Một hệ thống nghiên cứu của Google DeepMind đã tạo ra những chứng minh đầy đủ, được máy kiểm chứng cho chín bài toán mở do nhà toán học Paul Erdős đặt ra, hai trong số đó chưa có lời giải suốt 56 năm. Cùng hệ thống ấy đã khép lại 44 phỏng đoán lấy từ Bách khoa toàn thư trực tuyến về các dãy số nguyên, giải một câu hỏi hình học đại số mở suốt 15 năm và siết chặt một cận đã biết trong tối ưu lồi. Con số gây chú ý ít quan trọng hơn phương pháp. Mỗi chứng minh trong số này được một cỗ máy kiểm chứng, chứ không chỉ được nó khẳng định.

Erdős, qua đời năm 1996, để lại hàng trăm câu hỏi chính xác và cứng đầu, nhiều câu dễ phát biểu nhưng cực kỳ khó khép lại. Qua nhiều thập kỷ, chúng trở thành một kiểu kỳ thi thường trực của ngành. Các phỏng đoán về dãy số đến từ một cơ sở dữ liệu công khai mà các nhà toán học đào bới để tìm quy luật, nơi một công thức đoán ra có thể nằm chưa được chứng minh trong nhiều năm. Đây không phải bài kiểm tra dựng lên để tâng bốc một mô hình. Đó là phần tồn đọng thật sự của toán học mở.

Chính sự phân biệt ấy là toàn bộ câu chuyện. Hệ thống mang tên AlphaProof Nexus viết lập luận của mình bằng Lean, một ngôn ngữ hình thức có trình biên dịch bác bỏ mọi bước nó không thể xác nhận. Một chứng minh hoặc qua hoặc không, không có chỗ cho một đoạn văn tự tin mà về sau hóa ra sai. Với ai muốn phán xét một ‘khám phá’ của AI có thật hay không, đây chính là lằn ranh giữa một thông cáo báo chí và một kết quả.

Bên dưới, bộ chứng minh chạy trên Gemini 3.1 Pro, còn một mô hình nhẹ hơn lo việc xếp hạng. Vòng lặp gần như tẻ nhạt. Mô hình phác một chứng minh bằng Lean, trình biên dịch trả về các lỗi, và những lỗi đó nuôi lần thử kế tiếp. Thứ giữ cho nó trung thực là phản hồi ký hiệu, chứ không phải lối hành văn trôi chảy. Nhóm đã dựng bốn phiên bản với độ phức tạp tăng dần, một trong số đó có thể sinh ra và xếp hạng các bản nháp chứng minh cạnh tranh. Vậy mà phiên bản đơn giản nhất, chỉ là một vòng lặp gồm mô hình và trình biên dịch, đã tự mình giải cả chín bài toán của Erdős.

Phần lặng lẽ gây kinh ngạc là chi phí. Mỗi bài toán được giải tốn vài trăm đô la thời gian tính toán. Những câu hỏi từng ngốn cả sự nghiệp được khép lại với cái giá xấp xỉ một chuyến đi cuối tuần. Điều này không cho nhà toán học về hưu. Vẫn cần có người chọn bài toán nào đáng công phá, diễn đạt chúng theo dạng mà hệ thống đọc được và quyết định một lời giải có nghĩa gì. Cái thay đổi là phép tính về việc rốt cuộc điều gì đáng để thử.

Những dè dặt nặng hơn cái tựa. Giải được chín trong 353 bài toán Erdős đã thử là tỷ lệ trúng khoảng 2,5 phần trăm. Con số ở mảng dãy số, 44 trên 492, dưới chín phần trăm. Các tác giả thẳng thắn rằng phần lớn những bài toán này vẫn ngoài tầm với, càng đúng với những bài đòi hỏi lý thuyết mới và đồ sộ, và rằng thành công dồn vào những lĩnh vực mà thư viện toán học của Lean vốn đã dày. Bỏ đi giàn giáo do con người dựng và danh sách mục tiêu được tuyển chọn, hệ thống chẳng còn mấy chỗ đứng.

Sự thận trọng là xứng đáng. Trong một vụ bị chế giễu rộng rãi, một phòng thí nghiệm đối thủ tuyên bố mô hình của họ đã giải mười bài toán Erdős, cho đến khi các nhà toán học chỉ ra rằng lời giải đã có sẵn trong tài liệu đã công bố. Mô hình đã tìm thấy chúng, chứ không chứng minh chúng. AlphaProof Nexus được xây để miễn nhiễm với sai lầm đó. Một chứng minh bằng Lean cho một kết quả đã biết vẫn là một chứng minh hợp lệ, và một chứng minh bằng Lean cho điều thực sự mới thì không thể bịa. Demis Hassabis, người điều hành DeepMind, cố ý nói rằng công trình này không phải trí tuệ nhân tạo tổng quát, một ghi chú thận trọng hiếm thấy ở một công ty hiếm khi rụt rè với các mô hình của mình.

Còn một phần thưởng tinh tế hơn mà các nhà nghiên cứu nhấn mạnh. Ngay cả những lần thất bại cũng hữu ích. Vì mỗi chứng minh từng phần đều được kiểm chứng hình thức, các nhà toán học có thể thấy chính xác hệ thống khép được những mục tiêu con nào và không khép được những cái nào, mà không phải kiểm lại toàn bộ lập luận bằng tay. Cỗ máy thôi làm một lời sấm và trở thành một cộng sự không biết mệt, phơi bày công việc của mình và chỉ ra phần khó vẫn còn ẩn ở đâu.

Kết quả không đứng một mình. Nó rơi vào cùng quãng thời gian với một tuyên bố riêng từ một mô hình suy luận đối thủ, được cho là đã bác bỏ một phỏng đoán Erdős chừng 80 năm tuổi trong hình học rời rạc, một phát hiện mà các nhà toán học đang hành nghề đã tinh chỉnh và xác nhận. Hai phòng thí nghiệm, hai phương pháp, một bên dựa vào kiểm chứng hình thức và bên kia dựa vào chuỗi suy luận thô, cùng chạm tới một biên giới chỉ cách nhau vài tuần. Cuộc đua không còn là về những chatbot nghe có vẻ thông minh.

Công trình được trình bày trong một bài báo công bố trong tháng này, và phương pháp dựa vào các công cụ mở, cụ thể là Lean và thư viện do cộng đồng dựng nên, nhờ vậy các nhóm bên ngoài có thể kiểm tra và chạy lại các chứng minh thay vì tin một blog của công ty. DeepMind chưa nói liệu hệ thống có đến tay các nhà nghiên cứu ngoài công ty hay không. Con số đáng theo dõi không phải là chín. Mà là liệu 2,5 phần trăm ấy có thành mười, rồi hai mươi hay không, bởi vào ngày đó, cuộc tranh luận về việc những cỗ máy này dùng để làm gì sẽ phải bắt đầu lại từ đầu.