Lean4, Terence Tao’nun son makalesindeki küçük bir hatayı bulmaya yardımcı oldu

• Terence Tao, Lean4 biçimselleştirme projesi üzerinde çalışırken makalesindeki küçük ama önemsiz olmayan bir hatayı fark etti
• Hata, arXiv makalesi 2310.05328 içindeki 6. sayfadaki argümanda ortaya çıktı; burada 1/2 log((n - 1)/(n - k - 1)), n = 3, k = 2 iken ıraksıyor
• Sorun yalnızca küçük n değerleriyle sınırlı; n >= 8 için mevcut argüman çalışmaya devam ediyor ve küçük n değerleri daha kaba bir yöntemle doğrudan ele alınabiliyor
• Lean, 0 < n - 3 ispatını istedi ancak varsayım olarak yalnızca n > 2 vardı; bu yüzden linarith taktiği gerekli çelişkiyi elde edemedi
• Tao, bazı sayısal sabitleri ayarlayarak argümanı düzelteceğini ve yeni sürüme, önceki argümandaki bu isabetsizliğin Lean ile biçimselleştirme girişimi sırasında fark edildiğini belirten bir dipnot eklemeyi planlıyor

---

Lean4 biçimselleştirmesinin ortaya çıkardığı hata

• Terence Tao, kendi Lean4 biçimselleştirme projesi sırasında makalesinde küçük ama önemsiz olmayan bir hata olduğunu keşfetti
• Biçimselleştirilen bölüm, arXiv makalesi 2310.05328 içindeki 6. sayfadaki argümandı
• Sorunlu ifade şu biçimdeydi
  • 1/2 log((n - 1)/(n - k - 1))
• Bu ifade n = 3, k = 2 olduğunda ıraksıyor

Hatanın kapsamı ve düzeltme yöntemi

• Bu sorun yalnızca küçük n değerlerinde ortaya çıkıyor
  • n >= 8 için ilgili argüman hâlâ çalışıyor
  • Küçük n değerleri daha kaba bir yöntemle doğrudan ele alınabiliyor, ancak sabitler daha kötü oluyor
• Tao, ilgili sayfadaki bazı sayısal sabitleri değiştirerek argümanı düzeltebileceğini düşünüyor
• Makalenin yeni sürümüne, önceki argümanın biraz isabetsiz olduğunu ve bunun Lean ile biçimselleştirme denenirken fark edildiğini belirten bir dipnot eklemeyi planlıyor

Lean’in takıldığı somut nokta

• Biçimselleştirme başarısız olduğunda Lean, 0 < n - 3 ifadesinin ispatını istedi
  • Eldeki kullanılabilir varsayım yalnızca n > 2 idi
  • linarith taktiği, 0 < n - 3 ifadesinin değillemesinden bir çelişki çıkaramadı

[GN⁺]

Hacker News yorumları

• Bu ayın başlarında GPT-4’ün yardımıyla Lean4 öğrenmeye başlamış: https://mathstodon.xyz/@tao/111208692505811257
  Bu ayki Mastodon gönderilerinin epeyce bir kısmı öğrenme süreciyle ilgiliydi; bu da büyük dil modellerinin en üst düzeyde başarı gösteren kişilerin çalışmalarını bile ne kadar hızlandırabileceğini gösteren ilginç bir örnek.

  • Kod yazamasa bile iletişim becerisi iyi olan kişilerin büyük dil modelleriyle çalışan otomasyonları hızlıca oluşturabildiğini gördüm.
    İlginç biçimde, bu araçlar yalnızca çok becerikli kişiler tarafından etkili kullanılabiliyorsa eşitsizliği daha da artırabilir.
  • GPT-4 şaşırtıcı. Bugünlerde programlamayla ilgili bir soruya başlarken Google’ı neredeyse hiç kullanmıyorum.
  • Bir ölçüde katılıyorum ama Terry o kadar istisnai biri ki bu örneği genellemenin zor olduğunu düşünüyorum. Elbette kendisi cömert ve mütevazı biri de.
  • Elitler için kolayca 100 katlık bir araç oluyor. Artık en üst düzey mühendisler 10000 kat verimlilik üreten kişiler.

