Üretmek Ucuzlarken Doğrulama Pahalılaşıyor

Neden doğrulama, neden Lean

Modern matematiğin darboğazı üretmek değil, ikna etmektir. Uzun bir kanıt, okuyucunun dikkatine ve hakemin yeniden kurma kapasitesine bağlıdır; bu yüzden yanlışlar aylarca görünmez kalabilir. Lean bu soruna biçimsel bir cevap verir: kanıt, derlenen bir programdır.

Tao’nun yazılarındaki ısrar bu uçta toplanır. 2025’te, tahminleri doğrulamaya yarayan esnek bir kanıt asistanı üzerine yazdığı gönderi, kendi iş akışında denetimi araca devretme değil, aracın denetlenebilirliğini artırma çizgisini gösterir.

Bu ayrım, olimpiyat skorlarından daha pratik bir iddiadır: bir modelin ürettiği çözüm, biçimsel olarak derlenene kadar matematiksel bilgi değildir. Doğrulama katmanı, yapay zekayı matematiğe sokan kapıdır.

Makine katkılı işbirliği deneyi

Equational Theories Project, Tao’nun 2024 sonbaharında tanıttığı, sonra bir makaleye dönüşen açık bir deneme: cebirsel yapılar üzerine, internet üzerinden yürüyen, katkılarının kaydı tutulan bir çalışma. Projenin kendi tarifi, matematiğe “makine yardımıyla nasıl işbirliği yapılır” sorusunu sorması.

Deneyin değeri sonuçlardan çok yapıda: üretilen her bulgu, ya biçimselleştiriliyor ya da biçimselleştirmeye aday gösteriliyor; böylece ham motor gücün çöpü ile değerlisi ayrışabiliyor. Geniş katılım, modeli tek dâhi sohbeti olmaktan çıkarıyor.

Modele hangi iş veriliyor

Tao’nun tarif ettiği kullanım listesi tipik olarak üç katman: tarama (benzer sonuç nerede kullanılmış), yeniden yazım (bir argümanı başka bir dilde kurmak) ve biçimselleştirme (yazılı kanıtı derlenebilir hale getirmek). Ortak özellik, işin ölçülebilir ve geri döndürülebilir olması.

Buna karşılık sanı üretimi — hangi problemin değerli olduğu — modele devredilmiyor. Nedeni teknik değil, ekonomik: değerli problem, çevresindeki kanıtlar, tanımlar ve sezgiler hakkında yerel bilgi ister; bu bilgi, yazılmadığı için eğitim verisinde yoktur.

Yaygın bir hata, “AI matematik yapıyor” ile “AI matematikçi gibi çalışıyor” cümlelerini karıştırmak. İlki bir yetenek iddiası, ikincisi bir iş bölümü iddiası; Tao’nun pratiği ikincisine dayanıyor.

Uyarının gerekçesi: hatayı modele yedeklemek

Tao’nun en net itirazı yeteneğe değil, bağımlılığa yöneliyor: kendi hatalarını kapatmak için bu araçlara güvenmek, onun deyimiyle oldukça riskli. Sebep basit — model, hatayı tekrar eden ama özgüveni yüksek üslubu da öğrenmiştir.

Pratikte bu, iki kontrol katmanı demek: üretilen satırın insan tarafından okunması ve üretilen iddianın makine tarafından derlenmesi. İkincisi olmadan birincisi yorgunluğa yenilir; birincisi olmadan ikincisi yanlış hedefi hatasız doğrular.

Bu yüzden “doğrulama maliyeti” metrik olarak izlenmesi gereken şeydir: bir modelin ürettiği kanıt başına, biçimselleştirmeye giden insan saati. Verimlilik hikâyeleri, çoğu zaman bu saatin saklandığı yerden büyür.

Matematikçinin rolü nereye kayıyor

Hesap ve kopyalama işi ucuzlarken üç şey kıymetleniyor: hangi problemin sorulacağı, kanıtın hangi kısmının esas fikir olduğu ve bir sonucun hangi dile çevrileceği. Bunların hepsi anlatı ve seçim becerisidir; otomasyon bunları ucuzlatmadı.

İkinci bir sonuç pedagojik: öğrencinin “zor” saydığı rutin, artık öğreten işlevini yitiriyor. Müfredatın, hesaptan çok denetim ve formalizasyona dönmesi gerekiyor; aksi hâlde mezun, aracın ürettiğini okuyamayan bir onay makinesi olur.

Üçüncüsü, kurumsal: doğrulama altyapısı bir kamu malı gibi davranır. Mathlib’in büyüklüğü, hangi soruların cevaplanabilir olduğunu değiştirir. Yapay zeka çağında matematikçinin en stratejik katkısı, muhtemelen, bu altyapıya yazılan satırdır.

Sık sorulan sorular

Kaynakça

1. The equational theories project: a brief tourTerence Tao (blogs)
2. The Equational Theories Project (makale)arXiv
3. A tool to verify estimates, II: a flexible proof assistantTerence Tao (blogs)
4. Equational Theories Project kayıtlarıGitHub