Các nhà khoa học máy tính đang xây dựng một hệ thống AI với khả năng giành huy chương vàng tại cuộc thi toán toàn cầu IMO.

Olympic Toán Quốc tế lần thứ 61 đã chính thức khởi động và dự kiến sẽ đi vào lịch sử bởi ít nhất là hai lý do: Thứ nhất, đây là lần đầu tiên kỳ thi này được tổ chức từ xa do ảnh hưởng của đại dịch COVID-19. Thứ hai, đây có thể sẽ là kỳ thi cuối cùng trước khi có sự xuất hiện của Trí tuệ nhân tạo (AI).

Các nhà nghiên cứu cho rằng IMO là môi trường hoàn hảo để các máy tính (với thiết kế để có thể suy nghĩ như con người) thể hiện tài năng của mình. Nếu hệ thống AI có thể làm tốt tại IMO, thì công nghệ này sẽ đạt được một thành tựu lớn – chạm đến một khía cạnh quan trọng trong nhận thức của con người.

Hàng năm, các học sinh giỏi toán nhất thế giới vẫn cạnh tranh tại đấu trường Olympic Toán Quốc tế IMO (International Mathematical Olympiad). Tuy nhiên, sớm thôi, sẽ có một AI cạnh tranh với họ. Valerie Kuypers/AFP qua Getty Images.

Cá nhân tôi cho rằng, IMO sẽ đem lại những bài toán khó nhất để những cá nhân thông minh nhất có thể học cách giải một cách đáng tin cậy,” Selsam – nhân viên tại Microsoft Research phát biểu. Selsam là một trong những nhà sáng lập ra Thử thách IMO (IMO Grand Challenge), với mục tiêu huấn luyện một hệ thống AI có khả năng giành huy chương vàng tại giải đấu về toán học quy mô toàn cầu này.

IMO bắt đầu từ năm 1959, là một cuộc thi giành cho những học sinh bậc K-12 giỏi toán nhất trên thế giới. Trong hai ngày thi đấu, các thí sinh sẽ có 4,5 tiếng đồng hồ để giải 3 bài toán với mức độ khó tăng dần. Với mỗi bài toán, thí sinh sẽ giành được tối đa là 7 điểm, những thí sinh đạt điểm cao nhất sẽ giành huy chương – tương tự như tại Olympic. Những thí sinh IMO nổi tiếng nhất sau đó sẽ trở thành huyền thoại trong cộng đồng toàn học, và thậm chí là các nhà nghiên cứu và nhà toán học chuyên sâu.

Các bài toán của IMO không cần tới toán cao cấp để giải, hay thậm chí là tích phân, những vẫn cực kỳ “khó nhằn”. Để minh họa, sau đây là một bài toán xuất hiện trong đề thi IMO 1987, được tổ chức tại Cuba: “n là một số nguyên lớn hơn hoặc bằng 3. Hãy chứng minh rằng có tồn tại một tập n điểm ở trên cùng một mặt phẳng sao cho khoảng cách giữa 2 điểm bất kỳ là số vô tỷ, và mọi tam giác được tạo thành từ 3 điểm bất kỳ đều là tam giác không suy biến với diện tích là số hữu tỷ”. Cũng như nhiều bài toán IMO khác, việc tìm được lời giải dường như là bất khả thi.

Nhiều người sẽ đọc câu hỏi rồi tự nhủ rằng, ‘Tôi không thể giải được,” Kevin Buzzard – người đến từ Đại học Hoàng gia London, một thành viên của đội ngũ IMO Grand Challenge, đồng thời là người về nhất cuộc thi IMO năm 1987, chia sẻ. “Đó là các câu hỏi vô cùng khó, nhưng học sinh sẽ có thể giải được nếu họ biết cách sắp xếp các ý tưởng của mình một cách hợp lý”. 

Để giải quyết được các bài toán như vậy, ta cần phải xây dựng một tiền đề vô cùng khó, thậm chí là bất khả thi với các AI ở hiện tại. Ví dụ, một trong những câu trả lời toán học đầu tiên đến từ Euclid vào 300 năm trước Công Nguyên – người đã chứng minh rằng có vô hạn số nguyên tố. Lời giải này tới từ nhận thức rằng, ta luôn có thể tạo ra các số nguyên tố mới thông qua việc lấy tích của các số nguyên tố nhỏ hơn và cộng thêm 1. Việc chứng minh sau khi nhận thức được điều này là vô cùng dễ dàng – chính sự nhận thức, hay ý tưởng đầu tiên về câu hỏi, mới là thứ khó khăn.

