AI của DeepMind giải đề Olympic Toán học Quốc tế ở mức huy chương bạc

(deepmind.google)

3 điểm bởi GN⁺ 2024-07-26 | 3 bình luận | Chia sẻ qua WhatsApp

AlphaProof và AlphaGeometry 2 của Google DeepMind đã giải được các bài toán trong Olympic Toán học Quốc tế
- AlphaProof: hệ thống suy luận toán học dựa trên học tăng cường
- AlphaGeometry 2: hệ thống giải bài toán hình học được cải tiến
- Hai hệ thống đã giải được 4 trong 6 bài tại Olympic Toán học Quốc tế (IMO) năm nay, đạt thành tích ở mức huy chương bạc

Thành tựu AI trong việc giải các bài toán phức tạp

Giới thiệu về IMO
- Cuộc thi toán học dành cho thanh thiếu niên lâu đời và danh giá nhất, được tổ chức hằng năm từ năm 1959
- Đề thi bao gồm các lĩnh vực như đại số, tổ hợp, hình học và lý thuyết số
- Nhiều người đoạt Fields Medal từng xuất thân từ IMO
Thử thách IMO của các hệ thống AI
- AlphaProof và AlphaGeometry 2 đã giải các bài của IMO năm nay
- Các bài được chấm điểm theo đúng quy tắc chính thức của cuộc thi
- AlphaProof giải được 2 bài đại số và 1 bài lý thuyết số
- AlphaGeometry 2 giải được 1 bài hình học
- Hai bài tổ hợp vẫn chưa được giải
- Tổng cộng giành được 28 trên 42 điểm, tương đương mức huy chương bạc

AlphaProof: cách tiếp cận suy luận hình thức

Cách AlphaProof hoạt động
- Chứng minh các mệnh đề toán học bằng ngôn ngữ hình thức Lean
- Kết hợp mô hình ngôn ngữ được tiền huấn luyện với thuật toán học tăng cường AlphaZero
- Dịch bài toán ngôn ngữ tự nhiên thành các mệnh đề hình thức để giải những bài ở nhiều mức độ khó khác nhau
- Khi nhận bài toán, AlphaProof tạo ra các ứng viên lời giải rồi chứng minh hoặc bác bỏ chúng
- Các kết quả đã được chứng minh sẽ tiếp tục củng cố mô hình ngôn ngữ của AlphaProof, giúp nâng cao khả năng giải các bài khó hơn
Quy trình huấn luyện
- Được huấn luyện bằng cách chứng minh hoặc bác bỏ hàng triệu bài toán
- Ngay trong thời gian diễn ra cuộc thi, hệ thống vẫn áp dụng vòng lặp huấn luyện để chứng minh các biến thể của bài toán

AlphaGeometry 2 cạnh tranh hơn

Các cải tiến của AlphaGeometry 2
- Mô hình ngôn ngữ dựa trên Gemini cùng hệ thống lai thần kinh-ký hiệu
- Được huấn luyện với lượng dữ liệu tổng hợp nhiều hơn gấp 10 lần so với phiên bản trước
- Tốc độ và độ chính xác khi giải bài toán hình học được cải thiện
- Sử dụng cơ chế chia sẻ tri thức khi giải các bài toán mới
Thành tích tại IMO 2024
- Giải được 83% các bài hình học của IMO trong 25 năm qua
- Tại cuộc thi năm nay, đã giải bài số 4 chỉ trong 19 giây

Biên giới mới của suy luận toán học

Thử nghiệm hệ thống suy luận ngôn ngữ tự nhiên
- Thử nghiệm một hệ thống suy luận ngôn ngữ tự nhiên dựa trên Gemini
- Có thể giải bài toán mà không cần dịch sang ngôn ngữ hình thức
- Khám phá khả năng kết hợp với các hệ thống AI khác
Triển vọng tương lai
- Các nhà toán học có thể hợp tác với công cụ AI để khám phá giả thuyết mới, thử các cách tiếp cận giải bài toán và rút ngắn quá trình chứng minh
- Các hệ thống AI như Gemini sẽ tiếp tục nâng cao năng lực toán học và suy luận tổng quát

Tóm tắt của GN⁺

