AI giải thành công 4 bài toán hóc búa của Toán học: các giáo sư đầu ngành cũng phải thốt lời khen

Năm năm trước, hai nhà toán học Dawei Chen và Quentin Gendron đang tìm cách gỡ một nút thắt hóc búa trong hình học đại số, liên quan đến vi phân, một lĩnh vực của giải tích dùng để đo khoảng cách trên các bề mặt cong. Trong quá trình xây dựng định lý, họ gặp phải một rào cản bất ngờ: lập luận của họ phụ thuộc vào một công thức kỳ lạ trong lý thuyết số, một công thức họ không thể giải hoặc biện minh.

Cuối cùng, Chen và Gendron đành công bố ý tưởng của mình dưới dạng một giả thuyết chứ không phải định lý. Nhưng thời gian gần đây, công trình nghiên cứu của hai nhà toán học có bước tiến mới nhờ trí tuệ nhân tạo.

Ban đầu, ông Chen thử trò chuyện với ChatGPT để tìm lời giải nhưng vô hiệu. Nhưng tại hội nghị toán học mới diễn ra tại Washington, ông Chen chính thức bước tới “ngã rẽ cuộc đời”: ông gặp Ken Ono, một nhà toán học nổi tiếng vừa rời Đại học Virginia để gia nhập Axiom, một startup trí tuệ nhân tạo do một trong những học trò của ông là Carina Hong đồng sáng lập.

Chen kể cho Ono nghe về bài toán. Sáng hôm sau, Ono mang đến cho Chen một bài giải hoàn chỉnh, do công cụ AI giải toán của startup là AxiomProver tạo ra. Nhận thấy tiềm năng từ phương pháp suy luận của AI, ông Chen đã cùng Axiom viết lại chứng minh này, và hiện kết quả đã được đăng lên arXiv.

Không giống các mô hình AI phổ thông, AxiomProver được thiết kế để suy luận toán học một cách có hệ thống và kiểm chứng kết quả bằng ngôn ngữ chuyên dụng có tên “Lean”. Chính điều này cho phép nó không chỉ tìm lại kiến thức cũ, mà còn phát hiện ra những mối liên hệ mà con người đã bỏ lỡ, từ đó xây dựng các chứng minh hoàn toàn mới.

Thành công với giả thuyết Chen-Gendron chỉ là một trong nhiều ví dụ. AxiomProver còn tự mình giải Giả thuyết Fel, một bài toán gắn với các công thức của thiên tài toán học Srinivasa Ramanujan hơn một thế kỷ trước, cũng như những vấn đề phức tạp khác trong lý thuyết số và xác suất.

Chứng minh thứ ba do AI của Axiom tạo ra liên quan đến một mô hình xác suất về các "ngõ cụt" trong lý thuyết số. Chứng minh thứ tư sử dụng các công cụ toán học vốn được phát triển để giải được Định lý cuối cùng của Fermat, một trong những thách thức nổi tiếng nhất của ngành Toán.

“Ngay cả với tôi, người đã theo dõi sát sự phát triển của các công cụ AI cho toán học suốt nhiều năm và trực tiếp làm việc với chúng, điều này vẫn thật đáng kinh ngạc”, Scott Kominers, giáo sư tại Trường Kinh doanh Harvard, nhận định. “Không chỉ là việc AxiomProver giải được một bài toán như vậy một cách hoàn toàn tự động và được kiểm chứng ngay lập tức, mà còn là sự thanh thoát và vẻ đẹp của toán học mà nó tạo ra”.

Với Axiom, toán học không còn là mục tiêu mục tiêu đơn thuần, đây chính là lĩnh vực để trí tuệ nhân tạo thử nghiệm khả năng suy luận và kiểm chứng. Nếu những kỹ thuật này được mở rộng sang các lĩnh vực khác, từ phần mềm đến an ninh mạng, vai trò của AI có thể vượt xa hình ảnh một công cụ hỗ trợ đơn thuần. Trong con mắt của nhiều nhà toán học, AI đang dần trở thành một đối tác trí tuệ thực thụ.

Chen, người vừa chứng kiến giả thuyết của mình được Axiom giải quyết, cũng tỏ ra lạc quan về tác động của AI đối với lĩnh vực này. “Các nhà toán học không quên bảng cửu chương sau khi máy tính bỏ túi ra đời”, ông Chen nói. “Tôi tin AI sẽ đóng vai trò như một công cụ thông minh mới, hay đúng hơn là một ‘đối tác thông minh’, mở ra những chân trời phong phú và rộng lớn hơn cho nghiên cứu toán học”.