Góc nhìn của một nhà toán học về năng lực toán học của AI

• Mô hình ngôn ngữ mới o3 của OpenAI đạt 25% trên bài benchmark toán khó FrontierMath, làm lung lay lại cách đánh giá liệu AI làm toán có thể vượt mức đại học hay không
• FrontierMath là bộ dữ liệu kín do Epoch AI tạo ra, gồm hàng trăm bài toán khó đòi hỏi đáp án số có thể kiểm chứng tự động thay vì “chứng minh định lý”
• 5 mẫu công khai cũng không hề dễ ngay cả với các nhà toán học nghiên cứu; Tao đánh giá là “cực kỳ thách thức”, còn Borcherds cho rằng việc đưa ra đáp án số không đồng nghĩa với chứng minh sáng tạo
• Elliot Glazer của Epoch AI cho biết 25% bài trong bộ là “bài kiểu IMO/đại học”, nên do tính chất bộ dữ liệu kín, rất khó xác nhận điểm 25% của o3 thực sự tương ứng với mức độ khó nào
• Mục tiêu quan trọng hơn với giới toán học không phải là “hãy tìm con số này” mà là chứng minh định lý một cách đúng đắn và giải thích sao cho con người hiểu được; cách tiếp cận bằng mô hình ngôn ngữ và Lean có những giới hạn khác nhau

---

o3 và FrontierMath đã làm rung chuyển mốc chuẩn

• o3 là mô hình ngôn ngữ mới của OpenAI và đạt 25% trên FrontierMath
• Kể từ sau ChatGPT, các mô hình ngôn ngữ công khai đã cải thiện rất nhanh, và năng lực giải toán cũng được đánh giá trong dòng tiến bộ đó
• FrontierMath là bộ dữ liệu bài toán toán học kín do Epoch AI tạo ra; phần tóm tắt bài báo nói rằng có “hàng trăm” bài toán khó
• Nếu công khai bộ dữ liệu, mô hình ngôn ngữ có thể học cả đề lẫn đáp án, nên ngay cả thông tin cơ bản như số lượng bài cũng được xử lý rất thận trọng
  • Nếu đề và đáp án bị lộ, mô hình có thể lặp lại đáp án đã từng thấy
  • Vì vậy, rất khó để bên ngoài kiểm chứng độ khó thực tế và tính đại diện của một benchmark kín

Hình thức và độ khó của các bài trong FrontierMath

• Các bài trong FrontierMath gần với dạng “hãy tìm con số này” hơn là “hãy chứng minh định lý này”
• Bài toán phải có đáp án rõ ràng, tính toán được và có thể kiểm chứng tự động
• Đáp án của cả 5 bài mẫu công khai đều là số nguyên dương
  • Ví dụ có các đáp án 9811 và 367707
  • Ba đáp án còn lại lớn hơn, được thiết kế để khó đoán trúng bằng đoán mò
• Các mẫu công khai là không tầm thường ngay cả với nhà toán học nghiên cứu
  • Tác giả đều hiểu phát biểu của cả 5 bài
  • Bài thứ ba có thể giải tương đối nhanh; với bài thứ năm, tác giả biết cách giải bằng kỹ thuật chuẩn dùng Weil conjectures for curves nhưng không tính ra đáp án 13 chữ số
  • Tác giả cho rằng không giải được bài một và bài hai; còn bài bốn có thể tiến triển nếu bỏ công sức, nhưng đã không thử mà đọc lời giải
• Ngay cả một sinh viên đại học toán rất giỏi thông thường cũng có thể khó giải được bất kỳ bài nào trong số này
  • Bài đầu tiên có lẽ đòi hỏi ít nhất trình độ nghiên cứu sinh về giải tích số

Ưu điểm và giới hạn của benchmark đáp án số

• Lý do cốt lõi FrontierMath dùng các bài có đáp án số là chi phí chấm điểm
• Nếu phải chấm hàng trăm lời giải dạng “hãy chứng minh định lý”, sẽ cần tới chuyên gia con người
  • Tính đến năm 2024, việc giao mức chấm này cho máy vẫn bị xem là khó
• Trong khi đó, một danh sách đáp án số có thể được máy tính đối chiếu rất nhanh
• Borcherds cho rằng nhà toán học nghiên cứu dành phần lớn thời gian để tìm chứng minh và ý tưởng, chứ không phải con số
• Dù vậy, FrontierMath vẫn có giá trị với lĩnh vực AI toán học
  • Các bộ dữ liệu khó hiện rất khan hiếm
  • Việc tạo ra những bộ dữ liệu như vậy là cực khó hoặc rất tốn kém
  • Bài viết gần đây của Frieder và cộng sự bàn sâu hơn về giới hạn của các bộ dữ liệu AI toán học

Vì sao mốc 25% của o3 gây bất ngờ

• Theo nhận thức trước đây, AI toán học vẫn gần với mức đại học hoặc trước đại học
• AI đang trở nên rất mạnh ở các bài kiểu olympiad mà học sinh trung học xuất sắc giải được
• Có thể thấy rõ rằng trong vòng 1 năm, AI sẽ vượt qua các kỳ thi toán đại học
  • Đề thi đại học thường có những bài chuẩn hóa để sinh viên hiểu cơ bản môn học có thể vượt qua
  • Máy có thể làm tốt những bài kiểu này
