Bảy nhà nghiên cứu của Google Research đã nộp một bài báo lên arXiv vào ngày 30 tháng 9, giới thiệu hệ thống đa tác tử (multi-agent) có tên Cogentic, chuyên dùng để tìm các chứng minh toán học ở cấp độ nghiên cứu. Theo bài báo, hệ thống lấy Gemini làm mô hình nền, đã giải quyết được 5 bài toán mở trong ba lĩnh vực học trực tuyến, lý thuyết đấu giá và thiết kế cơ chế; toàn bộ các chứng minh sau đó đều được chuyên gia trong lĩnh vực kiểm chứng độc lập, và đã được mở rộng thành các bài báo hoàn chỉnh có đồng tác giả là chuyên gia.
Trong danh sách tác giả có Yang Cai, đồng thời công tác tại Đại học Yale, và Vineet Gupta, đồng thời thuộc Google DeepMind, cùng một số người khác như Aranyak Mehta, Christopher Liaw, Di Wang. Bài báo được xếp vào hai danh mục cs.AI và cs.GT (lý thuyết trò chơi).
Một lần sinh không đủ, phải chia thành một quy trình
Xuất phát điểm của bài báo khá đơn giản: các mô hình ngôn ngữ đã có thể đưa ra những ý tưởng toán học khá tốt, nhưng khi gặp bài toán khó cần thử nhiều hướng giả thuyết cùng lúc và triển khai liên tục trong nhiều ngày, việc sinh một lần là không đủ.
Cách làm của Cogentic là chia việc tìm chứng minh cho các vai trò khác nhau:
- Bộ điều phối (orchestrator) nắm trạng thái tổng thể, quyết định cử bao nhiêu "người chứng minh" đến hướng nào;
- Người chứng minh (prover) viết song song các chứng minh ứng viên;
- Người kiểm chứng (verifier) tìm lỗi từ các góc độ bổ sung cho nhau, mang tính đối kháng;
- Người tra cứu tài liệu bổ sung thông tin nền;
- Sổ cái (ledger) chỉ lưu các kết luận trung gian đã qua kiểm chứng, được giữ lại qua các vòng, để các chứng minh sau có thể trích dẫn trực tiếp;
- Ngoài ra còn có vai trò "cố vấn" theo dõi mô hình chung của toàn bộ quá trình, liên tục điều chỉnh tham số.
Chứng minh, kiểm chứng, rồi lại chứng minh, cứ thế lặp lại. Thiết kế sổ cái giải quyết một vấn đề cố hữu của các tác vụ dài hạn: bổ đề mà mô hình đưa ra ở vòng trước thường bị quên hoặc bị diễn đạt khác đi ở vòng sau, còn giờ đây chỉ cần qua kiểm chứng là được ghi cố định.
Năm bài toán được giải quyết đến đâu
Theo kết quả bài báo đưa ra:
- Tối ưu hóa tuyến tính nghịch trực tuyến (online inverse linear optimization): lần đầu đạt được cận hối tiếc (regret bound) O(d) hiệu quả, không phụ thuộc vào khoảng thời gian T, với chi phí tính toán mỗi vòng là O(d²);
- Độ phức tạp cạnh tranh của thị trường hai phía: chứng minh rằng chỉ cần thêm đúng 2 người bán ở phía nhỏ hơn, doanh thu giao dịch có thể đuổi kịp mức phân bổ tối ưu;
- Hối tiếc tức thời (anytime regret) với n chuyên gia: đưa ra một thuật toán anytime có hằng số tương đương với phiên bản thời lượng cố định;
- Cơ chế đơn giản và doanh thu tối ưu: tỷ lệ xấp xỉ doanh thu của một người mua duy nhất có thể cộng dồn được cải thiện từ 5,2 lên 3,52;
- Cái giá của vô chính phủ (price of anarchy) trong đấu giá tự động: với 2 người đấu giá đạt mức tối ưu 1,5, với n người đấu giá là 2−1/(4n+1).
Về chi phí, bài báo cho biết phần lớn các bài toán gọi Gemini ở mức hàng trăm lần, bài khó nhất ở mức hàng nghìn lần, nhưng không nêu rõ dùng phiên bản Gemini nào.
Đặt cạnh các nhóm chứng minh của OpenAI
Nửa cuối năm nay, tin tức về AI làm toán xuất hiện dồn dập, đặt cạnh nhau thì khác biệt nằm ở hướng kiểm chứng.
Tháng 8, OpenAI dùng Astra đưa ra 10 kết quả về toán học và khoa học máy tính lý thuyết, kèm bài báo dài 249 trang và chứng chỉ hình thức hóa bằng Lean; chứng minh giả thuyết Navier–Stokes công bố tháng 9 huy động khoảng mười nghìn tác tử chạy trong 88 giờ, cũng kèm theo tệp Lean. Chứng chỉ hình thức hóa mà máy có thể kiểm tra được là điểm bán hàng mà hướng đi của OpenAI liên tục nhấn mạnh.
Bài báo của Cogentic đặt trọng tâm ở phía khác: bên trong hệ thống dựa vào người kiểm chứng mang tính đối kháng để sàng lọc một lượt, sau khi ra khỏi hệ thống thì người am hiểu đọc từng chứng minh, rồi cùng chuyên gia viết thành bài báo chính thức. Quy mô bài toán cũng được thu hẹp hơn: cả 5 bài đều thuộc lĩnh vực nghiên cứu của chính các tác giả, là loại bài toán trong ngành có người theo dõi và có thể được đồng nghiệp đánh giá khi làm ra.
Cách chọn này giúp kết quả dễ được công nhận hơn, cái giá phải trả là khả năng ngoại suy. Bài báo tự thừa nhận các bài toán được "chọn từ lĩnh vực mà tác giả quen thuộc", còn chuyển sang hướng tác giả không quen thì hiệu quả ra sao, bài báo không trả lời.
Người đọc theo không kịp tốc độ viết
Trong bài báo có một câu gần như trùng với điều mà bài giảng của Đào Triết Hiên (Terence Tao) hồi tháng 8 đã lo ngại:
"A system like this can produce candidate results faster than they can be read."
"Một hệ thống như thế này có thể tạo ra kết quả ứng viên nhanh hơn tốc độ người ta đọc hết chúng."
Cả 5 bài toán của Cogentic đều có chuyên gia kiểm soát, nên mới có thể gọi là "đã kiểm chứng". Một khi cách vận hành này được mở rộng cho nhiều người hơn, bài toán trải rộng hơn, nút thắt cổ chai sẽ rơi vào người thẩm định. Bài báo không nêu rõ chuyên gia mất bao lâu để kiểm chứng mỗi chứng minh, mà đây chính là con số quyết định hệ thống có thể mở rộng đến quy mô nào.
Nguồn tham khảo: bài báo arXiv 2609.40324, CocoLoop, Google Research; các cận và tỷ lệ xấp xỉ, số lượng lệnh gọi của 5 kết quả đều theo nội dung chính của bài báo.