Tiến sĩ Việt tạo AI giải Toán ngang thí sinh đoạt huy chương vàng IMO

AlphaGeometry vừa gây chấn động giới toán học. Ảnh: Sabeswings.

Một công cụ trí tuệ nhân tạo (AI) có tên AlphaGeometry vừa gây chấn động giới toán học khi chứng minh thành công tính đúng sai của các định lý hình học - những mệnh đề về các hình phẳng như tam giác hay đa giác - với độ chính xác ngang ngửa với thí sinh giành huy chương vàng Olympic Toán quốc tế (IMO).

AlphaGeometry được giới thiệu trên tạp chí Nature ngày 17/1. Điều đặc biệt, tác giả chính của AlphaGeometry là TS Trịnh Hoàng Triều (29 tuổi, tốt nghiệp Đại học New York, Mỹ) và TS Lương Minh Thắng (36 tuổi, Đại học Stanford, Mỹ).

Nhóm nghiên cứu còn có 3 tác giả khác là GS He He (nhà khoa học máy tính tại Đại học New York, cố vấn của TS Triều), TS Lê Viết Quốc và Yuhuai Wu (đồng sáng lập xAI - trước đây thuộc Google). Ngoại trừ GS He He, 4 người còn lại đều là chuyên gia tại Google DeepMind - phòng thí nghiệm nghiên cứu AI của Google.

Khi được thử nghiệm trên một bộ 30 bài toán hình học của IMO, AlphaGeometry đã giải được 25 bài. Thành tích này gần tiệm cận với khả năng của những thí sinh xuất sắc nhất của cuộc thi, ít nhất là trong lĩnh vực hình học.

Nhà toán học Kevin Buzzard, Đại học Imperial College London, nhấn mạnh rằng hình học chỉ là một trong nhiều lĩnh vực mà thí sinh IMO phải giỏi. Việc AlphaGeometry đạt được trình độ tương đương trong các lĩnh vực khác của IMO, chẳng hạn như lý thuyết số, có thể khó khăn hơn nhiều.

"Tuy nhiên, việc AlphaGeometry giải được 25 bài toán IMO và thậm chí có thể tạo ra các chứng minh dễ hiểu cho con người là điều rất ấn tượng", ông Buzzard nói.

Cách AlphaGeometry giải bài toán 3 IMO 2015. Ảnh: Nature.

Khắc phục rào cản ngôn ngữ

Để giải quyết các bài toán khác nhau, các nhà nghiên cứu đã thử nghiệm sử dụng các mô hình ngôn ngữ lớn - một dạng AI được huấn luyện trên kho dữ liệu văn bản khổng lồ, thường được sử dụng trong các chatbot phổ biến. Kết quả thu được nhiều hứa hẹn, nhưng thường vô nghĩa.

Ví dụ, Minerva, một chatbot chuyên về toán học do Google phát triển cho mục đích nghiên cứu, được huấn luyện bằng các bài nghiên cứu toán học chuyên sâu và cách giải các bài toán cơ bản của học sinh được viết bởi con người.

Mặc dù các con số Minerva đưa ra thường chính xác, nhưng cách giải thích bằng văn bản của nó lại thường sai sót và cần được con người kiểm tra.

"Nếu một hệ thống được huấn luyện bằng ngôn ngữ tự nhiên, nó sẽ cho ra kết quả bằng ngôn ngữ tự nhiên mà chúng ta không thể tin tưởng hoàn toàn”, TS Triều nhận định.

Để vượt qua rào cản này, TS Triều cùng cộng sự đã tạo ra một ngôn ngữ riêng cho AlphaGeometry, cho phép giải các bài toán hình học một cách chính xác và dễ hiểu. Ngôn ngữ này có cú pháp chặt chẽ, tương tự ngôn ngữ lập trình máy tính, cho phép kiểm tra dễ dàng bằng máy tính và vẫn dễ hiểu với con người.

Nhóm nghiên cứu tập trung vào các bài toán hình học Euclid, mục tiêu là viết một bằng chứng toán học cho một mệnh đề cho trước. Họ đã đưa vào ngôn ngữ tùy chỉnh này hàng chục quy tắc hình học cơ bản.

Để huấn luyện AlphaGeometry, nhóm nghiên cứu đã tạo ra 100 triệu bài giải tự động, mỗi bài là một chuỗi các bước đơn giản nhưng logic chặt chẽ, ví dụ "cho hai điểm A và B, hãy dựng hình vuông ABCD".

AlphaGeometry được huấn luyện trên những bằng chứng do máy tạo ra. Điều này có nghĩa là AI có thể giải các vấn đề bằng cách đoán từng bước một, tương tự như cách các chatbot tạo văn bản.

Nhưng nó cũng đồng nghĩa với việc kết quả có thể đọc được bằng máy và dễ dàng kiểm tra độ chính xác. Đối với mỗi bài toán, AlphaGeometry tạo ra nhiều cách giải khác nhau.

Do AI có thể tự động loại bỏ những đáp án sai, nó có thể đưa ra kết quả chính xác một cách đáng tin cậy, bao gồm cả các bài toán hình học từ IMO.

Các tác giả của AlphaGeometry (từ trái sang) - Yuhuai Wu, TS Trịnh Hoàng Triều, TS Lê Viết Quốc, TS Lương Minh Thắng. Ảnh: Nytimes.

Mục đích khác

Stephan Schulz, nhà khoa học máy tính tại Đại học Bang Baden-Württemberg, Đức, cho rằng lý do đằng sau thành công của AlphaGeometry chính là kết hợp sức mạnh phán đoán và lập luận logic. Ông nhấn mạnh cách tiếp cận tổng hợp này rất hứa hẹn.

Nhà toán học Kevin Buzzard cũng đồng ý rằng việc huấn luyện AlphaGeometry bằng dữ liệu tổng hợp đã loại bỏ rủi ro gian lận khi sử dụng mô hình ngôn ngữ lớn thông thường vào toán học.

Ông giải thích khi hệ thống được huấn luyện bằng hàng tỷ văn bản trên Internet, "rất khó đảm bảo rằng mô hình chưa từng gặp câu hỏi đó trước đây".

"Chúng tôi muốn xây dựng một hệ thống không cần dữ liệu của con người, để nó có thể vượt qua khả năng của con người một ngày nào đó", GS He He tiết lộ một mục đích khác của việc huấn luyện AlphaGeometry bằng các bằng chứng tự động tạo ra.

Tuy nhiên, các nhà toán học có lẽ vẫn chưa cần lo lắng về việc bị AI thay thế trong thời gian sớm.

Ông Buzzard nhận định trong vài năm tới, ông có thể hình dung các kỹ thuật như vậy có thể giải được các bài toán bậc đại học mà chỉ những sinh viên giỏi nhất mới làm được.

"Nhưng hiện tại, tôi chưa thấy bằng chứng nào cho thấy máy móc có thể tự động giải quyết các vấn đề toán học nghiên cứu hiện đại", ông Buzzard nói.

Ngọc Bích