• Nhưng bước nhảy từ việc tái sử dụng ý tưởng chuẩn sang những ý tưởng mới ở mức đại học nâng cao hoặc đầu nghiên cứu sinh là rất lớn
• Các câu trả lời gần đây của ChatGPT cho kỳ thi Putnam không đạt kỳ vọng
  • Có vẻ chỉ bài B4 được máy trả lời tương đối đúng
  • Hầu hết các câu khác chỉ ở mức 1–2 điểm trên thang 10
• Vì thế, FrontierMath từng được dự đoán là gần như không thể công phá trong vài năm tới

Sự bất định do bộ dữ liệu kín để lại

• Elliot Glazer của Epoch AI nói trên Reddit rằng 25% bài trong FrontierMath là bài kiểu IMO/đại học
• Điều này có vẻ không khớp lắm với 5 bài mẫu công khai
  • Ngay cả bài dễ nhất trong số các mẫu công khai cũng có một cách giải dùng Weil conjectures for curves
  • Hoặc có thể cần một cách brute force đau đớn để phân tích nhân tử một đa thức bậc ba có bậc 10^12 trên trường hữu hạn
• Thông tin này làm dấy lên câu hỏi về độ khó thực của bộ dữ liệu kín và liệu 5 bài công khai có phải mẫu đại diện hay không
• Vì bộ dữ liệu không công khai, những nghi vấn này rất khó kiểm tra
• Nếu 25% là các bài ở mức đại học, thì điểm 25% của o3 có thể bớt gây ngạc nhiên hơn
• Bước đột phá lớn được chờ đợi là khi AI thể hiện năng lực đáng kể ở 50% bài tiếp theo, được mô tả ở mức “qual level”

“Hãy chứng minh định lý” vẫn là một bài toán khác

• Trong nghiên cứu toán học, câu hỏi quan trọng thường là “hãy chứng minh định lý này”
• Ngay cả khi xuất hiện cỗ máy đạt năng lực siêu nhân ở các bài tìm số, khả năng ứng dụng vào nhiều nhánh toán nghiên cứu vẫn có thể bị hạn chế
• Thành công lớn nhất của năm 2024 thường được nhắc đến là AlphaProof của DeepMind
  • AlphaProof đã giải được 4 trên 6 bài IMO 2024
  • Các bài này thuộc dạng “hãy chứng minh định lý” hoặc “hãy tìm con số và chứng minh nó là đúng”
  • Trong số đó, 3 bài được xuất ra dưới dạng chứng minh Lean đã hình thức hóa hoàn toàn
• Lean là một trình chứng minh định lý tương tác, còn mathlib là thư viện toán học bao gồm nhiều kỹ thuật cần cho việc giải bài IMO và hơn thế nữa
• Lời giải của hệ thống DeepMind đã được con người kiểm tra và xác nhận là lời giải “điểm tuyệt đối”
• Tuy nhiên, dù bài IMO rất khó, lời giải vẫn chỉ dùng các kỹ thuật ở mức phổ thông, nên rốt cuộc lại quay về bài toán trình độ trung học
• Dự đoán rằng đến năm 2025, máy sẽ đạt năng lực cỡ huy chương vàng IMO

Ai sẽ chấm lời giải của máy

• Có thể hình dung tới tháng 7/2025 tại IMO, không chỉ học sinh mà cả máy cũng tham gia
• Các hệ thống máy có thể chia thành hai loại
  • Hệ thống nộp lời giải bằng ngôn ngữ của trình kiểm tra chứng minh bằng máy tính như Lean, Rocq, Isabelle
  • Các mô hình ngôn ngữ nộp lời giải bằng ngôn ngữ của con người
• Với lời giải nộp bằng ngôn ngữ của trình kiểm tra chứng minh, chỉ cần xác nhận phát biểu bài toán đã được dịch đúng
  • Sau đó, nếu chứng minh biên dịch được thì về cơ bản có thể biết đó là lời giải “điểm tuyệt đối”
• Mô hình ngôn ngữ nộp đáp án bằng ngôn ngữ tự nhiên thì khác
  • Dù lời giải trông có vẻ hợp lý, người chấm vẫn phải đọc kỹ và đánh giá
  • Không có gì đảm bảo đó là lời giải điểm tuyệt đối
• Mô hình ngôn ngữ được cho là kém chính xác hơn chuyên gia con người ít nhất một bậc độ lớn trong suy luận logic
• Có lo ngại rằng một “chứng minh” của mô hình ngôn ngữ về giả thuyết Riemann có thể trộn lẫn các khẳng định mơ hồ hoặc không chính xác vào giữa 10 trang toán học đúng
• Ngược lại, các trình chứng minh định lý được xem là chính xác hơn ít nhất một bậc độ lớn
  • Trong những trường hợp tác giả từng thấy, khi Lean không chấp nhận một lập luận trong tài liệu toán của con người thì phía con người mới là bên sai

Mục tiêu còn lại: chứng minh đúng và con người hiểu được

• Điều các nhà toán học muốn không chỉ là “hãy chứng minh định lý” mà còn là một chứng minh chính xác và cách giải thích để con người hiểu được
• Với cách tiếp cận bằng mô hình ngôn ngữ, “độ chính xác” vẫn là mối lo lớn
• Với cách tiếp cận bằng trình chứng minh định lý, điều đáng lo là “trình bày sao cho con người hiểu được”
• Vẫn còn rất nhiều việc phải làm
• Tốc độ tiến bộ rất nhanh, nhưng không ai biết khi nào AI sẽ vượt qua rào cản bậc đại học