Yapay zeka teknolojilerindeki hızlı gelişmeler, resmi doğrulama (formal verification) alanını ana akım haline getiriyor. Özellikle yapay zeka destekli mekanik ispat sistemleri geliştiren şirketler milyar dolarlık değerlemelerle yatırım alırken, Lean gibi ispat asistanlarına olan ilgi de benzeri görülmemiş bir hızla artıyor. Yapay zeka modelleri, Uluslararası Matematik Olimpiyatı (IMO), ICPC ve Putnam gibi dünyanın en zorlu yarışmalarında ve Erdös Problemleri gibi açık matematik problemlerinde şaşırtıcı sonuçlar elde ediyor. Terry Tao, Martin Kleppman ve Ilya Sergey gibi önde gelen araştırmacılar, yapay zeka destekli ispatların potansiyelinden büyük heyecan duyuyor.
Ancak resmi doğrulamanın önünde bazı karmaşık zorluklar bulunuyor. İlk ve teknik olarak çözülmesi en güç sorun, dünyadaki çoğu yazılımın resmi bir spesifikasyona sahip olmamasıdır. Resmi spesifikasyon, geliştirilen sistemin daha basit, matematiksel bir tanımıdır. Algoritmalar, veri yapıları, protokoller ve güvenlik açısından kritik sistemler genellikle resmi spesifikasyonlara sahipken, programların büyük çoğunluğunun informal spesifikasyonları bile yoktur. Bu durum, bir yazılım parçasını resmi olarak doğrulamayı çok zorlaştırır, çünkü neyin doğrulanacağı belirsizdir.
İkinci zorluk ise, sistemler hakkında teoremler için ispat yazma pratiği olan "ispat mühendisliğinin" (proof engineering) oldukça zor olmasıdır. İspatlar, matematiksel bir teorem ispatından programlama dili ispatına kadar çok farklı alanlara özgü unsurlar içerir. Geniş çapta öğretilen Software Foundations gibi kitaplar bile her bölümde farklı ispat stilleri sunar. Büyük Dil Modellerinin (LLM) programlamadaki yükselişi, bu iki noktayı da derinden etkiliyor. Yapay zeka destekli programlama, spesifikasyon odaklı geliştirmeye çok doğal bir uyum sağlıyor ve programlama yeteneklerinin sınırlarını "ne uygulayabilirsin"den "ne belirleyebilirsin" ve "ne doğrulayabilirsin"e doğru genişletiyor. Bu da yürütülebilir spesifikasyonlar yazmak için güçlü bir teşvik oluşturuyor.
Yapay zeka, yazılım geliştirmede sadece test etmenin ötesine geçerek, resmi doğrulama süreçlerini ana akım haline getiriyor ve daha güvenilir sistemlerin önünü açıyor.