Tốc độ tạo lời giải không đồng nghĩa với tri thức đáng tin
AI giải toán là việc các hệ thống trí tuệ nhân tạo tạo ra hoặc hỗ trợ xây dựng lời giải và chứng minh toán học, nhưng kết quả chỉ đáng tin khi lập luận được kiểm tra độc lập và có thể đối chiếu với điều cần chứng minh. AI đang xử lý những bài toán phức tạp với tốc độ vượt xa con người. Tháng trước, Claude của Anthropic mất 11 ngày để tự động hình thức hóa 13 triệu dòng mã từ chứng minh Định lý cuối cùng của Fermat, hoàn thành năm 1995. Đầu tháng 10, OpenAI công bố 700 bản thảo toán học do AI tạo ra; chỉ một ngày sau, công ty rút lại ba bản vì phát hiện sai sót. Những con số ấy cho thấy năng suất đã đổi khác, nhưng không chứng minh rằng mọi kết luận đều đúng. Trong toán học, tốc độ sản xuất lời giải không thể thay thế trách nhiệm giải thích và thẩm định.
Lean kiểm tra hình thức, không đảm bảo bản gốc được diễn giải đúng
Phần mềm Lean, trợ lý chứng minh ra mắt năm 2013, được nhiều nhà toán học dùng để kiểm tra các mệnh đề đã chuyển sang ngôn ngữ máy tính. Nhưng đây không phải con dấu bảo đảm rằng một chứng minh viết bằng ngôn ngữ tự nhiên đã được chuyển đổi chính xác. Nếu AI vô tình thay mệnh đề cần chứng minh bằng một kết luận yếu hơn, Lean vẫn có thể xác nhận phần hình thức hóa ấy mà không phát hiện độ lệch so với bản gốc. Lean 4 cũng có thể mắc lỗi tính hợp lệ, khiến chứng minh sai lọt qua; ngay cả người tạo ra phần mềm, Leonardo de Moura, cũng không cho rằng hệ thống đã sạch lỗi. Vì vậy, lời giải được máy xác nhận vẫn cần con người đối chiếu từ đầu đến cuối. Kiểm chứng chứng minh không thể chỉ là kiểm tra xem phần mềm có báo đạt hay không.
Lời giải dài và khó hiểu làm tăng gánh nặng thẩm định
Ngay cả khi hình thức hóa hợp lệ, một chứng minh dài hàng trăm trang hoặc hàng trăm nghìn dòng mã vẫn có thể nằm ngoài khả năng đọc hiểu thực tế của nhiều nhà toán học. Các định nghĩa có thể xuất hiện mà không làm rõ chúng đóng vai trò gì, còn bước đột phá và ý tưởng mới thì khó nhận diện. Trong một cuộc rà soát kéo dài ba tuần, một nhóm xem xét 180 trang chứng minh bằng Lean và dùng ChatGPT tìm khác biệt giữa bản thông thường với bản hình thức hóa. Chỉ kiểm tra kỹ hai trang, họ đã phát hiện hai trường hợp Lean xác nhận kết luận hẹp hơn điều bản gốc tuyên bố. Rủi ro này không bó hẹp trong học thuật: Lean còn được dùng cho chứng minh hình thức liên quan đến an ninh mạng và môi trường sandbox, trong khi mô hình AI đã góp mặt trong đánh giá hồ sơ vay và rủi ro tài chính. Sai sót khó phát hiện có thể ảnh hưởng đến công chúng.
Kiểm chứng độc lập phải đi cùng quản trị cộng đồng
Toán học và AI có thể bổ trợ nhau, nhưng không nên để khả năng tạo kết quả của máy vượt xa năng lực kiểm tra của con người. Nếu khoảng cách ấy tiếp tục mở rộng, có nguy cơ hình thành hai nền toán học song song: một do con người phát triển, một do AI tạo ra. Lối ra không phải từ chối công cụ mới, mà là yêu cầu công khai cách hệ thống vận hành, cho phép nhà nghiên cứu tự tái lập kết quả và đối chiếu độc lập. Các trường đại học, hiệp hội nghề nghiệp, cơ quan tài trợ và quỹ khoa học cần phối hợp xây dựng, quản trị các mô hình phục vụ nghiên cứu. Cộng đồng cũng phải giữ khả năng can thiệp và vô hiệu hóa hệ thống khi cần. AI có thể đề xuất lời giải nhanh hơn bất kỳ nhóm người nào; nhưng cho đến khi lập luận được kiểm tra và hiểu rõ, đó vẫn là một kết quả cần thẩm định, chưa phải tri thức toán học đáng tin.
