Yapay zekâ güncellemesi: 43 milyon satırlık bir ispat, sızan bir önbellek ve ucuzlayan kamu yapay zekâsı

Bir önceki güncellemede “yapay zekâ artık yalnızca daha akıllı model yarışı değil” diye bitirmiştim. Bu iki gün o cümleyi farklı bir açıdan doğruladı: öne çıkan haberlerin neredeyse hepsi bir şekilde güven ve doğrulama ile ilgiliydi. Bir ispatın gerçekten doğru olup olmadığı, bir bulut servisinin müşterilerin verisini birbirinden ayırıp ayıramadığı, devletin bu araçları hangi koşullarla kullanacağı ve ajanların uygulamalarımıza hangi kapıdan gireceği. Her zamanki notum: şirket rakamları, aksini belirtmedikçe şirketin kendi iddiasıdır.

1. “Devasa teorem” artık bilgisayar tarafından kontrol edilmiş

Axiom, 26 Ekim’de sonlu basit grupların sınıflandırmasının (CFSG) Lean ispat asistanında tamamlanmış, bilgisayarla denetlenmiş ilk ispatını yayımladı. Şirketin anlatımına göre özgün ispat yaklaşık 100 matematikçinin 500’den fazla makalesine yayılan yaklaşık 15.000 sayfa tutuyor ve bu yüzden “devasa teorem” diye anılıyor. Axiom’un mühendis ve matematikçileri 24 gün boyunca onlarca yapay zekâ ajanından oluşan “sürüleri” yönlendirmiş; ortaya yaklaşık 43,1 milyon satır Lean kodu çıkmış (Axiom). Kod açık; depo, ispatın sorry (yani “bunu sonra kanıtlarım” boşluğu) içermediğini ve yalnızca standart aksiyomları kullandığını belirtiyor (GitHub, AxiomMath/CFSG).

Benim için en ilginç kısım, biçimselleştirmenin yayımlanmış literatürde sorunlar bulması. Axiom’a göre çoğu yazım ya da tablo hatası gibi küçük şeylerdi, ama 34 kayda değer sapma çıktı; en önemlisi “Dengesiz Grup Teoremi”ne giden yayımlanmış bir yoldaki bir iddiaya karşı örnek bulunması. Ekip bunun için alternatif bir argüman geliştirip ayrı bir makalede anlatmış (CFSG in Lean).

Bir önceki yazıda OpenAI’ın bilimsel iddialarında “kim doğrulayacak?” sorusunu sormuştum. Bu haber o soruya güzel bir karşılık: yapay zekâ burada yeni bir şey iddia etmekten çok, insanların zaten inandığı bir sonucu satır satır kontrol edilebilir hâle getiriyor. Yine de bir uyarıyı not etmek istiyorum: Lean her adımı denetler ama biçimsel ifadenin gerçekten kastedilen matematiği yakalayıp yakalamadığına hâlâ insanlar bakmalı. Axiom da benzer bir noktayı, ilerlemenin kolayca abartılabileceğini kendi yazısında açıkça söylüyor (Axiom).

2. Cloudflare: Uzun istemler başka müşterilerin verisini görmüş

Cloudflare, 26 Ekim’de dürüst ve ayrıntılı bir olay raporu yayımladı. Workers AI üzerinde sunulan GLM-5.3 modeli, 27 Ağustos ile 9 Eylül arasında bazı müşterilere, kısa süre önce başka müşterilerin aynı modele gönderdiği isteklerden veri içeren yanıtlar vermiş. Toplam 155 yanıt etkilenmiş ve hepsi 681.280 token’dan uzun istemlere verilen yanıtlarmış. Sorunu bir güvenlik araştırmacısı HackerOne üzerinden bildirmiş; Cloudflare modeli ertesi gün kapatıp aynı gün düzeltilmiş hâliyle geri açmış. Şirket kasıtlı istismara dair bir kanıt bulmadığını söylüyor (Cloudflare).

Nedeni iki hatanın üst üste binmesi: Model 1.048.576 token’lık bağlam penceresiyle sunulmuş ama ön işleme (prefill) GPU’larındaki KV önbelleği (modelin daha önce okuduğu metni hızlı hatırlamak için tuttuğu ara bellek) yalnızca 681.280 token’a yetiyormuş. Açık kaynak çıkarım motoru SGLang’deki bir hata yüzünden sığmayan istek hata döndürmek yerine işlenmeye devam etmiş ve yanıt, önceki isteklerden kalan eski önbellek sayfalarına bakılarak üretilmiş (Cloudflare). SGLang ekibi de aynı gün eşgüdümlü bir açıklama ve düzeltmeler yayımladı (LMSYS / SGLang).

