- Biçimsel doğrulama (formal verification), kodun bir belirtimi her zaman karşıladığını matematiksel olarak kanıtlama yöntemidir ve uzun süre araştırma odaklı sınırlı bir alanda kaldı
- seL4 mikroçekirdeği gibi bazı büyük sistemler biçimsel doğrulamayla geliştirildi, ancak yüksek zorluk ve maliyet nedeniyle sanayide neredeyse hiç kullanılmadı
- Son dönemde LLM tabanlı kodlama yardımcı araçları, yalnızca gerçekleştirim kodunda değil, çeşitli dillerde kanıt betikleri yazımında da sonuç vermeye başlayarak doğrulama maliyet yapısını büyük ölçüde değiştirme ihtimalini ortaya koyuyor
- Yapay zeka, kod üretimiyle birlikte doğruluk kanıtını da otomatikleştirebilirse, insan kod incelemesinden daha güvenilir bir geliştirme yöntemine geçiş mümkün olabilir
- Biçimsel doğrulamanın otomasyonu, yapay zeka çağında yazılım güvenilirliğini sağlamanın temel teknolojisi olarak görülüyor; ana akım yayılımın önündeki asıl belirleyici, teknik sınırlardan çok kültürel dönüşüm olabilir
Biçimsel doğrulamanın bugünü ve sınırları
- Rocq, Isabelle, Lean, F*, Agda gibi kanıt odaklı diller ve araçlar, kodun belirtimi karşıladığını matematiksel olarak kanıtlamayı mümkün kılar
- seL4 işletim sistemi çekirdeği, CompCert C derleyicisi ve Project Everest kriptografik protokol yığını bunun öne çıkan örnekleridir
- Ancak sanayide biçimsel doğrulama neredeyse hiç kullanılmıyor
- seL4 örneğinde, 8.700 satır C kodunu doğrulamak için 20 insan-yılı ve 200 bin satır Isabelle kodu gerekti
- Her bir gerçekleştirim satırı için 23 satır kanıt ve yarım günlük insan emeği gerekiyor
- Dünya genelinde bu tür kanıtları yazabilecek uzmanların sayısının birkaç yüz düzeyinde olduğu tahmin ediliyor
- Ekonomik açıdan da çoğu sistemde hataların yol açtığı kayıptan doğrulama maliyeti daha yüksek, bu yüzden pratikliği düşüktü
Yapay zekanın biçimsel doğrulamanın ekonomisini değiştirmesi
- Son dönemde LLM tabanlı kodlama asistanları, yalnızca gerçekleştirim kodunda değil, kanıt betikleri yazımında da başarı göstermeye başladı
- Nature, Galois ve arXiv gibi kaynaklarda, LLM'lerin çeşitli dillerde kanıt ürettiği örnekler raporlandı
- Bugün hâlâ uzman yönlendirmesi gerekiyor, ancak tam otomasyonun birkaç yıl içinde mümkün olabileceği öngörülüyor
- Doğrulama maliyeti keskin biçimde düşerse, daha fazla yazılımda biçimsel doğrulama uygulanabilir
- Aynı zamanda yapay zekanın ürettiği kod için de insan incelemesi yerine biçimsel doğrulamayla güvenilirlik sağlanması gerekecek
- Yapay zeka, kodun doğruluğunu kendisi kanıtlayabilirse, el yazımı koda göre daha çok tercih edilebilir
LLM'ler ile kanıt doğrulamanın karşılıklı tamamlayıcılığı
- LLM'ler kanıt betiği yazarken asılsız içerik (halüsinasyon) üretse bile, kanıt denetleyicisi (proof checker) bunu reddeder
- Denetleyici, kendi içinde doğrulanmış küçük ölçekli koddan oluştuğu için yanlış bir kanıtın kabul edilmesi zordur
- Bu nedenle LLM'lerin belirsizliğini biçimsel doğrulamanın katılığı telafi eder
- Bu birleşim, yapay zekanın ürettiği kodun güvenilirliğini sağlamak için güvenli bir otomasyon yolu olarak işleyebilir
Yeni görev: belirtim tanımının doğruluğu
- Otomatik doğrulama ortamında bile belirtimin (specification) doğru tanımlanması temel mesele olarak kalır
- Kanıtlanan özelliğin gerçekten geliştiricinin amaçladığı özellikle örtüşüp örtüşmediği kontrol edilmelidir
- Belirtim yazımı hâlâ uzmanlık ve dikkatli düşünme gerektirir, ancak elle kanıt yazmaktan çok daha basit ve hızlıdır
- Yapay zeka, doğal dil ile biçimsel dil arasında belirtim çevirisini destekleyebilir
- Yine de anlam kaybı riski vardır; ancak bunun yönetilebilir düzeyde olduğu değerlendirilir
Yazılım geliştirme biçiminde beklenen değişim
- Geliştiriciler, istedikleri kodun özelliklerini bildirimsel belirtimlerle ifade edip, yapay zekanın gerçekleştirim ve kanıtı birlikte üretmesine yönelebilir
- Bu durumda geliştiricilerin yapay zekanın ürettiği kodu doğrudan incelemesi gerekmeyebilir; kod, derleyicinin makine kodu gibi güvene dayalı şekilde kullanılabilir
- Özetle şu üç değişim bekleniyor
- Biçimsel doğrulama maliyetinde keskin düşüş
- Yapay zeka üretimi kodun güvenilirliğini sağlamak için doğrulama talebinde artış
- Biçimsel doğrulamanın kesinliği, LLM'lerin olasılıksal doğasını tamamlayacak
- Bu etkenler birleşirse, biçimsel doğrulama yazılım mühendisliğinin ana akım teknolojilerinden biri haline gelebilir
- Gelecekte sınırlayıcı unsurun teknolojiden çok geliştirme kültürünün değişimi ne kadar hızlı benimsediği olması bekleniyor
1 yorum
Hacker News görüşleri
Bana göre biçimsel doğrulama (formal verification), spesifikasyona kıyasla implementasyonun çok daha karmaşık olduğu alanlarda gerçekten değerini gösteriyor.
Örneğin kriptografi implementasyonlarında bit düzeyindeki optimizasyonlar ya da derleyici optimizasyon aşamaları gibi yerlerde.
Ancak çoğu geliştiricinin (veya yapay zekanın) yazdığı kod, yüksek seviyeli diller sayesinde zaten spesifikasyona oldukça yakın, bu yüzden biçimsel doğrulamanın faydasının çok büyük olmadığını düşünüyorum.
Spesifikasyonu ayrıca yazmanın daha okunabilir olup olmayacağı da şüpheli.
Zaten bugün de çeşitli framework ve kütüphaneler implementasyon ayrıntılarını soyutluyor.
Biçimsel doğrulama daha güçlü garantiler sağlayabilir, ama çoğu insan böyle bir garanti düzeyi istemiyor ve yapay zekanın da buna yeni bir ihtiyaç yaratacağını sanmıyorum.
Bazı insanlar yapay zekanın biçimsel doğrulamayı tamamen otomatikleştireceğini öngörüyor, ama ben bu mantıkta bir sorun görüyorum.
Eğer yapay zeka yazılımı otomatik olarak ispatlayabiliyorsa, insanın yazdığı yazılımı ayrıca doğrulamaya da gerek kalmaz.
Çünkü yapay zeka fikri kurgulayıp uygulayabilir ve doğrulama düzeyine kendisi karar verebilir.
Sonuçta insanların yaptığı programlama ya da doğrulama büyük ölçüde ortadan kalkabilir.
Gerçekte insanların ispat asistanı tasarlaması mümkün, ama bunlarla büyük ölçekli programları doğrulamak çok daha zor.
Dolayısıyla böyle bir yapay zeka ortaya çıkarsa, yeni ispat asistanlarını da kendisi geliştirebilir.
Elbette bu tür hayaller daha çok bilim kurgu alanına giriyor ve yapay zekanın neyi kolaylaştırıp neyi zorlaştıracağını net bilmeden yapılan tahminlerin çok anlamı yok.
İlgili tartışma bağlantısı
Bu, insanlığın bambaşka bir evreye geçtiği dönüm noktası olabilir.
Kodlama ajanlarından (Claude Code, Codex CLI vb.) faydalı sonuç almak için asıl kritik nokta, onların yazdığı kodu çalıştırıp doğrulayabilecek bir ortam kurmak.
Python gibi çalıştırması kolay diller bunun için en uygun seçenek; HTML+JS ise Playwright gibi araçlar gerektiriyor.
Bir sonraki adım otomatik test paketleri ve ardından code formatter, linter, fuzzer gibi kalite araçları.
Debugger da iyi bir araç, ama etkileşimli olduğu için ajanların kullanması zor olabiliyor.
Bence biçimsel doğrulama araçları da bu spektrumun içinde yer alıyor — çünkü günümüz modelleri özel programlama dilleriyle de iyi çalışıyor.
Eğer kodlama ajanlarının pek işe yaramadığını düşünüyorsanız, bunun nedeni büyük ihtimalle yürütme ve test ortamının yetersiz olmasıdır.
Mesela Haskell’de kod derleniyorsa, neredeyse her zaman doğru çalışır.
Bu özellik insanlar için faydalıysa, LLM’ler için de aynı şekilde faydalı olacaktır.
Özellikle property test, LLM’lerle çok uyumlu — çünkü az sayıda testle geniş bir hata alanını kapsayabiliyor.
Matematik topluluğunda Lean kodunu iyileştirmek için LLM kullanma denemeleri olduğunu görünce, daha güçlü tip sistemlerinden yararlanan yazılım geliştirme de gayet mümkün görünüyor.
Çünkü debugging doğrusal bir süreç değil; neden ve sonuç zaman içinde birbirine karışıyor.
Eskiden gdb ile çok iş parçacıklı bir bug yakalamaya çalışırken ChatGPT’yi denemiştim, ama sadece basitçe print eklemeyi önermeyi tekrarlıyordu.
Sonunda bunun yine deneyim ve sezgi gerektiren bir alan olduğunu hissettim.
Junior bir mühendise debugger veya test runner olmadan çalışmasını söylemek mantıklı değil.
Sonuçta daha fazla hesaplama kaynağı gerekecek gibi duruyor.
Claude implementasyonu yapıyor, Codex ve Gemini ise gözden geçiriyor.
Bu yöntem pahalı, ama öz önyargıyı (self-bias) azaltmak ve kod kalitesini artırmak için bulduğum en güvenilir yol oldu.
Statik analiz araçları da ek fayda sağlayabilir, ama yalnızca araç sayısını artırmanın tek başına yeterli olmadığını düşünüyorum.
Doğrulama süreci otomatikleşirse, gerçekten zor olan kısım spesifikasyonu doğru tanımlamak haline gelir.
İspatın kendisine kıyasla spesifikasyon yazmak çok daha hızlı ve kolaydır, ama yine de uzmanlık ve dikkat gerektirir.
Geçmişte biçimsel ispatların yaygınlaşmamasının nedeni sadece zorluğu değildi; waterfall yaklaşımının ortadan kalkması ve agile geliştirmenin baskın hale gelmesi de etkili oldu.
Uzun spesifikasyonlar yazmak yerine, kullanıcı ihtiyaçlarına göre hızlı iterasyon yapılan bir yönteme evrildik.
Sanırım artık OCaml öğrenme zamanı geldi.
Birçok ispat asistanı ve doğrulama sistemi OCaml kodu üretebiliyor; ADA/Spark da değerlendirilebilir.
Yapay zeka çağında yazılım mühendisliği bir şekilde değişecek, ama bizim bugün olduğundan daha yüksek kaliteli yazılımlar üretmemiz gerekiyor.
Biçimsel doğrulama bu hedefe kesinlikle yardımcı olacaktır.
Henüz tamamlanmamış olsa da deneysel projemi paylaşayım.
Kod odaklı yazıların az olduğu bir dünyada, eğlenceli bir hackathon fikri arayan biri için bakmaya değer olabilir.
py-mcmas proje bağlantısı
LLM’ler doğrulaması kolay problemleri çözmede iyi olma eğiliminde.
Bu yüzden ben problem çözmeyi üç aşamaya ayırıyorum.
1️⃣ Önce başarı koşulunu kontrol eden programı yazıyorum
2️⃣ Sonra o programla asıl problemi doğrulatıyorum
3️⃣ Son olarak da kendim kontrol ediyorum
Bu yaklaşımı uzun zamandır kullanıyorum, ama artık Opus veya GPT-5.2 gibi modeller bunu insansız modda da iyi yapıyor.
İlgili blog yazısı
Doğrulamanın uzun sürdüğü alanlarda, bu durum insanın doğrulama yükünü daha da artırabilir.
“Doğrulama programını kim doğruluyor?” sorusu gelebilir.
Eğer onu da LLM yazıyorsa, bu sonsuz bir kaplumbağa kulesi (turtles all the way down) gibi görünebilir.
zor olan kısım ispatı üretme sürecidir.
Elbette karmaşık önermelerde istisnalar vardır, ama bu yine de bug azaltmada çok işe yarar.
Biçimsel doğrulama yaygınlaşsa bile herkesin Lean ya da Isabelle kullanacağını sanmıyorum.
Daha çok, yapay zekanın mevcut iş akışlarına doğal biçimde entegre olması şeklinde yayılacaktır.
Mesela CI içinde özellik doğrulaması ya da IDE’de “bu modülün invariant’ını ispatla” düğmesi gibi.
Çoğu mühendisin ispat script’lerini doğrudan görmesine bile gerek kalmayacaktır.
Asıl zor olan, LLM’in ispat üretmesi değil; organizasyonların spesifikasyon ve model yazmaya yatırım yapmasını sağlamaktır.
Eğer yapay zeka spesifikasyon önermeyi ve düzenlemeyi kolaylaştırırsa, doğrulama da testler veya linter’lar gibi doğal bir refactoring aracı haline gelebilir.
GPT‑5.2’nin “garlic” kelimesinde kaç tane r olduğunu bile doğru sayamadığından şikâyet edenler de var.
Gerçekten gerekiyorsa, LLM’e bir Python script’i yazdırıp çalıştırabilirsiniz.
Doğru bir nokta olabilir, ama bu sadece tokenization implementasyon ayrıntısı ve gerçek faydayla neredeyse hiç ilgili değil.
Bir kelimedeki harf sayısını saymak için LLM kullanmanız gereken durum neredeyse hiç yoktur.