AlphaProof: AI Matematik Olimpiyatında Gümüş Madalyaya

"Matematik AI için zor"

Klasik AI varsayımı: matematik insan dehasının zirvesidir. AI yapamaz.

Bu varsayım 2023'te çözülmeye başladı. Temmuz 2024'te DeepMind şok haberle çıktı:

"AlphaProof ve AlphaGeometry 2 Uluslararası Matematik Olimpiyatı (IMO) 2024 sorularını gümüş madalya düzeyinde çözdü."

6 sorudan 4 tanesi. 42 üzerinden 28 puan. 609 öğrencinin 58'inden daha iyi.

IMO — matematik olimpiyatları

IMO yıllık uluslararası lise matematik yarışması:

• 110+ ülke.
• En zeki lise öğrencileri.
• 6 soru, 2 gün, 9 saat.
• Genelde geometri + cebir + sayı teorisi + kombinatorik.

Altın madalya: Yaklaşık ilk 50. Gümüş: İlk 200. AlphaProof gümüş.

AlphaProof + AlphaGeometry 2

İki ayrı sistem:

AlphaProof

• Genel matematik: Cebir, sayı teorisi, analiz.
• Reinforcement learning + LLM.
• Formal ispat dilinde (Lean) çalışır.

AlphaGeometry 2

• Geometri uzmanı.
• Neuro-sembolik: LLM önerir, sembolik motor doğrular.
• AlphaGeometry 1 (2024 başı) üzerine kurulu.

Lean — formal matematik dili

AlphaProof Lean programlama dilinde çalışır. Lean modern formal matematik aracı.

İspatlar mantıksal olarak doğrulanmış — yanlış olamaz. Klasik kağıt-kalem matematikten farklı.

Bu sayede sistem yanlışı tespit edebilir: ispat geçerse doğru, geçmezse yanlış.

Performans detayları

• Soru 1, 2, 6: AlphaProof çözdü (cebir + sayı teorisi).
• Soru 4: AlphaGeometry 2 çözdü (geometri).
• Soru 3, 5: Çözemediler (kombinatorik zor).

Çözüm zamanı: insan 4.5 saat, AlphaProof birkaç dakika - 3 gün. Yani tek bir soru için bazen günler.

Trilyonlarca sentetik veri

AlphaProof eğitimi:

• 1M+ insan ispatı (Lean kütüphanesinden).
• Trilyonlarca sentetik ispat (kendi kendine üretti).
• Pekiştirmeli öğrenme — başarılı ispatlardan öğrendi.

Bu, self-play matematik versiyonu. AlphaGo'nun self-play satrancın olimpiyat matematiğine uyarlanmış hâli.

"Bilgisayar bilimi içinde matematik"

Modern AI dünyasında formal matematik önem kazanıyor. Sebepler:

1. Yanlış tespiti: AI ispatlarını otomatik kontrol etmek.
2. Sentetik veri: AI ispatların sonsuz sentetik veri kaynağı.
3. Akıl yürütme test alanı: Matematik AI sınırlarını ölçer.
4. Bilim için: Kuantum fiziği, kompleks teorem ispatları.

Bu hat Terence Tao ve diğer dünya çapında matematikçilerin de ilgisini çekti.

o1 ve diğer reasoning modeller

AlphaProof, OpenAI o1 ile aynı hat. Modern AI artık akıl yürütme odaklı:

• o1: Genel akıl yürütme.
• DeepSeek-R1: Aynı.
• AlphaProof: Matematik özgü.

Hepsi test-time compute paradigmasının somut örneği.

"AGI yolundaki adım?"

AlphaProof matematik başarısı AGI tartışmasını alevlendirdi:

• Iyimser: Matematik insan zekâsının zirvesi; AI yapıyor → AGI yakın.
• Karşı görüş: Matematik özel; sağduyu, robustness, etik AI hâlâ zayıf.

Bu tartışma sürüyor.

Sade ders

AlphaProof hikâyesinden iki şey:

1. AI insan zekâsının sıralı zirvelerini geçiyor. Satranç, Go, protein, matematik, kodlama... Her birinde AI ulaşıyor. Bu, uzun vadeli paradigma değişimi.
2. Formal yöntemler AI için temeldir. AlphaProof Lean kullanır — yanlış tespit eder. Klasik LLM'ler halüsinasyon yapar. Gelecek: AI + formal doğrulama birleşimi.

Bağlam

DeepMind için: [[demis-hassabis-deepmind-kurucu-ortagi-ve-2024-nobel-kimya]]. Test-time compute için: [[test-time-compute-aiya-dusunmek-icin-zaman-vermek]]. Chain-of-thought için: [[chain-of-thought-llm-leri-akil-yurutmeye-zorlamak]]. GRPO ve reasoning için: [[grpo-deepseek-in-akil-yurutme-icin-rl-algoritmasi]]. AlphaGo ve self-play için: [[monte-carlo-tree-search-mcts-alphagonun-zekasinin-kalbi]].