Ethereum kurucularından Vitalik Buterin, yapay zekanın ürettiği ispatların insan tarafından anlaşılmasını kolaylaştırmak amacıyla yeni bir programlama dili önerdi. Bu dil, doğrudan Lean veya HOL gibi formal ispat asistanlarına derlenecek şekilde tasarlanıyor. Amaç, matematiksel doğruluğun tek koşul olduğu, okunabilir tanımlar ve teoremlerin öne çıktığı bir yapı oluşturmak.

Buterin, bu konuyu daha önce de bir blog yazısında ele almıştı. Formel olarak doğrulanmış kodun, güvenlik araştırmalarında yapay zeka destekli saldırılara karşı önemli bir savunma mekanizması oluşturduğu belirtiliyor. Yeni dil, geliştiricilerin ispatın tamamına gömülmeden doğrudan iddiaları denetlemesini sağlayacak.

Buterin, bu yaklaşımları kamusal alanda test etmeye devam ediyor. Anonim bir billboard demosu ile denetlenebilir ispatların teorik alanlardan gerçek ürünlere nasıl aktarılabileceğini gösterdi. Araştırmacılar, Lean kullanarak konsensüs client’larını da formel olarak doğrulamaya başladı. Yeni dilin henüz prototipi yok ve sözdizimi açık bırakılmış durumda. Yapay zeka ile doğrulanmış kodun gerçek üretim için devreye alınma hızını bu seçimin belirleyeceği düşünülüyor.