• Lean4’e kolayca başlamak istiyorsanız Natural Number Game iyi bir seçenek: https://adam.math.hhu.de/#/g/hhu-adam/NNG4
  Oyun olmadan sadece okumak isterseniz burası: https://lean-lang.org/theorem_proving_in_lean4/introduction.html

  • Acemi olduğum için merak ediyorum: Lean4, TLA+ veya Alloy’dan nasıl farklı? Başta karşılaştırılabilecek şeyler olup olmadıklarını da merak ediyorum.
    İlk başta Alloy’u Allow diye yazmıştım.

• Birkaç yıl önce, yazdığım programlardaki hataları azaltmanın yollarını ararken Lamport’un TLA+’ını öğrendim ve program davranışını durum makinesi olarak düşünerek biçimsel belirtim yazmayı öğrendim.
  TLA+ soyutlamaları net biçimde anlamamı sağladı; daha sonra Coq ispat yardımcısını kullanarak biçimsel olarak doğru yazılım üretmeyi anlatan Software Foundations serisini de keşfettim. Alıştırmalar küçük oyunlar gibi düzenlenmişti, çözmesi oldukça keyifliydi: https://softwarefoundations.cis.upenn.edu/

  • Kod doğruluğu kayıp bir sanata dönüştü. Soyut düşünme gerekliliği birçok geliştiriciyi korkutuyor.
    Üst düzey bir soyutlama olan biçimsel belirtim, kodu açıklamak için özel bir dile odaklanır; alt düzey bir soyutlama olan kod sözleşmeleri ise doğrulama mantığını daha iyi bir modelle değiştirmeye daha yakındır. C#’ta bir zamanlar Code Contracts[1] vardı; Z3 SMT çözücüsü[2] ile derleme zamanında sözleşmeleri denetleyen basit ama güçlü bir yöntemdi, ancak birkaç yıl sonra terk edildi[3] ve .NET Runtime’dan kaldırılınca fiilen sona erdi. Şu anda C#’ta buna en yakın şey muhtemelen Dafny[4]; C# geliştirme tarafı da hâlâ bunu doğrudan dile nasıl ekleyebileceğini düşünüyor[5].
    [1] https://www.microsoft.com/en-us/research/project/code-contracts/
    [2] https://github.com/Z3Prover/z3
    [3] https://github.com/microsoft/CodeContracts
    [4] https://github.com/dafny-lang/dafny
    [5] https://github.com/dotnet/csharplang/issues/105
  • Idris2’ye de baktın mı merak ediyorum. Bu tür teorem ispatlayıcıları gördüğümde genel programlamayla aralarında hep bir empedans uyumsuzluğu varmış gibi hissettim.
    Idris2, genel amaçlı bir dil olmayı hedeflerken teorem ispatı için daha gelişmiş bir tip sistemi de sunuyor gibi görünüyor: https://github.com/idris-lang/Idris2
  • Ben de Software Foundations ile aynı olumlu deneyimi yaşadım.
    Coq yerine Agda kullanan, bir ölçüde türetilmiş bir kitap da var: https://plfa.github.io/
    Henüz okuyamadım ama listeme aldım; Agda ya da Idris’in Coq’tan daha çok bir programlama dili gibi hissettirmesi olası diye düşünüyorum.

• Bağımlı tipler konusunda gerçekten heyecanlıyım. Ancak bir süre daha gelmeleri zor görünüyor.
  Dependent Haskell üzerinde çalışılıyor, ama mevcut bir dile sonradan eklemenin zor olduğu söyleniyor; Idris’in yaratıcısı da Idris’in başka dillere model olmasını umduğunu söylemişti, ana akımda benimsenmesi ise zor görünüyor. Coq, Agda, F* da genel amaçlı diller olarak tasarlanmış değil. Derleyici uygulaması karmaşık, sözdizimi de uzun ve hantal olabilir; ama benim istediğim şey basitlik. Girdi ve çıktı hakkında bildiğim her şeyi kodlamak istiyorum. Günümüz ana akım dillerinde, argümanlar veya çıktılar hakkında çoğu zaman tip sisteminin ifade etmemize izin verdiğinden daha fazlasını biliyoruz.

  • Bağımlı tiplere duyulan heyecanı tamamen paylaşıyorum; ancak alıştığımız tip sistemlerinden farklı olarak bağımlı tipler hakkındaki teoremleri kanıtlamak çok daha zor olduğundan, tüm programda kullanmak pek rahat görünmüyor.
    TypeScript’teki gibi kademeli bir yaklaşımla, her şeyi her yerde kanıtlamak zorunda kalmadan, herhangi bir noktaya tip düzeyinde değer kısıtı bilgisi ekleyebilmek güzel olurdu.
  • Bağımlı tipleri basitçe anlatmak gerekirse, bir değişkenin tipinin başka bir değişkenin değerine bağlı olabilmesi kavramıdır.
    Örneğin bir sayı listesini ve uzunluğunu birlikte biliyorsanız, bağımlı tiplerle uzunluğu açıkça içeren bir liste tipi oluşturabilir ve derleme zamanında işlemlerin bu uzunluğu koruduğunu garanti edebilirsiniz. Yalnızca uzunluğu 3 olan listeleri kabul eden bir fonksiyon tanımlayıp uzunluğu 4 olan bir liste verirseniz derlenmez; böylece hatayı çalıştırmadan önce yakalayabilirsiniz. Tiplerin daha ifade gücü yüksek hâle gelmesi ve değişkenler arasındaki karmaşık ilişkileri bile kodlayan ek bir güvenlik denetimi katmanı gibi düşünülebilir.