AlphaProof và AlphaGeometry 2 cho thấy tiềm năng của AI trong suy luận toán học
Việc đạt thành tích ở mức huy chương bạc tại Olympic Toán học Quốc tế chứng minh năng lực giải toán của AI
Mở ra khả năng để các nhà toán học hợp tác với AI nhằm khám phá những cách tiếp cận giải quyết vấn đề mới
Một dự án có chức năng tương tự là các mô hình xử lý ngôn ngữ tự nhiên như GPT-3 của OpenAI

3 bình luận

chabulhwi 2024-07-26

Càng có nhiều nhà toán học đóng góp vào việc phát triển thư viện toán học hình thức thì càng dễ tạo ra AI toán học có hiệu năng tốt. Theo tôi được biết, hiện có 3 người Hàn Quốc đang chuyển các lý thuyết toán học do chính họ hình thức hóa bằng ngôn ngữ của trợ lý chứng minh Lean sang Mathlib, thư viện toán học của Lean.

Năm ngoái tôi có tham gia một phần vào công việc chuyển Mathlib từ Lean 3 sang Lean 4, và năm nay tôi đã chứng minh được một định lý chưa giải quyết trong thư viện Batteries của Lean 4.

GN⁺ 2024-07-26

Ý kiến Hacker News

Ý kiến thứ nhất
- Rất hào hứng với dự án này, nhưng chưa rõ máy tính đã đóng góp bao nhiêu trong quá trình chuyển các bài toán sang ngôn ngữ hình thức
- Trong lời giải có thể tải xuống, không rõ đâu là phần do con người quyết định trong quá trình chuyển đổi và đâu là phần do máy tính tìm ra
Ý kiến thứ hai
- Tại IMO, huy chương được trao cho 50% thí sinh, và tỷ lệ huy chương vàng, bạc, đồng là 1:2:3
- Việc AI giải tốt hơn 75% học sinh là rất ấn tượng
- Tuy nhiên, thời gian AI dùng để giải bài khác với thời gian làm bài mà học sinh được cấp trong kỳ thi, nên so sánh trực tiếp là không phù hợp
Ý kiến thứ ba
- AlphaGeometry đã giải các bài toán bị giới hạn, nhưng phương pháp lần này sẽ có ảnh hưởng rộng hơn đến toán học
- Họ đang triển khai một pipeline chuyển đổi toán học ngôn ngữ tự nhiên sang toán học hình thức, và điều này cũng có thể học cách xây dựng lý thuyết nền tảng
- Đây là chén thánh của hỗ trợ chứng minh, và sẽ giúp con người hình thức hóa toán học một cách tự nhiên hơn
Ý kiến thứ tư
- Nếu hệ thống mất 3 ngày để giải bài toán, thì điều đó chẳng khác gì vét cạn đơn thuần
- Đây không phải là suy luận thực sự
Ý kiến thứ năm
- Đang sử dụng Lean
- Điều này quan trọng không chỉ với các bài toán mà còn để tránh các kết quả vô nghĩa nói chung
- Hy vọng sẽ có nhiều người viết type trong các hệ thống như Lean hơn
Ý kiến thứ sáu
- Ghen tị với những người tham gia dự án này
- Việc thúc đẩy công nghệ tiên tiến nhất hẳn sẽ rất vui và thỏa mãn
Ý kiến thứ bảy
- Những cuộc thảo luận hay nhất diễn ra trong chat Zulip của LeanProver
Ý kiến thứ tám
- Tim Gowers, người đoạt Huy chương Fields, đã đưa ra một bản tổng quan tốt, giải thích các điểm cần lưu ý chính và cung cấp bối cảnh
Ý kiến thứ chín
- Chứng minh định lý là một trò chơi một người chơi với không gian tìm kiếm rất lớn
- Những người đóng góp lớn nhất cho AlphaProof là các nhà phát triển Lean và Mathlib
- Sự thiếu hụt hình thức hóa trong các bài báo toán học đã cản trở các nỗ lực tự động hóa
Ý kiến thứ mười
- Máy móc đã vượt con người ở cờ vua trong nhiều thập kỷ
- Nhưng mọi người vẫn xem Magnus Carlsen
- Con người quan tâm đến hành động của những con người khác
- Máy móc chỉ đáng quan tâm trong chừng mực chúng hữu ích cho con người