- Model Gemini Deep Think dari Google DeepMind mencapai skor standar medali emas (35 poin) di International Mathematical Olympiad (IMO) 2025
- Model ini menyelesaikan 5 dari 6 soal dengan sempurna, dan diakui oleh dewan juri resmi IMO atas solusi matematis yang jelas dan presisi
- Ini merupakan lompatan besar dari level medali perak tahun lalu (28 poin) yang dicapai AlphaProof·AlphaGeometry 2; model ini memahami soal resmi dalam bahasa alami dan menyelesaikan pembuktian seperti manusia dalam 4,5 jam
- Mode Deep Think menerapkan parallel thinking dan reinforcement learning terbaru untuk mengeksplorasi dan menggabungkan beberapa solusi secara bersamaan, dioptimalkan untuk pemecahan soal bergaya IMO
- Ke depan, Google berencana memperluas kolaborasi dengan matematikawan dan melangkah menuju pengembangan AGI generasi berikutnya yang menggabungkan penalaran matematis dan kemampuan verifikasi formal
Breakthrough Performance at IMO 2025 with Gemini Deep Think
- Gemini Deep Think dari Google DeepMind menerima total 35 poin (menyelesaikan sempurna 5 dari 6 soal) di International Mathematical Olympiad (IMO) 2025, sehingga secara resmi mencapai standar medali emas
- Dewan juri resmi IMO memberikan penilaian tinggi pada kejelasan, presisi, dan solusi yang mudah dipahami, dan Ketua IMO Prof. Dr. Gregor Dolinar merilis pernyataan resmi bahwa "Google DeepMind dipastikan telah mencapai skor medali emas 35 poin"
- Tahun lalu, AlphaGeometry·AlphaProof mengharuskan para ahli menerjemahkan soal dari bahasa alami ke bahasa khusus domain (seperti Lean), dan komputasinya juga memakan waktu lebih dari dua hari. Tahun ini, Gemini menyelesaikan seluruh proses dari pemahaman soal hingga penulisan pembuktian berbasis bahasa alami, dalam batas waktu kompetisi IMO (4,5 jam)
Making the most of Deep Think mode
- Gemini Deep Think adalah mode penalaran yang ditingkatkan yang menerapkan teknik riset terbaru seperti parallel thinking, mengeksplorasi beberapa jalur penyelesaian secara bersamaan untuk menghasilkan solusi optimal
- Model ini dilatih dengan teknik reinforcement learning untuk menyelesaikan masalah matematika yang kompleks serta beragam data pembuktian bergaya IMO, dan juga diberi masukan tambahan berupa petunjuk dan tips umum tentang pendekatan terhadap soal IMO
- Model Deep Think ini rencananya akan lebih dulu diberikan dalam versi uji kepada sejumlah matematikawan dan pakar tepercaya, lalu nantinya dibuka untuk pelanggan Google AI Ultra
The Future of AI and Mathematics
- Google DeepMind terus melanjutkan kolaborasi dengan komunitas matematika, sembari juga menjalankan riset berbasis sistem formal seperti AlphaGeometry·AlphaProof selain penalaran berbasis bahasa alami
- Ke depan, AI yang menggabungkan pemahaman bahasa alami dan kemampuan penalaran matematis yang formal serta dapat diverifikasi diperkirakan akan menjadi alat inti di bidang matematika, sains, teknik, dan riset
- DeepMind menilai pencapaian ini sebagai kemajuan penting di jalur menuju AGI (kecerdasan umum buatan), dan berencana menantang penyelesaian masalah matematika yang lebih kompleks dan lebih tingkat tinggi di masa mendatang
Verifikasi jawaban dan posisi resmi IMO
- Panitia penyelenggara IMO secara resmi mengonfirmasi bahwa jawaban yang diajukan merupakan solusi yang lengkap dan akurat
- Namun, IMO juga menegaskan bahwa peninjauan mereka tidak mencakup verifikasi sistem, proses, atau model dasar itu sendiri
- Untuk rincian lebih lanjut dan penafsiran yang lebih luas, lihat pernyataan resmi IMO (Lihat selengkapnya)
5 komentar
OpenAI mengumumkan pencapaian setara medali emas di Olimpiade Matematika Internasional (IMO) 2025
Karena OpenAI sudah lebih dulu mengumumkannya 2 hari lalu, rasanya jadi agak hambar, tetapi ada juga yang mengatakan bahwa Alexander Wei dari OpenAI berbicara lebih dulu tanpa diskusi dengan IMO adalah tindakan yang kurang beretika.
Karena pihak IMO bahkan belum mengakuinya secara resmi, pengumuman itu dianggap telah merampas ucapan selamat dan penghargaan yang seharusnya diberikan kepada peserta manusia biasa, bukan AI.
Jadi, berkat itu OAI hanya diverifikasi oleh panel internalnya sendiri, dan jadinya berada dalam situasi tidak menerima penilaian resmi dari IMO. Ditambah lagi, kalau melihat banyak pendapat yang menilai kualitas jawaban Gemini sedikit lebih baik... rasanya ini malah jadi situasi yang lebih memalukan, bukan? Mereka tidak menanggung risiko terhadap reputasi, lalu jika berhasil diumumkan hasilnya (bahkan dalam kondisi bukan penilaian resmi), dan jika hasilnya buruk mereka tinggal menarik diri. Mungkin itu masih bisa dilakukan dalam benchmark, tetapi menurut saya itu bukan sikap yang tepat untuk ditunjukkan dalam kompetisi tempat para peserta bertanding dengan membawa nama mereka sendiri.
Meski performa LLM Google dan OpenAI nyaris setara, perbedaan kematangan perusahaan mereka terlihat di sini.
Pendapat Hacker News
AlphaGeometry dan AlphaProof terlebih dahulu menerjemahkan soal bahasa alami ke bahasa khusus domain seperti Lean, lalu mengubah hasil pembuktiannya kembali ke bahasa alami, dan komputasinya memakan waktu 2–3 hari. Model Gemini tahun ini menggunakan pendekatan end-to-end yang langsung menghasilkan pembuktian matematis dari deskripsi soal resmi hanya dengan bahasa alami, artinya tidak diterjemahkan dulu ke Lean. Namun, masih belum jelas apakah secara internal ia menggunakan alat seperti Lean, pencarian internet, kalkulator, Python, dan sebagainya. OpenAI mengatakan model mereka tidak menggunakan alat semacam itu, tetapi saya tidak yakin apakah klaim itu juga berlaku persis untuk Gemini. Saya juga ingin tahu kisaran kasar jumlah komputasi yang dipakai masing-masing sistem, yaitu biayanya. Jika biayanya sangat besar, itu berarti masih belum terlalu praktis. Karena belum ada informasi yang dipublikasikan, saya menduga biayanya sangat mahal. Lalu dibagikan juga tautan yang mengonfirmasi "tanpa penggunaan alat, tanpa koneksi internet" https://x.com/FredZhang0/status/1947364744412758305
Model Gemini tahun ini menghasilkan pembuktian matematis dari deskripsi soal resmi hanya dengan bahasa alami, dan seluruh proses berlangsung dalam waktu lomba 4,5 jam. Tidak menggunakan alat eksternal.
Secara resmi, alat verifikasi formal seperti Lean memang tidak dipakai saat benar-benar menyelesaikan soal IMO, tetapi saya penasaran apakah alat itu digunakan dalam proses pelatihan model. Dalam riset IMO Google tahun 2024 ada teknik untuk mengubah pembuktian bahasa alami menjadi bahasa formal yang dapat diverifikasi. Menurut saya, langkah alami berikutnya adalah memanfaatkannya dalam pelatihan RLVR (verification-reward melalui reinforcement learning). Jika semua penalaran yang dihasilkan math LLM bisa diterjemahkan dan diverifikasi lalu dipakai sebagai sinyal reward, sinyal reward akan jauh lebih rapat. Mendapatkan bukti formal yang sempurna mungkin masih sulit, tetapi ini berguna untuk mendorong model agar menghindari penalaran yang salah atau kalimat yang tidak bisa diuraikan. Dengan komputasi yang sangat besar, soal setingkat IMO pun bisa diselesaikan. Seperti AlphaProof, sudah ditunjukkan bahwa dengan bolak-balik antara bukti Lean dan keluaran LLM, ruang penalaran dapat dijelajahi secara efisien hingga soal level IMO bisa dipecahkan. Saya bertanya-tanya apakah dengan melewati langkah perantara itu dan mengajarkan LLM meniru penalaran formal lewat RLVR, kita bisa mendapatkan efisiensi dan kemampuan pemecahan masalah yang serupa.
Saya juga penasaran kenapa mereka tidak memakai Lean. Apakah itu berarti memakai Lean sekarang justru membuat penyelesaian soal terlalu mudah, atau Lean sendiri malah menjadi hambatan?
Saya juga penasaran apakah "tanpa penggunaan alat, tanpa koneksi internet" berarti sistem itu benar-benar bisa berjalan offline tanpa infrastruktur Google, sehingga mungkin bisa dideploy secara lokal bila diperlukan.
Tahun ini memang dikatakan bahwa model Gemini yang lebih canggih langsung menghasilkan pembuktian matematis dari deskripsi soal resmi hanya dalam bahasa alami, tetapi justru saya merasa agak disayangkan bahwa arahnya menjauh dari teknik formalisasi. Menurut saya, jika kita benar-benar ingin mengotomatisasi matematika, atau misalnya mencapai tingkat di mana pembuktian ribuan halaman bisa dihasilkan secara mekanis, tidak ada jalan lain selain formalisasi. Kalau tidak, peninjau manusia tetap dibutuhkan, dan tidak ada cara untuk benar-benar memercayai pembuktian itu.
Jika LLM bisa membuat bukti yang ketat dalam bahasa alami, maka membuktikannya dalam bahasa formal seperti Lean juga seharusnya bukan kesulitan besar. Penggunaan Lean dalam AlphaProof cukup terbatas dan khusus untuk jenis masalah matematika tertentu. Sebaliknya, jika pendekatan RL dan bahasa alami bisa mencapai hal yang sama, itu bisa diperluas ke berbagai bidang yang verifikasinya lebih sulit.
Dibagikan juga fakta bahwa DeepMind saat ini sedang mengumpulkan repositori yang mencatat masalah-masalah formal yang belum terpecahkan https://github.com/google-deepmind/formal-conjectures
Saya seorang matematikawan, tetapi sudah tidak lagi meneliti, dan saya ingin memberi sedikit konteks mengapa banyak matematikawan bersikap setengah hati terhadap teknik formal. Secara realistis, untuk membuat pembuktian ribuan halaman memang mustahil tanpa formalisasi, dan saya setuju bahwa kalau ingin benar-benar "memercayai" sesuatu, itu harus diverifikasi secara formal. Tetapi yang benar-benar diinginkan matematikawan dalam praktiknya adalah penjelasan tentang "mengapa" hasil itu benar. Produk yang sesungguhnya bukan jawaban ya-atau-tidak, melainkan interpretasi dan alasannya. Misalnya, semua orang merasa Hipotesis Riemann mungkin benar, tetapi bukan berarti mereka hanya menunggu jawaban akhir. Bahkan banyak hasil yang berbentuk "jika Hipotesis Riemann benar maka teorema baru ini berlaku". Yang diharapkan dari sebuah pembuktian pada dasarnya adalah wawasan baru yang mendalam, atau cara yang memberi pemahaman lebih dalam tentang teori bilangan. Jika sesuatu seperti Lean hanya memverifikasi bahwa itu benar secara formal tetapi manusia bahkan tidak bisa memahaminya, maka nilainya hampir tidak ada.
Formalisasi yang tepat cenderung lebih mudah daripada memecahkan masalahnya, jadi masalahnya bisa diselesaikan dulu lalu diformalisasi dan diverifikasi setelahnya.
Soal IMO sejak awal memang dirancang agar manusia bisa menyelesaikannya tanpa alat. Jika nantinya model diminta memecahkan soal yang lebih sulit, saat itu tentu alat bisa diberikan. Setidaknya, mereproduksi kemampuan setingkat manusia tanpa alat terlebih dahulu menurut saya adalah arah yang baik.
Jika membandingkan jawaban OpenAI dan Gemini, gaya penulisan Gemini terasa jauh lebih jelas. Penyajiannya masih bisa dibuat sedikit lebih baik, tetapi isi pembuktiannya sendiri mudah diikuti, dan kalimat-kalimatnya lebih singkat serta lebih rapi daripada jawaban OpenAI.
Pembuktian Google mungkin merupakan hasil yang diringkas setelah fakta, dan ada kemungkinan bagian dari mekanisme seperti Tree of Thoughts juga mencakup proses peringkasan. Sepertinya ini bukan sekadar hasil dari perintah sederhana dan pasif seperti "berikan jawaban akhir".
Hasil pembuktian IMO dari OpenAI dan Google yang disebutkan bisa dilihat masing-masing di Google proof PDF dan contoh pembuktian OpenAI Repository
Baik OpenAI maupun Google menekankan bahwa "seluruh proses selesai dalam waktu lomba 4,5 jam", tetapi saya ragu batasan ini punya makna yang penting. Pada praktiknya, mereka mungkin saja menjalankan jutaan proses penalaran paralel sekaligus untuk mencari pembuktian. Tentu saja, untuk ini juga dibutuhkan banyak komputasi pada model evaluator yang menilai hasil dan memilih pembuktian final yang akan dikirimkan. Bisa jadi sebenarnya dibutuhkan waktu GPU setara ratusan tahun. Meski begitu, tetap mengejutkan bahwa pendekatan seperti ini bisa menemukan solusi, dan bahwa paralelisasi bisa dilakukan sampai sejauh itu. Terlepas apakah AGI akan dicapai dengan komputasi yang lebih besar atau tidak, otak manusia tidak bisa diskalakan semudah itu, jadi makna dari hasil ini tetap jelas.
Sangat menarik bahwa pendekatannya beralih dari sistem khusus Lean tahun lalu ke LLM umum berbasis bahasa alami + RL. Saya memperkirakan pendekatan ini akan membantu peningkatan performa juga di luar bidang kompetisi matematika. Menarik untuk melihat sejauh mana ini bisa meluas ke depan. Dan tampaknya sistem kali ini juga tidak terlalu berbeda dengan model/fitur "DeepThink" yang dijadwalkan rilis pada musim panas.
Saat ini rasanya seperti sedang mengalami momen era Deep Blue vs Kasparov dalam kompetisi matematika melawan mesin. Kemajuannya luar biasa dibanding hanya beberapa tahun lalu, tetapi menurut saya masih sangat jauh dari AI matematikawan yang sesungguhnya. Tetap saja, kita hidup di masa yang benar-benar menakjubkan.
Dalam podcast terbaru, Terrence Tao juga menunjukkan minat besar untuk bekerja bersama alat-alat seperti ini. Ia menyebut bahwa untuk sementara waktu, cara pemanfaatan terbaik kemungkinan adalah manusia menetapkan ide/parameter lalu LLM melakukan eksplorasi dan pembuktian secara paralel. Analogi mesin catur juga tepat. Dulu para pemain catur terbaik dibantu tim pakar besar untuk analisis, tetapi sekarang superkomputer dan perangkat lunak menganalisis sangat banyak posisi, lalu ide terbaik dipilih dan disampaikan kepada pemain.
Menurut saya ini lebih mirip Deep Blue melawan anak ajaib daripada melawan jenius, karena peserta IMO bukan matematikawan kelas dunia, melainkan siswa SMA.
Perbedaannya di sini adalah bahwa skor tinggi tidak bisa didapat dalam batas waktu hanya dengan brute force sederhana. Ini benar-benar tonggak teknis, dan berbeda dari situasi Deep Blue yang "secara prinsip memungkinkan".
Soal nomor 6 terasa janggal. Baik openai maupun deepmind tidak bisa memberikan jawaban. Manusia setidaknya bisa memberi solusi parsial, jadi aneh kalau AI malah tidak menghasilkan jawaban sama sekali. Saya jadi bertanya-tanya apakah LLM menyadari sendiri bahwa ia gagal menyelesaikannya. Salah satu keterbatasan LLM adalah tidak tahu bahwa dirinya tidak tahu, dan kalau begitu saya rasa hampir mustahil memeriksa konsistensi logis tanpa solver.
Kemungkinan besar sistem itu belum selesai "berpikir" dalam batas waktu lomba dan tidak sempat masuk ke tahap "mengeluarkan" jawaban.
Keterbatasan ini hanya berlaku untuk generasi teks LLM pre-trained paling dasar. Kita juga bisa melatih linear probe tambahan (lapisan jaringan saraf sederhana) agar mengeluarkan confidence score. Tentu ini tidak bisa dipercaya 100%, tetapi setidaknya jika diterapkan pada domain terbatas seperti matematika, mungkin cukup bisa diandalkan.
Tanpa alat verifikasi formal, risikonya mungkin masih terlalu besar untuk penggunaan nyata. o3 lama juga, meski bukan yang terbaru, cukup kuat dalam menemukan referensi dan mengusulkan ketaksamaan baru. Namun, pada tahap pembuktian nyata, ia bisa menghasilkan jawaban yang tampak meyakinkan tetapi memuat proposisi yang salah di detailnya atau kesalahan aljabar. Semakin baik modelnya, justru kesalahan halus seperti ini bisa makin sulit ditemukan.
Saya penasaran mengapa mereka menekankan bahwa mereka tidak menggunakan theorem prover. Bukankah sebaiknya alat apa pun yang bisa meningkatkan performa model dipakai saja? Lagi pula, Gemini juga telah disesuaikan secara khusus untuk IMO. Model itu dilatih lewat reinforcement learning pada data penalaran multi-langkah/pemecahan masalah/pembuktian teorema, dan juga diberi kumpulan penjelasan soal matematika berkualitas tinggi serta petunjuk tentang pendekatan soal IMO.
Saya menduga "versi lanjutan dari Gemini Deepthink" sebenarnya berbeda dari Deepthink yang akan masuk ke produk langganan Gemini Ultra saat dirilis, atau setidaknya menggunakan komputasi fase pengujian yang jauh lebih besar. Meski begitu, tetap menyenangkan melihat OpenAI dan Google saling bersaing.
Saya akan membagikan tautan system prompt rekayasa konteks yang menyelesaikan semua soal nomor 1-6; bisa dipakai dengan o3 atau Gemini 2.5, cukup masukkan semua prompt lalu ajukan pertanyaannya dan minta agar soalnya diselesaikan https://github.com/redcrash0721/freederia/blob/main/imo6kr.pdf