AI của DeepMind giải đề Olympic Toán quốc tế ở mức huy chương bạc
(deepmind.google)- Tại IMO 2024, thước đo tiêu biểu cho suy luận toán học độ khó cao, AlphaProof và AlphaGeometry 2 của Google DeepMind đã giải được 4 trong 6 bài, lần đầu đưa AI đạt thành tích ở ngưỡng huy chương bạc
- Hệ thống đạt 28 điểm trên tổng 42 điểm, và cả 4 bài giải được đều được chấm điểm tuyệt đối; chỉ kém 1 điểm so với mốc huy chương vàng năm 2024 là 29 điểm
- Việc chấm điểm do các nhà toán học thực hiện theo quy tắc chấm của IMO; AlphaProof xử lý đại số và số học, còn AlphaGeometry 2 phụ trách hình học, kết hợp các phương thức suy luận khác nhau
- Các bài toán trước hết được dịch thủ công sang ngôn ngữ toán học hình thức; trong khi thí sinh có 2 buổi thi, mỗi buổi 4,5 giờ, thì hệ thống có bài chỉ mất vài phút nhưng các bài khác mất tới 3 ngày
- Kết quả lần này cho thấy AI toán học đã tiến từ tính toán đơn thuần sang tìm kiếm và kiểm chứng chứng minh, nhưng đầu vào đã được hình thức hóa và thời gian giải dài vẫn là những hạn chế quan trọng
Thành tích ở ngưỡng huy chương bạc tại IMO 2024
- Google DeepMind công bố hệ thống suy luận toán học AlphaProof và phiên bản cải tiến của hệ thống giải hình học AlphaGeometry 2
- Hai hệ thống đã giải được 4 trong 6 bài của International Mathematical Olympiad 2024
- AlphaProof: giải 2 bài đại số, 1 bài số học
- AlphaGeometry 2: chứng minh 1 bài hình học
- Không giải được 2 bài tổ hợp
- Mỗi bài tối đa 7 điểm, tổng điểm là 42
- Hệ thống giành điểm tuyệt đối ở cả 4 bài đã giải và đạt 28 điểm
- Mức này nằm ở nhóm trên của ngưỡng huy chương bạc IMO 2024
- Mốc huy chương vàng năm 2024 là 29 điểm, và trong kỳ thi chính thức có 58 trên 609 thí sinh đạt ngưỡng huy chương vàng
- Đây là trường hợp đầu tiên một hệ thống AI đạt thành tích ở mức huy chương bạc tại IMO
Cách đánh giá và điều kiện giải bài
- Đề bài sử dụng là các bài thi do ban tổ chức IMO cung cấp
- Bài làm được đánh giá theo quy tắc cho điểm của IMO
- Người chấm là Prof Sir Timothy Gowers, huy chương vàng IMO và chủ nhân Fields Medal, cùng Dr Joseph Myers, người hai lần giành huy chương vàng IMO và là chủ tịch IMO 2024 Problem Selection Committee
- Để hệ thống có thể hiểu bài toán, toàn bộ đề trước tiên được dịch thủ công sang ngôn ngữ toán học hình thức
- Trong kỳ thi chính thức, học sinh nộp bài trong hai buổi, mỗi buổi 4,5 giờ
- Hệ thống AI giải một bài trong vài phút, còn các bài khác mất tới 3 ngày
- Trong số các bài AlphaProof giải được có bài khó nhất của IMO 2024, bài mà chỉ có 5 thí sinh giải được
AlphaProof: suy luận hình thức dựa trên Lean
- AlphaProof là hệ thống được huấn luyện để chứng minh các mệnh đề toán học bằng ngôn ngữ hình thức Lean
- Hệ thống kết hợp mô hình ngôn ngữ tiền huấn luyện với thuật toán học tăng cường AlphaZero
- AlphaZero là thuật toán từng được dùng để tự học cờ vua, shogi và Go
- Việc sử dụng ngôn ngữ hình thức cho phép kiểm chứng tính chính xác của các chứng minh có chứa suy luận toán học
- Trước đây, dữ liệu chứng minh hình thức do con người viết rất ít, khiến việc sử dụng ngôn ngữ hình thức trong machine learning bị hạn chế
- Các cách tiếp cận dựa trên ngôn ngữ tự nhiên có thể dùng lượng dữ liệu lớn hơn nhiều, nhưng có thể tạo ra các bước suy luận trung gian hoặc lời giải nghe có vẻ hợp lý nhưng sai
- DeepMind đã fine-tune mô hình Gemini để tự động dịch bài toán ngôn ngữ tự nhiên thành mệnh đề hình thức, đồng thời tạo thư viện bài toán hình thức vớ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 khám phá những bước chứng minh khả thi trong Lean để chứng minh hoặc bác bỏ chúng
- Những chứng minh được tìm thấy và xác minh sẽ được dùng để tăng cường mô hình ngôn ngữ của AlphaProof
- Quá trình lặp này được dùng để nâng cao khả năng giải các bài toán khó hơn
- Trong quá trình chuẩn bị cho IMO, hệ thống học bằng cách chứng minh hoặc bác bỏ hàng triệu bài toán trong nhiều tuần
- Ngay trong lúc thi, một vòng lặp học cũng được áp dụng để tăng cường chứng minh trên các biến thể tự sinh của bài toán nhằm tìm lời giải hoàn chỉnh
AlphaGeometry 2: mở rộng sang các bài hình học khó hơn
- AlphaGeometry 2 là phiên bản được cải tiến đáng kể của AlphaGeometry
- Hệ thống này có cấu trúc lai neuro-symbolic kết hợp mạng nơ-ron và suy luận ký hiệu
- Mô hình ngôn ngữ dựa trên Gemini
- Hệ thống được huấn luyện lại từ đầu bằng lượng dữ liệu tổng hợp nhiều hơn một bậc so với phiên bản trước
- Nhờ dữ liệu nhiều hơn và mô hình được cải thiện, hệ thống có thể xử lý các bài hình học khó hơn có liên quan đến chuyển động của vật thể và các phương trình về góc, tỷ lệ, khoảng cách
- Bộ máy ký hiệu của AlphaGeometry 2 nhanh hơn hàng chục lần so với phiên bản trước
- Khi nhận bài mới, hệ thống tận dụng các tổ hợp cấp cao giữa những cây tìm kiếm khác nhau thông qua cơ chế chia sẻ tri thức mới để xử lý các bài toán phức tạp hơn
- Tỷ lệ giải bài hình học IMO trong 25 năm gần đây:
- Tính đến trước kỳ thi năm 2024, AlphaGeometry 2 có thể giải 83% các bài hình học IMO trong 25 năm gần đây
- Tỷ lệ giải của AlphaGeometry trước đó là 53%
- Tại IMO 2024, hệ thống đã giải Problem 4 trong vòng 19 giây sau khi nhận đầu vào đã được hình thức hóa
Suy luận ngôn ngữ tự nhiên và ứng dụng tương lai
- Trong khuôn khổ công việc liên quan đến IMO, DeepMind cũng thử nghiệm hệ thống suy luận ngôn ngữ tự nhiên dựa trên Gemini và các nghiên cứu mới nhất
- Hệ thống này không cần dịch bài toán sang ngôn ngữ hình thức và có thể kết hợp với các hệ thống AI khác
- Cách tiếp cận này cũng đã được thử nghiệm trên các bài IMO 2024 và kết quả được đánh giá là đầy hứa hẹn
- Phương pháp kỹ thuật chi tiết hơn của AlphaProof được công bố trong bài báo trên Nature
- DeepMind hướng tới một tương lai nơi các nhà toán học cùng công cụ AI khám phá giả thuyết, thử những cách tiếp cận mới cho các bài toán lâu năm và nhanh chóng hoàn thành các phần tốn nhiều thời gian của việc chứng minh
3 bình luận
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.
Ý kiến trên Hacker News
Tôi thật sự rất kỳ vọng vào công bố này, nhưng không rõ câu “trước tiên con người đã tự tay dịch bài toán sang ngôn ngữ toán học hình thức để hệ thống có thể hiểu” đang gánh bao nhiêu phần việc
Tất cả các bài không phải hình học đều có dạng “hãy tìm mọi X sao cho ...”, còn phát biểu định lý thì có dạng “chứng minh tập hợp mọi X là {foo}”
Chỉ nhìn vào các lời giải có thể tải xuống ở https://storage.googleapis.com/deepmind-media/DeepMind.com/B... thì khó biết ở bước dịch, con người đã quyết định {foo} hay máy tính tìm ra. Tôi muốn tin là máy tính đã tìm, nhưng chưa thấy căn cứ để xác nhận
{1,1}, ở P6 là2, và trong từng trường hợp cũng đưa ra cả chứng minh LeanNgay cả con người khi trực tiếp xử lý các kỹ thuật hình thức cũng thường gặp chuyện này, nên có lẽ các nhà nghiên cứu đã cho rằng cuối cùng vẫn phải kiểm toán mọi bản dịch, dù là LLM hay công cụ khác
Tuy nhiên không rõ tác nhân đã được cung cấp dạng hình thức ban đầu nào để có thể thực hiện bước này
Tức là dù AlphaProof nhận một dạng “bài toán” nào đó, và dù họ đã hình thức hóa “hãy tìm mọi X sao cho ...” như thế nào, có lẽ nó tạo ra các định lý ứng viên bằng Lean. Ví dụ có thể là tập hợp có dạng
{n: P(n)}đối với một công thức P nào đó. Sau đó nó tìm kiếm chứng minhNếu AlphaProof không tự tìm {foo} mà được cho sẵn, thì tuyên bố rằng nó đã giải bài toán sẽ khá vô lý. Dù vậy tôi vẫn rất kỳ vọng vào kết quả này
Chắc chắn là ấn tượng, nhưng khi nhắc đến IMO thì cần có lưu ý. Huy chương được trao cho 50% thí sinh, tức học sinh trung học tham gia, và tỷ lệ vàng·bạc·đồng là 1:2:3, nên những người đạt huy chương vàng và bạc nằm trong top 25% toàn bộ thí sinh
Vì vậy cách nói sẽ là “AI giải bài IMO tốt hơn 75% học sinh”, mà thật ra điều này có thể còn ấn tượng hơn
Nhưng điều kiện “một bài trong vài phút, các bài còn lại mỗi bài tối đa 3 ngày” khác với 9 giờ mà học sinh được nhận, nên khó xem là một so sánh thực sự. Nếu học sinh cũng được cho tối đa 15 ngày thay vì 9 giờ, hẳn sẽ có nhiều người đạt hoặc vượt số điểm này hơn
Trên thực tế, trong 9 giờ như học sinh, AI coi như chỉ giải được một bài, nên khả năng cao là còn rất xa nhóm có huy chương. Tôi tự hỏi có cần làm mờ một kết quả ấn tượng như vậy bằng kiểu so sánh táo với cam không
Khách quan hơn thì chỉ cần báo cáo rằng nó mất nhiều thời gian hơn nhưng đã giải được X% tổng số bài, hoặc đạt X điểm trên tổng N điểm
Ở đây thời gian không phải là trục quá thú vị. Vì con người không dùng CPU giống như một cụm GPU khổng lồ. Câu hỏi nhị phân “khi được cấp đủ tài nguyên, liệu có thể đi đến lời giải không” thú vị hơn, và câu trả lời của GPT/Claude rõ ràng là không
Họ đã rất sát ngưỡng, và thông thường chỉ cần có chút tiến triển cũng có thể được 1 điểm. Tuy nhiên, nếu truyền thông nói rằng họ giành huy chương vàng vì lý do kỹ thuật thì hẳn sẽ không hay, nên có vẻ họ hài lòng với huy chương bạc không gây tranh cãi
Điều này là thật sự đấy. AlphaGeometry đã giải một tập bài toán rất hạn chế bằng rất nhiều tìm kiếm vét cạn.
Phương pháp lần này rộng hơn nhiều, và tôi nghĩ nó sẽ tác động lớn đến cách làm toán. Nó đi từ toán học bằng ngôn ngữ tự nhiên sang toán học được hình thức hóa, rồi từ đó thực sự triển khai một pipeline tự cung cấp, nơi có thể huấn luyện cả việc hình thức hóa lẫn chứng minh.
Về nguyên tắc, pipeline này cũng có thể học cả việc xây dựng lý thuyết cơ bản như tạo định nghĩa phụ trợ và bổ đề. Nó gần với chén thánh của hỗ trợ chứng minh, và tôi nghĩ nó sẽ giúp hình thức hóa phần lớn toán học mà chúng ta tạo ra một cách tự nhiên. Con người sẽ làm việc theo kiểu nghiêm ngặt hóa sau, còn máy sẽ hỗ trợ điền các chi tiết.
Ngược lại, kiểu hình thức hóa mở như thế này là một lĩnh vực mà tiến bộ vốn rất chậm và tiệm tiến. 5 năm trước tôi làm việc trong một lĩnh vực lân cận, và có thể xem kết quả này là ở mức không thể đạt tới bằng các kỹ thuật suy luận tự động truyền thống.
Chứng minh định lý tự động thực sự hữu ích rộng hơn rất nhiều so với toán học thuần túy. Ví dụ, có thể viết ngữ nghĩa tiên đề của một ngôn ngữ lập trình nhỏ bằng Lean rồi đặt câu hỏi kiểu “hãy chứng minh rằng tồn tại một chương trình thỏa mãn đặc tả này”.
Nếu cách tiếp cận này mở rộng được, nó sẽ trở nên quan trọng hơn bất kỳ ứng dụng học máy nào xuất hiện trong vài năm qua.
Tiến hóa đã tạo ra chúng ta cũng là một quá trình tìm kiếm vận hành bằng vô số thử nghiệm vét cạn, và nghiên cứu theo phương pháp khoa học về bản chất cũng là tìm kiếm.
https://leandojo.org/
https://machine-learning-for-theorem-proving.github.io/
https://www.youtube.com/watch?v=P5ew0BrRm_I
https://paperswithcode.com/task/automated-theorem-proving
https://old.reddit.com/r/math/comments/11mb9lx/future_of_aut...
https://github.com/RiccardoBiosas/LeanGPT
Để làm việc hữu ích, không nhất thiết phải chứng minh các bài toán cực khó. Nhiều khi chỉ cần chứng minh những điều đơn giản là đủ. Khi yêu cầu mô hình ngôn ngữ hoàn thành công việc, sắp xếp mục, điều phối lịch, viết mã thực hiện X, v.v., khó có thể tin ngay kết quả; nhưng nếu hệ thống có thể dịch một phần vấn đề sang logic và tìm lời giải, nó sẽ đáng tin cậy hơn nhiều.
Điểm cốt lõi hơi bị chìm đi, nhưng họ đang dùng Lean.
Điều này quan trọng vượt ra ngoài các bài toán. Buộc mô hình học máy vật lộn với một hệ thống chứng minh là một cách tốt để tránh những lời nói nhảm thông thường.
Hy vọng trong tương lai sẽ có nhiều người viết kiểu trong Lean hoặc các hệ thống tương tự, dùng chúng như một cách tốt hơn nhiều để viết prompt.
polyriththì chỉ cần gõ tám ký tự. Tôi cũng thấy AlphaProof dùngnlinarith.Tim Gowers có một phần tổng quan ngắn rất hay, giải thích các điểm cần lưu ý chính và đặt chúng vào bối cảnh. Ông là người đoạt huy chương Fields và cũng tham gia vào công trình lần này: https://x.com/wtgowers/status/1816509803407040909
Nói vậy đúng, nhưng bản thân việc vào được đội tuyển quốc gia đã là một quá trình cực kỳ gian nan. Ở mỗi bước như olympiad toán khu vực, olympiad toán quốc gia, v.v., đều bị sàng lọc khốc liệt.
Sau đó còn có thêm huấn luyện cho nhóm tinh hoa này, và tùy trường hợp có thể có thêm tuyển chọn nữa.
Tóm lại, được chọn vào đội tuyển IMO của một quốc gia tự nó đã là chuyện lớn, còn giành huy chương vàng/bạc trong đó thì đơn giản là một thành tựu khổng lồ.
Nguồn là một người bạn từng đoạt huy chương bạc IMO.
Thật sự ghen tị với những người được trả tiền để làm việc này. Trông cực kỳ thú vị, và việc đẩy trình độ tiên tiến nhất lên theo cách như vậy hẳn sẽ rất thỏa mãn
Theo tôi, trong mức độ hài lòng với công việc, môi trường làm việc quan trọng hơn chủ đề. Dù bạn làm về một chủ đề thay đổi thế giới, nếu đội ngũ tệ thì bạn sẽ có quãng thời gian khó khăn. Có những người có tài hút cạn mọi niềm vui, và chính trị nội bộ thì ở đâu cũng có, đặc biệt càng đúng với những chủ đề thay đổi thế giới
Ngược lại, ngay cả với chủ đề trông nhàm chán nhất như đưa dữ liệu khách hàng vào cơ sở dữ liệu, nếu có một đội ngũ tử tế, kiến trúc được thiết kế tốt, thời gian để thử nghiệm và chia sẻ kiến thức, bạn vẫn có thể có khoảng thời gian tuyệt vời. Tôi ngày càng trân trọng vẻ đẹp của những thứ đơn giản nhưng hoạt động tốt. Những thứ như vậy có khi còn hiếm hơn cả đột phá khoa học
Tất nhiên, môi trường làm việc tuyệt vời và chủ đề tuyệt vời cũng có thể đi cùng nhau, và khi đó gần như trúng độc đắc, đáng để ghen tị
Lẽ ra tôi nên hào hứng và biết ơn vì được làm việc này, nhưng các công cụ thô sơ đã lấy đi khá nhiều niềm vui trong công việc
(/s)
Máy móc đã chơi cờ vua giỏi hơn con người từ vài thập kỷ nay
Nhưng chẳng ai bận tâm. Mọi người đều bận xem Magnus Carlsen
Vì là con người, chúng ta quan tâm đến những việc con người khác làm. Với máy móc, chúng ta chỉ quan tâm trong chừng mực chúng giúp ích cho mình
Nguyên tắc này cũng mở rộng khá rộng sang công việc và nghệ thuật. Chừng nào con người còn tồn tại, trong những lĩnh vực này chỗ đứng của con người sẽ luôn còn đó
Nhưng tôi rất nghi ngờ rằng trong tương lai gần còn có nhà toán học nào công bố những tiến bộ toán học mới không phải phần lớn hoặc toàn bộ do AI phát hiện. Con người có thể được ghi công chứng minh vì đã đặt ra câu hỏi ban đầu, nhưng hầu như sẽ không có một thế giới nào khăng khăng để con người giải chậm hơn và tốn kém hơn trong khi máy tính có thể dễ dàng giải các bài toán có ý nghĩa
Nguyên tắc này chắc chắn áp dụng cho nghệ thuật, nhưng với công việc thì chỉ áp dụng cho một phần hoặc phần lớn mà thôi
Khi đó không cần phải hiểu chứng minh, và cũng chẳng ai quan tâm liệu một nhà toán học nào đó ở đâu đó có hiểu hoàn toàn chứng minh ấy hay không. Việc máy móc giỏi hơn chúng ta trong việc tìm và kiểm chứng chứng minh là ổn, thậm chí còn là điều có thể dự đoán
Nhiều nhà toán học có lẽ sẽ không muốn bám vào những việc như vậy. Tuy nhiên, giữa IMO và tuyến đầu của toán học nghiên cứu vẫn còn một khoảng cách lớn
Chứng minh định lý là một trò chơi một người với không gian tìm kiếm lớn đến phi lý, nên tôi luôn nghĩ nó sẽ được giải quyết từ rất lâu trước AGI
Cá nhân tôi cho rằng những người đứng sau Lean và Mathlib là những người đóng góp lớn nhất cho AlphaProof. Vì họ đã gánh lấy công việc gian nan là hình thức hóa toàn bộ toán học
Sự thiếu hình thức hóa trong các bài báo toán học liên tục giết chết các nỗ lực tự động hóa. Bởi các nhà nghiên cứu AI phải vật lộn với những yếu tố rất con người như ký hiệu riêng của tác giả, tri thức ngầm, các bước chứng minh bị lược bỏ
Tôi cho rằng bản thân thuật ngữ AGI chưa được định nghĩa, nhưng tôi không hiểu vì sao lại dự đoán rằng việc tạo ra “một thứ thông minh nói chung”, tức trí thông minh ở mức trung vị của con người, lại khó hơn nhiều so với việc “giỏi toán hơn Terrence Tao”
Thảo luận hay nhất ở đây: https://leanprover.zulipchat.com/#narrow/stream/219941-Machi...
Bạn có thể xem cuộc thảo luận hay nhất đó tại đây: https://leanprover.zulipchat.com/#narrow/stream/219941-Machine-Learnin…