- Google DeepMind'in Gemini Deep Think modeli, 2025 Uluslararası Matematik Olimpiyatı'nda (IMO) altın madalya barajı olan 35 puana ulaştı
- Model, 6 sorunun 5'ini eksiksiz çözdü ve IMO resmi jüri değerlendirmesinde açık ve son derece hassas matematiksel çözümlemeler sunduğu kabul edildi
- Geçen yıl AlphaProof ve AlphaGeometry 2'nin gümüş madalya düzeyi olan 28 puanından büyük bir sıçrama yaparak, resmi problemleri doğal dille anlayıp 4,5 saat içinde insanlar gibi ispat tamamladı
- Deep Think modu, paralel düşünme (parallel thinking) ve en yeni pekiştirmeli öğrenme tekniklerini kullanarak birden fazla çözüm yolunu aynı anda araştırıp birleştiriyor; böylece IMO tarzı problem çözümüne optimize ediliyor
- Google, bundan sonra matematikçilerle iş birliğini genişletmeyi ve matematiksel akıl yürütme ile resmi doğrulama yeteneklerini birleştiren yeni nesil AGI geliştirmeye ilerlemeyi planlıyor
Gemini Deep Think ile IMO 2025'te çığır açan performans
- Google DeepMind'in Gemini Deep Think modeli, 2025 Uluslararası Matematik Olimpiyatı'nda (IMO) toplam 35 puan aldı (6 sorunun 5'ini eksiksiz çözerek) ve böylece altın madalya barajını resmi olarak geçti
- IMO resmi jüri heyeti, açıklık, hassasiyet ve anlaşılması kolay çözüm anlatımını yüksek değerlendirdi. IMO Başkanı Prof. Dr. Gregor Dolinar da "Google DeepMind'in 35 puanlık altın madalya skoruna ulaştığını teyit ediyorum" şeklinde resmi bir açıklama yaptı
- Geçen yıl AlphaGeometry ve AlphaProof için uzmanların problemleri doğal dilden alan uzmanlığına özgü dillere (Lean vb.) çevirmesi gerekiyordu ve hesaplama iki günden uzun sürüyordu. Bu yıl Gemini ise problem anlama aşamasından ispat yazımına kadar tüm süreci doğal dil tabanlı olarak ve IMO yarışma süresi olan 4,5 saat içinde tamamladı
Deep Think modundan en iyi şekilde yararlanmak
- Gemini Deep Think, paralel düşünme (parallel thinking) gibi en yeni araştırma tekniklerini uygulayan geliştirilmiş bir akıl yürütme modu; birden fazla çözüm yolunu aynı anda araştırarak en iyi sonuca ulaşıyor
- Model, karmaşık matematik problemlerini çözmek için pekiştirmeli öğrenme teknikleri ve çeşitli IMO tarzı ispat verileriyle eğitildi; ayrıca IMO problemlerine yaklaşım konusunda genel ipuçları ve tavsiyeler de eklendi
- Bu Deep Think modeli, güvenilir bazı matematikçilere ve uzmanlara önce test sürümü olarak sunulacak; ileride ise Google AI Ultra abonelerine açılması planlanıyor
Yapay zeka ve matematiğin geleceği
- Google DeepMind, matematik topluluğuyla iş birliğini sürdürürken, yalnızca doğal dil tabanlı akıl yürütme değil, AlphaGeometry ve AlphaProof gibi resmi (formal) sistemlere dayalı araştırmaları da paralel biçimde yürütüyor
- Gelecekte doğal dil anlama becerisi ile resmi ve doğrulanabilir matematiksel akıl yürütme yeteneğini birleştiren yapay zekanın; matematik, bilim, mühendislik ve araştırma alanlarında temel bir araç haline gelmesi bekleniyor
- DeepMind, bu başarıyı AGI'ye (genel yapay zeka) giden yolda önemli bir ilerleme olarak değerlendiriyor ve gelecekte daha karmaşık, daha ileri düzey matematik problemlerini çözmeyi hedefliyor
Yanıt doğrulaması ve IMO'nun resmi tutumu
- IMO organizasyon komitesi, sunulan yanıtların eksiksiz ve doğru çözümler olduğunu resmi olarak doğruladı
- Ancak IMO'nun incelemesinin, sistemin, sürecin veya temel modelin kendisinin doğrulanmasını kapsamadığı özellikle belirtildi
- Ayrıntılar ve kapsamlı açıklama için IMO'nun resmi bildirisini inceleyebilirsiniz: Daha fazla bilgi
5 yorum
OpenAI, 2025 Uluslararası Matematik Olimpiyatı'nda (IMO) altın madalya düzeyinde başarı elde ettiğini duyurdu
OpenAI bunu 2 gün önce önce duyurduğu için heyecanı biraz kaçmıştı; ayrıca OpenAI'dan Alexander Wei'nin IMO ile hiçbir görüşme yapmadan bunu önce açıklamasının nezaketsizce olduğu yönünde yorumlar da vardı.
Resmî olarak IMO tarafı tarafından da henüz tanınmadan duyurulduğu için, bunun yapay zekanın değil normal katılımcıların kutlamalarını ve emeklerini gölgede bıraktığı söyleniyor.
Bu sayede OAI, bunu kendi panelinin doğruladığı bir şey haline getirmiş oldu; yani IMO’nun resmî değerlendirmesini bile almamış bir durum ortaya çıktı. Üstelik yanıtların kalitesinin de Gemini’de biraz daha iyi olduğuna dair görüşlerin çok olması düşünülürse... bu, daha da kötü bir görüntü yaratmıyor mu diye düşünüyorum. İtibar açısından risk almıyor, başarılı olursa duyuru yapıyor (üstelik bu da resmî puanlama olmayan bir durumda), sonuç kötü olursa geri çekiliyorsa, bunun benchmark’larda yapılması kabul edilebilir olsa da, katılımcıların kendi adlarını ortaya koyarak yarıştığı bir turnuvada sergilenecek doğru tutum gibi görünmüyor.
Google ile OpenAI arasında LLM performansı başa baş olsa da, kurumsal tecrübe farkı işte burada ortaya çıkıyor.
Hacker News görüşleri
AlphaGeometry ve AlphaProof önce doğal dil problemlerini Lean gibi alana özgü dillere çevirip sonra kanıt sonuçlarını yeniden doğal dile dönüştürüyordu ve hesaplama 2-3 gün sürüyordu; bu yılki Gemini modeli ise resmi problem açıklamasından yalnızca doğal dil kullanarak matematiksel kanıtları doğrudan üreten uçtan uca bir yaklaşım kullandı, yani önce Lean'a çevirmedi; ancak içeride Lean, internet araması, hesap makinesi, Python gibi araçları kullanıp kullanmadığı net değil; OpenAI kendi modelinde bu tür araçların kullanılmadığını söyledi ama bunun Gemini için de tam olarak geçerli olup olmadığını bilmiyorum; ayrıca iki sistemin kullandığı hesaplama miktarının, yani maliyetin, kabaca ne düzeyde olduğunu da merak ediyorum; eğer fiyat çok yüksekse bu henüz pratik olmadığı anlamına gelir; henüz açık bilgi yok, bu yüzden çok pahalı olduğunu tahmin ediyorum; ayrıca "araç kullanımı yok, internet bağlantısı yok" ifadesinin doğrulandığını söyleyen bir bağlantı da paylaşılıyor https://x.com/FredZhang0/status/1947364744412758305
Bu yılki Gemini modeli, resmi problem açıklamasından yalnızca doğal dil kullanarak matematiksel kanıtlar üretiyor ve tüm süreç 4,5 saatlik yarışma süresi içinde tamamlanıyor; dış araç kullanılmadı
Resmi olarak Lean gibi biçimsel doğrulama araçlarının IMO problemlerini gerçekten çözerken kullanılmadığı söyleniyor ama modelin eğitim sürecinde kullanılıp kullanılmadığını merak ediyorum; Google'ın 2024 IMO araştırmasında doğal dil kanıtlarını biçimsel olarak doğrulanabilir bir dile dönüştürme tekniği var; bunun RLVR (pekiştirmeli öğrenme ile doğrulama-ödül) eğitiminde kullanılmasının doğal bir sonraki adım olduğunu düşünüyorum; matematik LLM'lerinin ürettiği tüm akıl yürütmeleri çevirip doğrulayarak ödül sinyali olarak kullanabilirseniz ödül sinyali çok daha sık olur; kusursuz biçimsel kanıt elde etmek hâlâ zor olurdu ama yanlış akıl yürütmelerden ya da çözülemeyen cümlelerden kaçınmayı öğretmekte işe yarardı; muazzam hesaplama ile birlikte bu, IMO zorluğundaki problemleri çözmeyi mümkün kılabilir; AlphaProof gibi Lean kanıtı ile LLM çıktısı arasında gidip gelerek çıkarım uzayını verimli biçimde aramak, IMO düzeyindeki problemlerin çözülebileceğini zaten gösterdi; ara adımı atlayıp RLVR ile LLM'e biçimsel akıl yürütmeyi taklit etmeyi öğretirsek benzer verimlilik ve problem çözme yeteneği elde edilemez mi diye düşünüyorum
Neden Lean kullanılmadığını da merak ediyorum; Lean kullanıldığında artık problem çözmenin fazla kolaylaştığı mı kastediliyor, yoksa Lean'ın kendisi mi engelleyici bir unsur?
"Araç kullanımı yok, internet bağlantısı yok" ifadesinin gerçekten Google altyapısı olmadan çevrimdışı da çalışabileceği anlamına gelip gelmediğini, yani gerekirse yerelde dağıtılıp dağıtılamayacağını merak ediyorum
Bu yıl gelişmiş Gemini modelinin resmi problem açıklamasından yalnızca doğal dille doğrudan matematiksel kanıt ürettiği söyleniyor ama ben tersine, biçimselleştirme tekniklerinden uzaklaşılmasını biraz üzücü buluyorum; matematiği gerçekten otomatikleştirmek ya da örneğin binlerce sayfalık kanıtları makineyle üretmek istiyorsak biçimselleştirme dışında bir yol olduğunu sanmıyorum; aksi hâlde yine insan denetleyici gerekir ve kanıta gerçekten güvenmenin bir yolu kalmaz
Eğer LLM doğal dille sıkı kanıtlar üretebiliyorsa, Lean gibi biçimsel bir dilde kanıt üretmesi de büyük bir zorluk olmamalı; AlphaProof'ta Lean kullanımı oldukça sınırlıydı ve belirli matematik problemlerine özeldi; buna karşılık RL yaklaşımı ve doğal dille aynı şeyi başarırsanız doğrulaması zor pek çok alana da genişleyebilir
DeepMind'ın şu anda resmi olarak çözülmemiş problemleri biçimselleştirip kaydeden depolar topladığını da paylaşıyor https://github.com/google-deepmind/formal-conjectures
Ben bir matematikçiyim ama artık araştırma yapmıyorum; birçok matematikçinin neden biçimsel yöntemlere mesafeli durduğuna dair biraz bağlam vermek istiyorum; pratikte binlerce sayfalık bir kanıt üretmek istiyorsanız elbette biçimselleştirme olmadan bu mümkün değil ve bir şeye "güvenmek" için onun biçimsel olarak doğrulanması gerektiğine katılıyorum; ama matematikçilerin gerçekten istediği şey, o sonucun neden doğru olduğuna dair açıklamadır; asıl ürün evet-hayır cevabı değil, onun yorumu ve gerekçesidir; örneğin Riemann hipotezinin muhtemelen doğru olduğunu herkes düşünür ama sadece doğru cevabı beklemiyoruz; hatta "eğer Riemann hipotezi doğruysa şu yeni teorem geçerlidir" türünde çok sayıda sonuç da var; bir kanıttan beklenen şey temelde yeni bir içgörü ya da sayı teorisine dair derin bir anlayış kazandırmasıdır; Lean gibi yalnızca biçimsel olarak doğru olduğunu doğrulayıp insanın anlayamadığı bir şey sunuyorsa bunun neredeyse hiç anlamı yoktur
Doğru biçimselleştirme, problemi çözmekten daha kolay olma eğilimindedir; bu yüzden önce problemi çözüp sonra biçimselleştirerek doğrulamak da mümkündür
IMO problemleri zaten insanların araç kullanmadan çözmesi için tasarlanmış problemlerdir; modele daha zor problemler çözdürecekseniz o zaman yeterli araçları da verebilirsiniz; en azından önce insan düzeyindeki yeteneği araçsız olarak yeniden üretmek iyi bir yön gibi görünüyor
OpenAI ve Gemini yanıtlarını karşılaştırınca, Gemini tarafının yazım tarzı çok daha açık görünüyor; sunum biraz daha iyi olabilirdi ama kanıtın kendisini takip etmek kolay ve OpenAI yanıtına göre daha kısa, daha derli toplu cümlelerden oluşuyor
Google'ın kanıtı muhtemelen sonradan özetlenmiş bir sonuç da olabilir ve Tree of Thoughts benzeri bir mekanizmanın bir parçası olarak özetlenmiş olması da mümkün; basitçe ve pasif biçimde "nihai cevabı ver" komutunun çıktısı gibi görünmüyor
Bahsedilen OpenAI ve Google IMO kanıt sonuçları sırasıyla Google kanıt PDF'i ve OpenAI'nin kanıt örnekleri deposu üzerinden görülebilir
"Tüm süreci 4,5 saatlik yarışma içinde tamamladık" noktasını hem OpenAI hem Google vurguladı ama bu sınırın gerçekten önemli olup olmadığından emin değilim; pratikte yüz binlerce ya da milyonlarca paralel akıl yürütme sürecini aynı anda çalıştırarak kanıt aramış olabilirlerdi; tabii bunun için sonuçları değerlendirecek ve sonunda hangi kanıtın gönderileceğini seçecek bir değerlendirme modeline de çok fazla hesaplama gerekir; gerçekte yüzlerce yıllık GPU zamanı harcanmış olabilir; yine de böyle bir yaklaşımın çözüm bulabiliyor olması ve paralelleştirmenin bu kadar ilerleyebilmesi başlı başına etkileyici; sonuçta AGI'ya daha fazla hesaplama ile ulaşsınlar ya da ulaşmasınlar, insan beyni bu kadar kolay ölçeklenemediği için bunun anlamı açık
Geçen yılın Lean odaklı sisteminden, doğal dile dayalı genel amaçlı LLM + RL yaklaşımına geçilmiş olması çok ilginç; bu yaklaşımın matematik yarışmaları dışındaki alanlarda da performans artışı sağlayacağını düşünüyorum; nereye kadar ölçeklenebileceğini görmek heyecan verici ve bu sistemin yazın çıkması beklenen "DeepThink" model/özelliğinden de çok farklı görünmediği hissi var
Şu an sanki makinelerle matematik yarışında Deep Blue ve Kasparov dönemindeki ana tanıklık ediyoruz; sadece birkaç yıl öncesine göre muazzam ilerleme var ama bunun hâlâ gerçek bir AI matematikçiden çok uzak olduğunu düşünüyorum; yine de olağanüstü zamanlarda yaşıyoruz
Terrence Tao da yakın tarihli bir podcast'te bu tür araçlarla çalışma konusunda büyük ilgi gösterdi; ona göre yakın vadede en iyi kullanım biçimi, insanın fikirleri/parametreleri belirlemesi ve LLM'in arama ile kanıt gibi şeyleri paralel biçimde denemesi olacak; satranç motoru benzetmesi de yerinde; en iyi satranç oyuncuları bile eskiden çok sayıda uzmandan oluşan ekiplerle analiz yapıyordu ama bugün süper bilgisayarlar ve yazılımlar sayısız konumu analiz edip en iyi fikirleri seçerek oyuncuya iletiyor
Bunun Deep Blue ile bir dahi çocuğun karşılaşmasına daha çok benzediğini düşünüyorum; IMO katılımcıları dünya çapında matematikçiler değil, lise öğrencileri
Buradaki fark, sadece kaba kuvvetle zaman sınırı içinde yüksek puan almanın mümkün olmaması; bu gerçek bir teknik dönüm noktası ve Deep Blue dönemindeki "ilke olarak mümkün" durumundan farklı
Muhtemelen yarışma süresi içinde "düşünme" kısmını bitiremediler ve "çıktı" aşamasına geçemediler
Bu sınırlama yalnızca en temel ön eğitimli LLM metin üretimi için geçerli; ek olarak linear probe (basit bir sinir ağı katmanı) eğitilerek confidence score ürettirilebilir; elbette %100 güvenilir olmaz ama en azından matematik gibi sınırlı alanlarda oldukça işe yarayabilir
Biçimsel doğrulama aracı olmadan gerçek kullanım için hâlâ fazla riskli olabilir; eski o3 de artık en yeni model değil ama kaynak bulma ve yeni eşitsizlikler önerme konusunda iyiydi; buna rağmen gerçek kanıt aşamasında ikna edici görünen ama ayrıntılarda yanlış önermeler ya da cebirsel hatalar içeren yanıtlar verebiliyordu; model geliştikçe bu tür ince hataları yakalamak daha da zorlaşabilir
Neden teorem ispatlayıcı kullanmadıklarını özellikle vurguladıklarını merak ediyorum; sonuçta model performansını artıran herhangi bir aracı kullanmak iyi değil mi; ayrıca Gemini de IMO'ya uygun olacak şekilde özelleştirilmişti; pekiştirmeli öğrenmeyle çok adımlı akıl yürütme / problem çözme / teorem kanıtlama verileri üzerinde eğitildi ve yüksek kaliteli matematik çözüm kitaplarıyla IMO problem yaklaşım ipuçları da verildi
"Gemini DeepThink'in gelişmiş bir sürümü" ifadesi, gerçekte piyasaya çıkacak Gemini Ultra abonelik ürünündeki DeepThink'ten muhtemelen farklıdır ya da çok daha fazla test zamanı hesaplaması kullanmıştır; yine de OpenAI ile Google'ın rekabetini izlemek eğlenceli
1-6. soruların hepsini çözen context engineering sistem promptu bağlantısını paylaşayım;
o3veyaGemini 2.5ile kullanabilirsiniz. Tüm promptları girip soruyu ekledikten sonra problemi çözmesini istemeniz yeterli. https://github.com/redcrash0721/freederia/blob/main/imo6kr.pdf