Robinhood CEO’su Tenev: Tüm Yazılım Kodu 2 Yıl İçinde Matematiksel Olarak Doğrulanacak

Robinhood CEO’su Vlad Tenev, yazılım dünyasında köklü bir değişim öngörüyor: Ona göre iki yıl içinde tüm kodlar yalnızca test edilmekle kalmayacak, matematiksel olarak da kanıtlanacak. Tenev’in X’teki bu çıkışı, hem yapay zekâ hem de yazılım güvenliği tartışmalarında yankı buldu. Ancak öngörünün ticari bir arka planı da var.

“Tüm kodlar iki yıl içinde doğrulanmış olacak”

Tenev, 4 Kasım’da X’te yaptığı paylaşımda “Tüm kodlar 2 yıl içinde biçimsel olarak doğrulanmış olacak” ifadesini kullandı. Sürecin önce güvenlik açısından kritik kodlarla başlayacağını, ardından diğer yazılımlara yayılacağını da ekledi. Biçimsel doğrulama, bir yazılımın belirli özelliklerinin olası tüm girdiler için geçerli olduğunu matematiksel yöntemlerle kanıtlama anlamına geliyor. Klasik testler ise yalnızca sınırlı sayıda senaryoyu deneyebiliyor.

Harmonic ve Aristotle devrede

Tenev, yapay zekâ girişimi Harmonic’in kurucu ortağı ve yönetim kurulu icra başkanı. Şirket, 27 Ekim’de Aristotle sisteminin C yazılımlarını ve Verilog donanım tasarımlarını doğrulayabildiğini duyurdu. Harmonic’in aktardığına göre sistem, C kodunda işlevsel doğruluğu ve belirli tanımsız davranış sınıflarının bulunmadığını denetleyebiliyor. Şirket 3 Kasım’da da Ibex RISC-V işlemcisinin çarpma ve bölme komutlarının doğrulanmasına dair teknik bir yazı yayımladı. Sequoia ve Ribbit Capital destekli Harmonic, geçen yıl 1,45 milyar dolar değerlemeyle 120 milyon dolar yatırım almıştı.

Öngörünün sınırları

Crypto Briefing, okurların Tenev’in tahminini Harmonic’in doğrulama hizmeti sattığı bilgisiyle birlikte değerlendirebileceğini vurguladı. Harmonic’in kendi kullanım koşulları da sınırları açıkça belirtiyor: “doğrulanmış” bir sonuç yalnızca kullanılan şartname, model ve varsayımlar için geçerli ve bağımsız inceleme yine de gerekebiliyor. Yani matematiksel kanıt, hatasız yazılım anlamına gelmiyor. Yine de yapay zekânın kod yazmanın yanında kodu kanıtlama işine de girmesi, sektörün yeni gündem maddelerinden biri olmaya aday.