Araştırma 2026-08-20

Makine yazımı ispatlar o kadar çoğaldı ki matematikçiler bir kayıt bürosu kurdu — iki denetiminden birini bir dil modeli yapıyor

Terence Tao 18 Ağustos'ta, Lean FRO ve ICARM tarafından kuluçkaya alınan Lean doğrulamalı matematik kayıt sistemi Palomar'ın gönderime açıldığını duyurdu. Çözmeye çalıştığı sorun yeni: son aylarda eski ve yeni sonuçların yapay zekâ üretimi ispatları büyük sayıda ortaya çıktı ve bunların hatırı sayılır bir kısmı, her adımı makineye onaylatmayı sağlayan ispat asistanı Lean'de biçimselleştirildi. Ama GitHub'da duran bir Lean deposu kendi kendini anlatmaz. Kodun, yazarının iddia ettiği şeyi gerçekten ispatlayıp ispatlamadığını çıkarmak ciddi bir emek ister; Lean kullanmayan bir matematikçi için neredeyse imkânsızdır. Palomar, gönderilen depoyu iki denetimden geçiriyor. İlki mekanik: Comparator adlı Lean aracı, modülün tip denetiminden geçtiğini ve tam olarak iddia edilen sonuçları ispatladığını doğruluyor. İkincisi, gündelik dildeki açıklamanın biçimsel ifadeyle örtüşüp örtüşmediğini soruyor ve bu denetimi büyük bir dil modeli yapıyor. İkisini de geçen depolar kayda alınıyor; tam ifade, dayanılan kütüphaneler ve değerlendirenin notları yanında yayımlanıyor. Tao bunu Lean ispatları için bir ön baskı sunucusunun karşılığı diye tanımlıyor ve Jeremy Avigad, Matthew Ballard, Jaume de Dios, Nestor Guillen, Bryna Kra, Kim Morrison, Ravi Vakil ve Akshay Venkatesh ile birlikte bilimsel danışma kurulunda yer alıyor.

Bu neden önemli?Matematikte hakem değerlendirmesi iki ucunda da insan darboğazı varsayıyordu: bir kişi ispatı yazar, insanlar okur. Makineler ilk yarıyı kırdı; ikinci yarı zaten hiç ölçeklenmemişti. Palomar, eksik tesisatı kurmaya yönelik ilk ciddi girişim ve merkezindeki tavizi açıkça söylüyor. Biçimsel denetim su sızdırmaz; ama biçimsel ifadenin gerçekten kimsenin umursadığı ifade olup olmadığı sorusunu, tam da bu selin sebebi olan türden bir sistem cevaplıyor. Bu bir skandal değil, elde olan dürüst seçenek ve gizlenmek yerine açıkça yazılmış. Daha büyük işaret şu: bir disiplin, makine üretimi işi kabul edip etmeyeceğini tartışmayı bırakıp onu ayıklayacak altyapıyı tasarlamaya başladı. Bu, hemen hemen her başka alandan daha ileri bir nokta.

#Kodlama #Bilim & Araştırma

✓ Doğrulandı · 4 kaynak

Uygulamada oku — ücretsiz, 9 dilde

İlgili haberler

Makine öğrenmesi hasta beyin hücrelerinin biçimini okudu ve onları sakinleştiren, hâlihazırda onaylı dokuz ilacı seçti
2026-08-21 Söylenti: Bir kodlama kıyaslamasının tepesine ücretsiz oturan isimsiz modelin, Zhipu'nun yayınlanmamış amiral gemisi olduğu iddia ediliyor
2026-08-21 Nvidia, rakibinin model üreten makinesine 6 milyar dolar ödüyor — ve o makineyi çalıştıran 109 kişiyi işe alıyor
2026-08-21 Yapay zekânın eğitilme biçimini iyileştirmek için dört saat ve bir GPU verildi: en iyi ajan 1 üzerinden 0,25 aldı — çoğu ise hiç denemedi
2026-08-21 Ajan, kendi kodunu savunsun diye ikinci bir kişi uydurdu. Teksas'taki 24 yaşındaki öğrenci ikisine de inanmadı.
2026-08-21