Bu olay bana yapay zekâ güvenliğinin her zaman “model ne kadar tehlikeli?” sorusu olmadığını hatırlattı. Bazen mesele, çok sıradan bir altyapı ayarı ve bir hata yolunun doğru test edilmemesi. Raporun en öğretici cümlesi bence şu itiraf: ekip bu boyut uyumsuzluğunu yayından önce biliyormuş ama motorun sığmayan istekleri reddedeceğini varsaymış. Ben de kendi küçük projelerimde “hata durumunda ne olur?” sorusunu daha sık test etmem gerektiğini not ettim.

3. Anthropic devlet için fiyatı düşürüyor

Anthropic ve ABD Genel Hizmetler İdaresi (GSA), 27 Ekim’de OneGov anlaşmasını genişlettiklerini duyurdu. Yeni anlaşmayla devlet kurumları Claude Enterprise, Claude for Government ve Claude API’de %40 indirim alıyor; ilk kez eyalet, yerel, kabile ve bölge yönetimleri de kapsama giriyor. Asgari harcama taahhüdü yok, kurumlar kullandıkları kadar ödüyor (Anthropic; GSA). Anthropic indirimlerin devlete yaklaşık 1 milyar dolar tasarruf sağlayacağını tahmin ediyor ve yaklaşık 500 ABD kamu kurumunun Claude kullandığını söylüyor; bunlar şirketin kendi rakamları (Anthropic). Nextgov’un aktardığına göre bu anlaşma, federal kurumların kullanıcı başına 1 dolara Claude aldığı eski teklifin 31 Ekim’de sona ermesinden hemen önce geliyor; OpenAI de ay başında GSA ile token bazlı kullanımda %50 indirimli benzer bir anlaşmaya geçmiş (Nextgov/FCW).

Burada gördüğüm eğilim, “tanıtım fiyatı” döneminin bitip kullanıma göre ödemeye geçilmesi. Bir önceki yazıda GPT-6.1 Terra için “ajanların yaygınlaşmasını birim maliyet belirleyecek” demiştim; kamu alımlarında da aynı şeyin yaşandığını görüyorum. Fiyat artık en az performans kadar güçlü bir rekabet aracı.

4. Apple, iWork uygulamalarının kapısını ajanlara açıyor

Apple, 27 Ekim’de Creator Studio güncellemesini duyurdu. Keynote, Pages ve Numbers’a, Apple modelleri ve OpenAI üzerine kurulu, belgenin bağlamını anlayan bir asistan (beta) geliyor. Benim için asıl haber ise Model Context Protocol (MCP) desteği: dış yapay zekâ ajanları ve araçları bu üç uygulamada içerik okuyabilecek, düzenleme yapabilecek ve otomatik işlemler çalıştırabilecek. Keynote ayrıca harici araçların ve ajanların okuyabileceği, JSON tabanlı açık bir dosya biçimi olan Keynote Interchange Format’ı (.keyx) destekliyor. Güncellemeler kasım ayında App Store’a gelecek; asistan şimdilik yalnızca ABD İngilizcesinde ve iOS 27, iPadOS 27 veya macOS 27 gerektiriyor, MCP desteği ise macOS 27 ve sonrasında çalışacak (Apple; The Verge).

Agent Skills yazısında ajan dünyasının ortak standartlara doğru gittiğini yazmıştım. Apple gibi kapalı ekosistemiyle bilinen bir şirketin kendi asistanının yanına, başka şirketlerin ajanlarına da açık bir kapı koyması bu eğilimin güçlü bir işareti. Öte yandan Cloudflare olayından sonra şunu düşünmeden edemiyorum: belgelerimize yazabilen bir ajan, iyi tanımlanmış izinler ve geri alma imkânı olmadan kurulmamalı.

Benim çıkarımım

Bu iki günden aklımda kalan şu: yapay zekânın değeri giderek “ne kadar şey üretebildiğinden” çok “ürettiğinin ne kadar denetlenebildiğine” bağlanıyor. 43 milyon satırlık bir ispat, ancak her satırı kontrol edilebildiği için anlamlı; bir bulut servisi, ancak müşterilerini birbirinden ayırabildiği sürece güvenilir. Bir sonraki güncellemede bu doğrulama araçlarının nerelere yayıldığına bakmaya devam edeceğim.

---

Kaynaklar

• Axiom — Formalizing the Enormous Theorem
• GitHub — AxiomMath/CFSG README
• Axiom — The Classification of Finite Simple Groups, formalized in Lean
• Cloudflare — Cross-request KV cache exposure in the GLM-5.3 Workers AI model, and our remediation with SGLang
• LMSYS Org — SGLang security update: improving request isolation
• Anthropic — Expanding our partnership with GSA to bring Claude to all levels of government
• GSA — GSA, Anthropic Reach OneGov Agreement on Discounted, Consumption-Based Pricing for Claude
• Nextgov/FCW — GSA unveils token-based OneGov pricing for Claude
• Apple — Apple Creator Studio adds powerful new AI features and even more creative tools
• The Verge — Apple is adding an AI chatbot to Pages, Keynote, and Numbers