AI vừa giải được 4 bài toán bế tắc nhiều năm

Năng lực suy luận của AI được cho là có thể hỗ trợ thực chất cho các nhà toán học chuyên nghiệp

Năm năm trước, hai nhà toán học Dawei Chen và Quentin Gendron nghiên cứu một lĩnh vực phức tạp của hình học đại số liên quan đến vi phân - những công 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 chứng minh một định lý, họ vấp phải trở ngại bất ngờ: lập luận của họ phụ thuộc vào một công thức lạ trong lý thuyết số mà họ không thể chứng minh hay biện giải. Kết quả, công trình chỉ có thể được công bố dưới dạng giả thuyết thay vì định lý hoàn chỉnh.

Gần đây, ông Chen đã thử dành nhiều giờ “gợi ý” ChatGPT với hy vọng AI có thể tìm ra lời giải cho bài toán này, song không thành công. Bước ngoặt đến vào tháng trước, khi ông Chen 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 startup AI Axiom.

Sau khi nghe Chen trình bày về bài toán, ngay sáng hôm sau ông Ono đã đưa cho ông một bản chứng minh do hệ thống AI của công ty, mang tên AxiomProver, tạo ra. “Sau đó mọi thứ tự nhiên đâu vào đấy”, ông Chen cho biết. Ông đã phối hợp với Axiom hoàn thiện bản chứng minh, hiện đã được đăng tải trên arXiv, kho lưu trữ công khai các công trình khoa học.

AI được cho là đã tìm ra lời giải cho nhiều bài toán toán học tồn tại nhiều năm

Theo Axiom, công cụ của họ đã phát hiện mối liên hệ giữa bài toán này với một hiện tượng số học được nghiên cứu từ thế kỷ 19, sau đó xây dựng lời chứng minh và tự xác minh tính đúng đắn. “Điều AxiomProver tìm ra là thứ mà tất cả các nhà toán học con người đều đã bỏ sót”, ông Ono nói.

Đây chỉ là một trong số nhiều lời giải cho các bài toán chưa có lời giải mà Axiom cho biết hệ thống của họ đã tìm ra trong những tuần gần đây. AI của công ty chưa chinh phục được những bài toán nổi tiếng nhất của toán học, nhưng đã giải quyết được các câu hỏi khiến giới chuyên môn bế tắc nhiều năm, chẳng hạn một chứng minh liên quan đến Giả thuyết Fel trong đại số, gắn với các công thức xuất hiện trong sổ tay của nhà toán học Srinivasa Ramanujan hơn một thế kỷ trước. Ở trường hợp này, AI được cho là đã xây dựng toàn bộ chứng minh mà không cần con người hoàn thiện phần còn thiếu.

Những kết quả này được xem là bằng chứng cho thấy năng lực toán học của AI đang tiến bộ đều đặn. Thời gian gần đây, nhiều nhà toán học khác cũng cho biết họ sử dụng công cụ AI để khám phá ý tưởng mới và hỗ trợ giải quyết các vấn đề tồn tại.

Những kết quả này được xem là bằng chứng cho thấy năng lực toán học của AI đang tiến bộ đều đặn

Cách tiếp cận của Axiom kết hợp các mô hình ngôn ngữ lớn với một hệ thống AI độc quyền mang tên AxiomProver, được huấn luyện để suy luận toán học và tạo ra lời giải có thể chứng minh là đúng. Năm 2024, Google từng giới thiệu ý tưởng tương tự với hệ thống AlphaProof, tuy nhiên Axiom đã tích hợp thêm nhiều cải tiến và kỹ thuật mới.

Điểm khác biệt của hệ thống Axiom là khả năng xác minh chứng minh bằng một ngôn ngữ toán học chuyên biệt có tên Lean. Nhờ vậy, hệ thống không chỉ tìm kiếm trong tài liệu có sẵn mà còn có thể phát triển những cách giải quyết thực sự mới.

Các nhà nghiên cứu tham gia dự án cho rằng kết quả cho thấy AI có thể hỗ trợ thực chất cho các nhà toán học chuyên nghiệp. Axiom cũng nhận định những kỹ thuật này có thể được ứng dụng ngoài toán học, như kiểm chứng độ tin cậy của phần mềm trong lĩnh vực an ninh mạng.

Về phần mình, ông Chen bày tỏ sự lạc quan về vai trò của AI. Ông so sánh: 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, và tin rằng AI sẽ trở thành một công cụ thông minh mới, thậm chí là một “đối tác thông minh”, mở ra những chân trời rộng lớn hơn cho nghiên cứu toán học.

Hồng Nhung