Đội ngũ IMO Grand Challenge đang sử dụng một chương trình phần mềm có tên gọi là Lean – được triển khai lần đầu vào năm 2013 bởi Leonardo de Moura – một nhà nghiên cứu tại Microsoft. Lean là một “trợ lý chứng minh”, với khả năng kiểm tra công trình của các nhà toán học, sau đó tự động hóa một số quy trình buồn tẻ nhưng cần thiết cho việc chứng minh.

De Moura và các đồng nghiệp thì mong muốn Lean có thể trở thành một “người giải đáp”, tức có khả năng tự đưa ra các lời giải cho những câu hỏi IMO. Tuy nhiên, ở hiện tại, phần mềm này còn không hiểu được các khái niệm bên trong câu hỏi. Nếu Lean muốn cải thiện, thì trước hết nó phải thay đổi hai yếu tố sau.

Trước hết, Lean cần phải học nhiều toán hơn, sử dụng một thư viện toán có tên gọi mathlib – được cập nhật liên tục. Hiên nay, mathlib đã bao gồm mọi vấn đề về toán ở trình độ năm thứ hai đại học đổ lại, tuy nhiên nó vẫn gặp khó khăn ở một số khái niệm nhỏ để giải quyết các câu hỏi IMO.

Thử thách tiếp theo, khó khăn hơn, đó là phải dạy được Lean cách sử dụng các kiến thức mà phần mềm này sở hữu. Cụ thể, đội ngũ IMO Grand Challenge muốn huấn luyện Lean sao cho phần mềm này có thể tiếp cận được việc chứng minh toán học, tương tự như cách các hệ thống AI khác đã học được hai môn cờ phức tạp là cờ vua và cờ vây. Bằng cách tuân thủ cây quyết định (decision tree) cho tới khi tìm được nước cờ/lời giải thích hợp nhất.

Nếu máy tính có thể nghĩ ra ý tưởng ban đầu bằng cách sàng lọc vô số các ý tưởng khác cho tới khi tìm ra hướng giải đúng, thì có lẽ ta sẽ hoàn thành được thử thách IMO Grand Challenge,” Buzzard nói.

Với các bài toán không phức tạp, việc chứng minh về cơ bản là một chuỗi các bước cụ thể và logic. Lean có thể giải được các bài toán này nếu các nhà nghiên cứu IMO cho nó thấy mọi chi tiết của các chứng minh cũ. Tuy nhiên, lúc này mọi chứng minh lại trở nên quá cụ thể, và không thể sử dụng khi liên hệ tới những câu hỏi khác.

Để khắc phục vấn đề này, đội ngũ IMO Grand Challenge cần phải thuê các nhà toán học viết ra các lời giải chi tiết cho các câu hỏi IMO trước đây. Sau đó, họ sẽ lấy những lời giải này để phân tích và tìm hiểu các kỹ thuật/chiến thuật dẫn tới thành công. Tiếp theo, họ sẽ huấn luyện một hệ thống AI có khả năng tìm kiếm các kết hợp “thành công”, qua đó giải được các câu hỏi IMO mới. Theo Selsam, vấn đề nằm ở độ khó, bởi độ khó khi giải một bài toán gấp nhiều lần việc chiến thắng các boardgame khó nhất.

Mục tiêu của cờ vây là tìm ra nước đi tốt nhất, còn mục tiêu của toán là tìm ra trò chơi tốt nhất, sau đó tìm ra nước đi tốt nhất trong trò chơi này,” Selsam giải thích.

Hiện tại, thử thách IMO Grand Challenge vẫn là một điều rất xa vời. Moura khẳng định rằng nếu Lean tham gia vào cuộc thi năm nay, thì số điểm phần mềm này đạt được sẽ là một điểm không tròn trĩnh.

Tuy nhiên, các nhà nghiên cứu lại đã đề ra một số mốc nhất định mà họ muốn đạt được trước khi cuộc thi năm sau được tổ chức. Đầu tiên, họ muốn lấp đầy các khoảng trống trong mathlib, qua đó giúp Lean hiểu được toàn bộ câu hỏi. Sau đó, họ sẽ thu thập các lời giải chi tiết cho thật nhiều bài toán IMO trước đây, mang lại một nền tảng khởi động cho Lean. Một khi đã hoàn thiện được hai mốc này, thì Lean, nếu không thể giành huy chương vàng thì ít nhất cũng sẽ đủ tư cách làm thí sinh. Hiện tại mọi thứ còn đang mông lung, cho dù chúng tôi đang thực hiện vô cùng nhiều điều. Nhưng năm sau, chúng tôi sẽ thực sự khởi động,” Selsam nói.

Theo QuantaMagazine

Tin liên quan: