Katie Collins, một nhà nghiên cứu tại Đại học Cambridge chuyên về toán học và AI nhưng không tham gia vào dự án, cho biết: “Thường sẽ dễ dàng hơn khi đào tạo một mô hình toán học nếu bạn có cách kiểm tra câu trả lời của nó (ví dụ, bằng ngôn ngữ chính thức), nhưng dữ liệu toán học chính thức trực tuyến tương đối ít hơn so với ngôn ngữ tự nhiên dạng tự do (ngôn ngữ không chính thức)”.
Thu hẹp khoảng cách này là mục tiêu của Google DeepMind khi tạo ra AlphaProof, một hệ thống dựa trên học tăng cường tự đào tạo để chứng minh các phát biểu toán học trong ngôn ngữ lập trình chính thức Lean. Chìa khóa là phiên bản Gemini AI của DeepMind được tinh chỉnh để tự động dịch các bài toán được diễn đạt bằng ngôn ngữ tự nhiên, không chính thức thành các phát biểu chính thức, dễ xử lý hơn đối với AI. Điều này đã tạo ra một thư viện lớn các bài toán chính thức với nhiều mức độ khó khác nhau.
Wenda Li, giảng viên về AI lai tại Đại học Edinburgh, người đã bình duyệt nghiên cứu nhưng không tham gia vào dự án, cho biết tự động hóa quá trình dịch dữ liệu sang ngôn ngữ chính thức là một bước tiến lớn đối với cộng đồng toán học.
Ông nói thêm: “Chúng ta có thể tin tưởng hơn nhiều vào tính chính xác của các kết quả đã công bố nếu họ có thể xây dựng được hệ thống chứng minh này và nó cũng có thể mang tính cộng tác hơn”.
Mô hình Gemini hoạt động cùng với AlphaZero—mô hình học tăng cường mà Google DeepMind đã đào tạo để thành thạo các trò chơi như Cờ vây và cờ vua—để chứng minh hoặc bác bỏ hàng triệu bài toán. Càng giải quyết thành công nhiều bài toán, AlphaProof càng trở nên giỏi hơn trong việc giải quyết các bài toán có độ phức tạp ngày càng tăng.
Mặc dù AlphaProof được đào tạo để giải quyết các vấn đề trong nhiều chủ đề toán học khác nhau, AlphaGeometry 2—một phiên bản cải tiến của hệ thống mà Google DeepMind công bố vào tháng 1—đã được tối ưu hóa để giải quyết các vấn đề liên quan đến chuyển động của các vật thể và các phương trình liên quan đến góc, tỷ lệ và khoảng cách. Vì được đào tạo trên nhiều dữ liệu tổng hợp hơn đáng kể so với phiên bản trước, nên nó có thể giải quyết các câu hỏi hình học khó hơn nhiều.