- Mô hình Gemini Deep Think của Google DeepMind đã đạt mức điểm chuẩn huy chương vàng (35 điểm) tại Olympic Toán học Quốc tế (IMO) 2025
- Mô hình này giải hoàn hảo 5 trên 6 bài toán, và được ban giám khảo chính thức của IMO công nhận có lời giải toán học rõ ràng và chính xác
- Từ mức huy chương bạc (28 điểm) của AlphaProof·AlphaGeometry 2 năm ngoái, đây là một bước nhảy vọt lớn; mô hình hiểu đề bài chính thức bằng ngôn ngữ tự nhiên và hoàn thành chứng minh như con người trong vòng 4,5 giờ
- Chế độ Deep Think áp dụng tư duy song song (parallel thinking) và học tăng cường mới nhất để đồng thời khám phá và tổng hợp nhiều lời giải, được tối ưu cho việc giải các bài toán kiểu IMO
- Google cho biết trong tương lai sẽ mở rộng hợp tác với các nhà toán học và hướng tới phát triển AGI thế hệ tiếp theo kết hợp suy luận toán học với năng lực kiểm chứng hình thức
Breakthrough Performance at IMO 2025 with Gemini Deep Think
- Gemini Deep Think của Google DeepMind đã đạt tổng 35 điểm (giải hoàn hảo 5 trên 6 bài) tại Olympic Toán học Quốc tế (IMO) 2025, qua đó chính thức đạt chuẩn huy chương vàng
- Ban giám khảo chính thức của IMO đánh giá cao độ rõ ràng, chính xác và dễ hiểu của lời giải, và Chủ tịch IMO, Prof. Dr. Gregor Dolinar, đã công bố tuyên bố chính thức rằng “xác nhận Google DeepMind đã đạt mức điểm huy chương vàng là 35 điểm”
- Năm ngoái, AlphaGeometry·AlphaProof cần chuyên gia dịch đề từ ngôn ngữ tự nhiên sang ngôn ngữ đặc thù miền (như Lean), và việc tính toán cũng mất hơn hai ngày. Năm nay, Gemini hoàn tất toàn bộ quy trình từ hiểu đề đến viết chứng minh bằng ngôn ngữ tự nhiên, trong đúng thời gian thi IMO (4,5 giờ)
Making the most of Deep Think mode
- Gemini Deep Think là chế độ suy luận nâng cao áp dụng các kỹ thuật nghiên cứu mới nhất như tư duy song song (parallel thinking), đồng thời khám phá nhiều hướng giải để tìm ra phương án tối ưu
- Mô hình được huấn luyện bằng các kỹ thuật học tăng cường để giải các bài toán toán học phức tạp cùng với nhiều dữ liệu chứng minh theo phong cách IMO, và còn được bổ sung các gợi ý, mẹo tiếp cận chung cho bài toán IMO
- Phiên bản Deep Think này dự kiến sẽ được cung cấp trước dưới dạng bản thử nghiệm cho một số nhà toán học và chuyên gia đáng tin cậy, sau đó sẽ được công bố cho người dùng đăng ký Google AI Ultra
The Future of AI and Mathematics
- Google DeepMind tiếp tục duy trì hợp tác với cộng đồng toán học, đồng thời song song nghiên cứu không chỉ suy luận dựa trên ngôn ngữ tự nhiên mà còn các hệ thống hình thức (formal) như AlphaGeometry·AlphaProof
- Trong tương lai, AI kết hợp năng lực hiểu ngôn ngữ tự nhiên với khả năng suy luận toán học hình thức, có thể kiểm chứng được kỳ vọng sẽ trở thành công cụ cốt lõi trong toán học, khoa học, kỹ thuật và nghiên cứu
- DeepMind đánh giá thành tựu lần này là một bước tiến quan trọng trên con đường hướng tới AGI (trí tuệ nhân tạo tổng quát), và có kế hoạch tiếp tục chinh phục những bài toán toán học ngày càng phức tạp và trình độ cao hơn
Xác minh câu trả lời và lập trường chính thức của IMO
- Ban tổ chức IMO đã chính thức xác nhận các câu trả lời được nộp là lời giải đầy đủ và chính xác
- Tuy vậy, IMO cũng nêu rõ rằng việc xem xét này không bao gồm xác minh hệ thống, quy trình hoặc chính mô hình nền tảng
- Có thể tham khảo thêm nội dung chi tiết và các lưu ý về diễn giải mở rộng trong tuyên bố chính thức của IMO (Xem thêm)
5 bình luận
OpenAI công bố đạt thành tích cấp huy chương vàng tại Kỳ thi Olympic Toán học Quốc tế (IMO) 2025
OpenAI đã công bố trước từ 2 ngày trước nên phần nào làm giảm hứng thú, và cũng có ý kiến cho rằng việc Alexander Wei của OpenAI lên tiếng trước mà không hề trao đổi với IMO là thiếu tế nhị.
Họ còn nói rằng vì phía IMO còn chưa chính thức công nhận mà đã công bố, nên như vậy là cướp mất lời chúc mừng và công lao vốn dành cho những người tham gia bình thường chứ không phải AI.
Nhờ vậy mà OAI chỉ là được hội đồng riêng của mình xác minh, chứ lại rơi vào tình huống thậm chí còn chưa hề được IMO chấm điểm chính thức. Hơn nữa, nhìn vào việc cũng có nhiều ý kiến cho rằng chất lượng câu trả lời của Gemini tốt hơn đôi chút... thì chẳng phải đây là một tình huống càng mất mặt hơn sao. Không phải chấp nhận rủi ro về danh tiếng, nếu thành công thì công bố, còn nếu kết quả không tốt thì rút lui (lại còn trong bối cảnh không phải chấm điểm chính thức); làm vậy có thể chấp nhận được trong benchmark, nhưng với một cuộc thi nơi các thí sinh thi đấu dưới chính tên tuổi của mình, thì dường như đó không phải là cách hành xử đúng đắn nên có.
Dù hiệu năng LLM của Google và OpenAI khá ngang ngửa, nhưng đây là lúc thấy rõ sự khác biệt về độ lão luyện của doanh nghiệp.
Ý kiến trên Hacker News
AlphaGeometry và AlphaProof trước đây đã đi theo quy trình trước hết dịch bài toán ngôn ngữ tự nhiên sang ngôn ngữ chuyên biệt theo miền như Lean, rồi lại chuyển kết quả chứng minh về ngôn ngữ tự nhiên, và việc tính toán mất 2~3 ngày; còn mô hình Gemini năm nay dùng cách tiếp cận end-to-end tạo trực tiếp chứng minh toán học từ mô tả bài toán chính thức chỉ bằng ngôn ngữ tự nhiên, nghĩa là không dịch sang Lean trước, nhưng vẫn chưa rõ nội bộ có dùng các công cụ như Lean, tìm kiếm internet, máy tính, Python hay không; OpenAI nói rằng mô hình của họ không dùng các công cụ như vậy, nhưng không rõ tuyên bố đó có áp dụng chính xác cho Gemini hay không; cũng muốn biết mức tính toán sử dụng, tức chi phí, của hai hệ thống này vào khoảng nào; nếu giá cực cao thì có nghĩa là vẫn chưa thực tiễn; do chưa có thông tin công khai nên đoán là sẽ cực kỳ đắt; và chia sẻ một liên kết xác nhận rằng "không dùng công cụ, không kết nối internet" https://x.com/FredZhang0/status/1947364744412758305
Mô hình Gemini năm nay tạo ra chứng minh toán học từ mô tả bài toán chính thức chỉ bằng ngôn ngữ tự nhiên, và toàn bộ quá trình diễn ra trong thời lượng thi 4,5 giờ, không dùng công cụ bên ngoài
Về mặt chính thức thì các công cụ kiểm chứng hình thức như Lean không được dùng khi thực sự giải các bài IMO, nhưng tôi tò mò liệu chúng có được dùng trong quá trình huấn luyện mô hình hay không; trong nghiên cứu IMO 2024 của Google có kỹ thuật chuyển chứng minh ngôn ngữ tự nhiên sang ngôn ngữ hình thức có thể kiểm chứng chính thức, và tôi nghĩ bước tiếp theo tự nhiên là dùng điều đó cho huấn luyện RLVR (xác minh-thưởng qua học tăng cường); nếu có thể dịch và kiểm chứng toàn bộ suy luận mà một toán LLM tạo ra rồi dùng làm tín hiệu thưởng, thì tín hiệu thưởng sẽ dày đặc hơn nhiều; việc có được chứng minh hình thức hoàn hảo vẫn sẽ khó, nhưng nó hữu ích để hướng mô hình tránh suy luận sai hoặc câu chữ không thể diễn giải; với lượng tính toán khổng lồ, có thể giải được cả các bài ở độ khó IMO; cách AlphaProof qua lại giữa chứng minh Lean và đầu ra của LLM để tìm kiếm không gian suy luận hiệu quả đã cho thấy có thể giải bài tầm IMO, nên tôi tự hỏi liệu có thể đạt hiệu quả và năng lực giải bài tương tự bằng cách bỏ qua bước trung gian và dạy LLM bắt chước suy luận hình thức bằng RLVR hay không
Tôi cũng tò mò tại sao lại không dùng Lean, liệu điều đó có nghĩa là dùng Lean thì dạo này việc giải bài trở nên quá dễ, hay chính Lean lại là yếu tố cản trở
Tôi cũng thắc mắc liệu "không dùng công cụ, không kết nối internet" có thực sự nghĩa là nó có thể chạy offline mà không cần hạ tầng của Google, tức có thể triển khai cục bộ khi cần hay không
Năm nay nói rằng Gemini nâng cấp đã tạo trực tiếp chứng minh toán học từ mô tả bài toán chính thức chỉ bằng ngôn ngữ tự nhiên, nhưng ngược lại tôi lại thấy tiếc vì điều đó dường như rời xa công nghệ hình thức hóa; tôi nghĩ muốn thực sự tự động hóa toán học, chẳng hạn đạt đến mức cơ học tạo ra các chứng minh dài hàng nghìn trang, thì ngoài hình thức hóa ra không còn con đường nào khác; nếu không thì vẫn cần người duyệt, và cũng không có cách nào thật sự tin cậy vào chứng minh đó
Nếu LLM có thể tạo ra chứng minh nghiêm ngặt bằng ngôn ngữ tự nhiên, thì chứng minh bằng ngôn ngữ hình thức như Lean cũng sẽ không phải khó khăn lớn; việc dùng Lean trong AlphaProof là một cách khá hạn chế và chuyên biệt cho một số bài toán toán học nhất định; ngược lại, nếu đạt được điều tương tự bằng RL và ngôn ngữ tự nhiên thì có thể mở rộng sang nhiều lĩnh vực khác nơi việc kiểm chứng khó hơn
Cũng chia sẻ rằng DeepMind hiện đang thu thập các kho lưu trữ ghi lại những bài toán chưa giải được đã được hình thức hóa một cách chính thức https://github.com/google-deepmind/formal-conjectures
Tôi là một nhà toán học nhưng không còn làm nghiên cứu nữa, và muốn cung cấp đôi chút bối cảnh về lý do nhiều nhà toán học vẫn chưa mặn mà với các kỹ thuật hình thức; trên thực tế, để tạo ra các chứng minh dài hàng nghìn trang thì rõ ràng là không thể nếu thiếu hình thức hóa, và tôi đồng ý rằng muốn "tin cậy" điều gì đó thì phải kiểm chứng hình thức; nhưng điều các nhà toán học thực sự muốn là lời giải thích về "vì sao" kết quả đó đúng; sản phẩm thực sự không phải là câu trả lời có-không, mà là cách diễn giải và lý do của nó; ví dụ, hầu như ai cũng nghĩ giả thuyết Riemann có lẽ là đúng, nhưng không phải chỉ đang ngồi chờ đáp án; thậm chí còn có rất nhiều kết quả kiểu "nếu giả thuyết Riemann đúng thì định lý mới này sẽ đúng"; điều người ta mong ở một chứng minh về bản chất là hiểu biết mới hoặc một cách đem lại cái nhìn sâu sắc hơn về lý thuyết số; nếu chỉ như Lean kiểm chứng rằng nó đúng một cách hình thức trong khi con người còn không hiểu nổi, thì điều đó gần như vô nghĩa
Hình thức hóa chính xác thường dễ hơn là giải bài toán, nên cũng có thể giải bài trước rồi sau đó hình thức hóa để kiểm tra
Các bài IMO vốn ngay từ đầu đã được thiết kế để con người giải mà không dùng công cụ; nếu để mô hình giải những bài khó hơn thì khi đó hoàn toàn có thể cung cấp đủ công cụ; ít nhất thì trước hết tái tạo được năng lực ở mức con người mà không cần công cụ vẫn là một hướng đi tốt
Khi so sánh câu trả lời của OpenAI và Gemini, tôi thấy văn phong của Gemini rõ ràng hơn nhiều; cách trình bày có thể còn tốt hơn nữa, nhưng nội dung chứng minh tự thân thì dễ theo dõi, và câu chữ cũng ngắn gọn, ngăn nắp hơn câu trả lời của OpenAI
Chứng minh của Google có thể là kết quả được tóm tắt hậu kỳ, hoặc cũng có thể phần tóm tắt là một phần của cơ chế như Tree of Thoughts; có vẻ không chỉ đơn giản là kết quả của một lệnh thụ động kiểu "hãy đưa ra đáp án cuối cùng"
Các kết quả chứng minh IMO của OpenAI và Google được nhắc đến có thể xem lần lượt tại PDF chứng minh của Google và repository ví dụ chứng minh của OpenAI
Cả OpenAI lẫn Google đều nhấn mạnh rằng "mọi quá trình đều hoàn tất trong thời gian thi 4,5 giờ", nhưng tôi nghi ngờ giới hạn đó có ý nghĩa quan trọng hay không; trên thực tế họ hoàn toàn có thể đã chạy đồng thời hàng triệu tiến trình suy luận song song để tìm ra chứng minh; tất nhiên làm vậy cũng sẽ cần rất nhiều tính toán cho mô hình đánh giá dùng để chấm kết quả và chọn ra chứng minh cuối cùng để nộp; thật ra có thể đã tốn lượng GPU tương đương hàng trăm năm; dù vậy, bản thân việc cách này tìm ra đáp án, và việc có thể song song hóa đến mức đó, vẫn rất đáng kinh ngạc; rốt cuộc dù AGI có đạt được nhờ nhiều tính toán hơn hay không thì não người không thể mở rộng dễ dàng như vậy, nên ý nghĩa của kết quả này là rõ ràng
Việc chuyển từ hệ thống chuyên biệt cho Lean năm ngoái sang LLM đa dụng dựa trên ngôn ngữ tự nhiên + RL năm nay là điều rất thú vị; tôi kỳ vọng cách tiếp cận này sẽ giúp cải thiện hiệu năng cả ở những lĩnh vực ngoài các cuộc thi toán; rất mong chờ xem nó có thể mở rộng đến đâu trong tương lai; và hệ thống lần này dường như cũng không khác biệt quá lớn với mô hình/tính năng "DeepThink" dự kiến công bố vào mùa hè
Lúc này có cảm giác như đang sống trong khoảnh khắc kiểu Deep Blue đấu Kasparov trong cuộc cạnh tranh toán học với máy; so với chỉ vài năm trước đã có tiến bộ khổng lồ, nhưng tôi vẫn nghĩ còn rất xa mới có một nhà toán học AI thực thụ; dù vậy, thật sự là đang sống trong một thời kỳ đáng kinh ngạc
Trong một podcast gần đây, Terrence Tao cũng bày tỏ sự quan tâm lớn đến việc làm việc cùng các công cụ này; ông nói rằng trong một thời gian nữa, cách tận dụng tốt nhất sẽ là con người đặt ra ý tưởng/tham số rồi để LLM song song hóa việc tìm kiếm và chứng minh; phép so sánh với công cụ cờ vua cũng phù hợp: trước đây ngay cả kỳ thủ mạnh nhất cũng có cả đội chuyên gia hỗ trợ phân tích, còn ngày nay người ta dùng siêu máy tính và phần mềm để phân tích vô số thế cờ, chọn ra ý tưởng tốt nhất rồi chuyển cho kỳ thủ
Tôi nghĩ đúng hơn là giống Deep Blue đấu với một thần đồng nhí, vì người dự IMO không phải các nhà toán học hàng đầu thế giới mà là học sinh trung học
Điểm khác biệt ở đây là chỉ brute force đơn thuần thì không thể đạt điểm cao trong thời gian giới hạn; đây là một cột mốc kỹ thuật thực sự, khác với thời Deep Blue nơi mọi thứ chỉ là 'về nguyên tắc thì có thể'
Bài số 6 khá khó hiểu, cả openai lẫn deepmind đều không đưa ra được câu trả lời; trong khi con người còn có thể nộp lời giải một phần, AI lại không có gì để nộp thì thật kỳ lạ; tôi tự hỏi có phải LLM đã tự nhận ra rằng nó thất bại trong việc giải hay không; một trong các giới hạn của LLM là "không biết rằng mình không biết", và nếu vậy thì tôi nghĩ gần như không thể kiểm tra tính nhất quán logic nếu không có solver
Có lẽ khả năng cao là trong thời gian thi giới hạn, nó chưa kịp hoàn tất phần 'suy nghĩ' nên chưa chuyển sang giai đoạn 'xuất ra'
Giới hạn này chỉ áp dụng cho kiểu sinh văn bản LLM đã pretrain ở mức cơ bản nhất; người ta còn có thể huấn luyện thêm một linear probe (một tầng mạng nơ-ron đơn giản) để nó xuất ra confidence score; tất nhiên không thể tin 100%, nhưng ít nhất nếu áp dụng trong miền hẹp như toán học thì có thể cũng khá đáng tin
Nếu không có công cụ kiểm chứng hình thức thì việc ứng dụng thực tế vẫn có thể rất rủi ro; o3 trước đây dù không còn là mới nhất nhưng vẫn mạnh ở việc tìm tài liệu tham khảo phù hợp và đề xuất các bất đẳng thức mới; nhưng ở bước chứng minh thực tế, nó có thể đưa ra câu trả lời trông thuyết phục nhưng chứa mệnh đề sai hoặc lỗi đại số trong chi tiết; mô hình càng tốt thì những lỗi tinh vi như vậy đôi khi lại càng khó phát hiện
Tôi tò mò vì sao họ lại nhấn mạnh chuyện không dùng theorem prover; rốt cuộc nếu có bất kỳ công cụ nào giúp tăng hiệu năng mô hình thì cứ dùng chẳng phải tốt hơn sao; hơn nữa Gemini cũng đã được chuyên biệt hóa theo IMO; họ đã huấn luyện mô hình bằng học tăng cường trên dữ liệu suy luận nhiều bước/giải bài/chứng minh định lý, và còn cung cấp các tuyển tập lời giải toán chất lượng cao cùng những gợi ý về cách tiếp cận bài IMO
Tôi đoán rằng "phiên bản nâng cao của Gemini Deepthink" thực ra có lẽ khác với Deepthink sẽ được đưa vào sản phẩm thuê bao Gemini Ultra khi phát hành, hoặc đã dùng nhiều compute ở giai đoạn test-time hơn rất nhiều; dù sao thì theo dõi OpenAI và Google cạnh tranh với nhau vẫn rất thú vị
Tôi sẽ chia sẻ liên kết đến prompt hệ thống context engineering đã giải hết cả 6 bài. Có thể dùng với o3 hoặc Gemini 2.5; chỉ cần nhập toàn bộ prompt rồi thêm câu hỏi và bảo nó giải bài là được. https://github.com/redcrash0721/freederia/blob/main/imo6kr.pdf