Từ hàng trăm bản thảo đến áp lực xác minh
AI giải toán là việc mô hình trí tuệ nhân tạo tạo ra lập luận hoặc lời giải cho các bài toán, nhưng kết quả chỉ trở thành tri thức đáng tin cậy sau khi được kiểm tra nghiêm ngặt. Ngày 6/10, OpenAI công bố trên GitHub 722 bản thảo do một mô hình nội bộ chưa thương mại hóa tạo ra; tài liệu được chia thành 372 nhóm kết quả, bàn về nhiều bài toán mở. Theo thông tin được nêu sau đó, mô hình này được cho là đã xử lý 372 danh mục bài toán phức tạp và tìm ra ba phát hiện toán học mới. Quy mô ấy đáng chú ý, nhưng không nên đánh đồng số lượng bản thảo với số định lý đã được xác nhận. Tốc độ tạo kết quả đang thay đổi nhịp độ nghiên cứu toán học; nếu khâu thẩm định không theo kịp, công bố nhanh có thể khiến sai sót lan rộng thay vì thúc đẩy tri thức.
Khoảng cách giữa bản thảo và kết quả được công nhận không phải giả định. OpenAI đã rút lại ba bản thảo sau khi phát hiện lỗi; một sai sót về dấu làm hỏng chứng minh chính và ảnh hưởng đến hai công trình phụ thuộc. Đây là lời nhắc quan trọng: một kết luận mới lạ chưa đủ, và văn phong toán học trông có vẻ chặt chẽ cũng không bảo đảm từng bước lập luận đều hợp lệ. Câu hỏi cấp bách không còn là liệu AI có thể viết lời giải hay không, mà là ai có thời gian đọc, kiểm tra và chịu trách nhiệm xác nhận chúng.
Tốc độ máy móc đang thử giới hạn của học thuật
Terence Tao cảnh báo về tình trạng ông gọi là “khai thác mỏ lộ thiên” trong toán học: AI có thể rà soát hàng trăm bài toán mở cùng lúc và tạo ra lượng lớn lời giải, trong khi quy trình bình duyệt vốn được xây dựng quanh nhịp làm việc của con người. Cùng Khâu Thành Đồng, ông cảnh báo giới học thuật có nguy cơ không theo kịp tốc độ tạo kết quả. Lo ngại này có cơ sở: những bản thảo dài, khó đọc và chưa được kiểm chứng đồng đều khiến nhà nghiên cứu phải tiêu tốn thời gian để phân loại điều đúng, điều sai và điều đáng theo đuổi. Nút thắt vì thế không nằm ở năng lực sinh văn bản, mà ở năng lực thẩm định. Nếu số lượng kết quả tăng nhanh hơn khả năng kiểm tra, hệ thống công bố có thể bị quá tải và những phát hiện có giá trị cũng khó được nhận diện.
Sức ép ấy còn có thể làm tổn hại văn hóa chia sẻ vốn nuôi dưỡng nghiên cứu toán học. Hugo Duminil-Copin cho biết 16 bài toán trong các tài liệu thuộc hướng nghiên cứu của ông; ông kể mình bật khóc khi đối diện quy mô và tốc độ tạo kết quả, đồng thời dự định cùng đồng nghiệp xem xét hơn 3.500 trang tài liệu liên quan. Nỗi lo không chỉ là cạnh tranh giữa người và máy. Nếu ý tưởng chưa hoàn thiện hay giả thuyết đang thảo luận lập tức trở thành đầu vào cho hệ thống tạo lời giải hàng loạt, nhà nghiên cứu có thể dè dặt hơn khi chia sẻ. Các nhà nghiên cứu trẻ, vốn cần thời gian định hình hướng đi và khẳng định vị trí, đặc biệt dễ chịu sức ép này.
Kiểm chứng hình thức phải thành một phần của quy trình
Một bản thảo do AI tạo ra không tự động trở thành định lý đã được giới toán học xác nhận; các tài liệu công bố chưa trải qua cùng một mức độ kiểm tra, và không phải chứng minh nào cũng được hình thức hóa bằng Lean. Đây là lý do kiểm chứng lời giải cần được xem như một công đoạn bắt buộc, không phải thủ tục đến sau khi kết quả đã gây tiếng vang. Lean cho phép biểu diễn lập luận theo dạng mà máy tính có thể kiểm tra từng bước, giúp phát hiện lỗ hổng logic mà người đọc có thể bỏ sót. Tao cùng 25 nhà toán học từng đoạt Huy chương Fields đã kêu gọi sử dụng phần mềm kiểm chứng hình thức trước khi công nhận định lý mới. Công cụ này không thay thế việc đánh giá ý nghĩa của kết quả, nhưng có thể tạo một lớp bảo đảm về tính hợp lệ của chứng minh.
Không nên kỳ vọng phần mềm tự giải quyết mọi vấn đề. Một chứng minh được kiểm tra hình thức vẫn cần người hiểu nó đang đóng góp điều gì, liên hệ ra sao với tri thức hiện có và có đáng để phát triển tiếp hay không. Duminil-Copin và các đồng nghiệp dự định xem xét, hệ thống hóa và truyền đạt kiến thức hữu ích từ khối tài liệu lớn, một công việc vượt xa việc dò lỗi từng dòng. Khâu Thành Đồng đã ra mắt một tạp chí chuyên ngành về toán học có AI hỗ trợ, cho thấy cộng đồng đang thử xây dựng khuôn khổ công bố mới. Hướng đi hợp lý là kết hợp kiểm chứng hình thức, bình duyệt minh bạch và ghi nhận rõ phần đóng góp của con người lẫn thuật toán.
AI có thể tăng tốc khám phá, nhưng không thể tự trao uy tín
AI chứng minh định lý có thể mở ra những hướng tìm kiếm mà một cá nhân khó theo đuổi với tốc độ tương tự. Nhưng năng lực tạo ra kết quả và thẩm quyền xác nhận kết quả là hai chuyện khác nhau. Ba bản thảo bị rút lại cho thấy sai sót có thể nằm trong chi tiết nhỏ mà kéo theo hệ quả lớn; hàng trăm tài liệu chưa đồng đều về mức độ kiểm chứng cho thấy bình duyệt thông thường khó hấp thụ làn sóng này. Vì vậy, phản ứng đúng không phải chạy đua công bố nhanh hơn AI, cũng không phải gạt bỏ mọi kết quả do máy tạo. Giới nghiên cứu cần quy trình phân loại, ưu tiên kiểm tra và xác nhận hình thức trước khi một khẳng định được lưu hành như định lý.
Cuối cùng, AI nên được xem là tác nhân tăng năng suất khám phá, không phải người phán quyết cuối cùng. Nhà toán học vẫn cần đặt câu hỏi, nhận ra ý nghĩa, kiểm tra lập luận và biến những kết quả rời rạc thành hiểu biết có thể truyền đạt. Nếu thiếu những bước đó, tốc độ chỉ tạo thêm một núi bản thảo; nếu có quy trình phù hợp, máy móc có thể giúp mở rộng phạm vi nghiên cứu mà không làm suy yếu chuẩn mực chứng minh. Bài toán lớn nhất của kỷ nguyên AI vì thế không chỉ là tạo ra lời giải, mà là bảo đảm mỗi lời giải đáng tin trước khi cộng đồng chấp nhận nó.