• Kuşağımızın en parlak zihinlerinden biri büyük dil modelleri ile otomatik ispatın birleşimi sayesinde çalışma kapsamını genişletebiliyorsa, bu teknoloji kombinasyonunun geleceği son derece iyimser görünüyor.
  Başlangıç bir hata düzeltmesi; ardından doğrulamaya yardım etme; sonunda da yeni keşifleri zorlayıp sınırları genişletme aşaması gelecek gibi. Moore Yasası benzeri dinamiklerin, aslında böyle birikimli bir niteliği olmayan alanları “enfekte etmesi” olgusunu adlandıracak bir terime ihtiyacımız var. Ek bağlam olarak, Terence Tao Lean öğrenirken Copilot kullanıyor: https://mathstodon.xyz/@tao/111271244206606941
  Copilot olmadan da yapabilirdi; ama yeni araçları benimsemenin sürtünmesi yüzünden belki hiç başlamayabilirdi. Büyük dil modellerinin bu tür “düşüncenin bisikleti” durumlarında büyük potansiyeli var.

  • Lean 4 hem bir programlama dili hem de bir teorem ispatlayıcı; bildiğim kadarıyla büyük dil modelleriyle ilgisi yok.
  • Büyük dil modelleri, İngilizce gibi doğal diller için bir derleyicidir.

• Birkaç yıl önce Terence Tao’nun matematik blogundaki bir yazıda da bir hata bulmuştum. Haber verdim, düzeltti ve teşekkür de etti.
  Elbette Hacker News’in ön sayfasına çıkmadı.

  • İlgilenenler için blog yazımda daha ayrıntılı yazmıştım: https://news.ycombinator.com/item?id=38040982

• Lean4’ün başka bir büyük dil modeli olduğunu sanıp endişelenmiştim; oysa aslında oldukça sağlam ve güvenilir bir araçmış.

  • Terence Tao’nun bir makalede hata bulmasına yardımcı olabiliyorsa, benim ölçütlerime göre yeterince sağlam ve güvenilirdir.
  • Lean 4 topluluğu, ispat yardımcılığı ve biçimselleştirme için büyük dil modelleriyle teorem ispatlayıcıları birleştirme konusunda oldukça iyimser.
  • Haber “Terry Tao, ChatGPT’yi yeni teoremleri ispatlamakta çok faydalı buluyor” olsaydı, kişisel olarak bu haberden daha büyük bir gelişme olurdu.
  • Tao, biçimselleştirme çalışmalarında Copilot’ın faydalı olduğunu düşünüyor: https://mathstodon.xyz/@tao/111271244206606941

• Lean kanıt denetleyicisi gibi biçimsel kanıt denetleyicileri ile, Lean gibi biçimsel bir dilde sentetik varsayım-kanıt çiftleri üreten dil modellerinin birleştirilip birleştirilemeyeceğini merak ediyorum
  Lean kanıt denetleyicisiyle, dil modelinin yazdığı sentetik kanıtın doğru olup olmadığı otomatik olarak doğrulanabilir; bu bilgi de özgün dil modeline uygulanacak pekiştirmeli öğrenme ödül sinyali olarak kullanılarak daha iyi kanıtlar yazması sağlanabilir. Ya da önceki turlardaki doğru sentetik kanıtlar eğitim verisi yapılıp yeni bir model eğitilebilir. Bu daha karşıt biçimde de kurgulanabilir. Sistemi bir varsayım üretim modeli ile bir kanıt/çürütme modeline ayırıp, sentetik kanıtın Lean kanıt denetleyicisi tarafından doğrulanıp doğrulanmayacağını tahmin eden bir model eklemek gibi. Doğru olma olasılığı ne kadar düşük tahmin edilirse, gerçekten doğru bir kanıt ürettiğinde kanıt üretim modeli o kadar büyük ödül alır. Son olarak, belirli bir sentetik varsayım için kanıt üretim modelinin alacağı ödülü tahmin eden bir model eklenirse, varsayım üretim modeli kanıt üretim modeli için ne çok zor ne de çok kolay olan, beklenen ödülü yüksek varsayımlar üretmeye teşvik edilir. Tüm sistem giderek daha zor sentetik kanıtlar üretir ve bu da kanıt üretim modelinin daha iyi kendi kendine öğrenmesine yol açabilir. İlke olarak kanıt üretiminde insanüstü yeteneklere kadar ölçeklenebilir; GAN’lere ya da AlphaGo Zero’nun kendi kendine oyun oynamasına benzer. Zor kısım ilk bootstrap aşamasıdır; üretim modelinin ilk eğitimi için insanlar tarafından sağlanmış Lean kanıt verileri gerekir. Ancak sentetik kanıtlar yeterince iyi hâle gelirse sistem otomatik olarak kendi kendine öğrenmeyi sürdürebilir

  • Bu iş akışı Lean 4 geliştiricilerinin açık hedeflerinden biri. Resmî Zulip sohbetinde de ikisi arasındaki arayüzü ele alan bir kanal var: https://leanprover.zulipchat.com/#streams/219941/Machine%20Learning%20for%20Theorem%20Proving
  • Böyle bir modeli tüm matematik literatürü üzerinde eğitmek de ilginç olabilir. İnsan bunun, matematik literatüründeki kanıtları doğrulanabilir bir biçime çevirip doğrulamak için kullanılmasını ister
    Sonunda matematik literatüründeki tüm teoremleri ve tüm doğru kanıtları bilen bir modele sahip olunabilir
  • Görünüşe göre zaten makine öğrenimi tabanlı kanıt sentezi dünyasına girmiş durumdayız. Anlattığım bütün sistemin tamamlandığını sanmıyorum ama benzer sistemler ve bileşenler çok sayıda var
    Mevcut kanıtlarla gözetimli öğrenmeye başlayıp yeni kanıtlar bulmaya yönelik erken aşama örnekler arasında TacticToe (https://arxiv.org/abs/1804.00596), Tactician (https://arxiv.org/pdf/2008.00120.pdf), CoqGym/ASTactic (https://arxiv.org/abs/1905.09381), Proverbot9001 (https://arxiv.org/abs/1907.07794), Diva (https://dl.acm.org/doi/10.1145/3510003.3510138#sec-terms) sayılabilir. Çoğunun içinde bir biçimde dil modeli var; ama son dönemde büyük ilgi gören büyük dil modellerini arıyorsanız GPT-f (https://arxiv.org/abs/2009.03393), Baldur (https://arxiv.org/abs/2303.04910), COPRA (https://arxiv.org/abs/2310.04353) var. Bununla birlikte şu an için bu modeller, özelleşmiş büyük dil modeli olmayan araçlar kadar etkili görünmüyor. İnsanların yazdığı kanıtların ötesine geçip pekiştirmeli öğrenmeyle öğrenme tarafında TacticZero (https://openreview.net/forum?id=edmYVRkYZv), OpenAI makalesi (https://arxiv.org/pdf/2202.01344.pdf), rlCoP (https://arxiv.org/abs/1805.07563), HOList serisi çalışmalar (https://arxiv.org/pdf/1905.10006.pdf), HyperTree Proof Search (https://arxiv.org/abs/2205.11491) bulunuyor; ayrıca University of Massachusetts ekibiyle benim sürdürdüğüm çalışma da var
  • Bunu hâlihazırda yapan insanlar var. Lean tarafındaki bir örnek burada: https://morph.so/blog/the-personal-ai-proof-engineer/

• Tao’nun bu süreçte GPT-4 dâhil büyük dil modeli araçlarını nasıl kullandığına dair önceki bağlam burada: https://mathstodon.xyz/@tao/111233986893287137

• İlerleyişi GitHub üzerinden de takip edilebilir: https://github.com/teorth/symmetric_project/