70 milyon dolarlık tohum yatırımı alan &Truth, biçimsel doğrulamayı yapay zekâyla otomatikleştirmeyi hedefliyor

Biçimsel doğrulama otomasyonu geliştiren &Truth, 70 milyon dolar (yaklaşık 93,5 milyar won) tohum yatırımı aldığını açıkladı. Şirket, yapay zekâyı kendi teknolojisiyle birleştirerek yazılımın gereklilikleri karşıladığını kanıtlama sürecini kısaltmayı hedefliyor.

&Truth, 29 Ekim'de (yerel saatle) yayımladığı kuruluş duyurusunda gizlilik dönemini sona erdirerek faaliyetlerini kamuoyuna açtığını bildirdi. Yatırım, yapay zekâ güvenliği ve girişim sermayesi alanlarından isimlerin oluşturduğu bir gruptan geldi. Şirket, yatırımcıların adlarını ve değerlemesini açıklamadı.

ABD Ulusal Standartlar ve Teknoloji Enstitüsü (NIST), biçimsel doğrulamayı; gerekliliklerin resmî olarak tanımlandığı, uygulamanın matematiksel bir modelinin oluşturulduğu ve mantık kurallarıyla uygulamanın bu tanıma uygun olduğunun kanıtlandığı bir süreç olarak açıklıyor.

Standart yazılım testlerinde program seçilmiş girdilerle çalıştırılır ve sonuçlar incelenir. Biçimsel doğrulama ise tanımlanan koşulların karşılandığını kanıtlamaya çalışır.

Ancak bu kanıt yalnızca tanımın kapsadığı koşullar için geçerlidir. Kodun gereklilikleri karşıladığının gösterilmesi, bu gerekliliklerin gerçek kullanım ortamını ve kullanıcıların niyetini bütünüyle yansıttığı anlamına gelmez.

&Truth, kanıt oluşturma sürecinde yapay zekâ ve kendi otomasyon teknolojisini kullanacağını duyurdu. Şirket, birden fazla programlama dilinde kod doğrulamayı hedefliyor.

Şirket, yapay zekânın kanıt üretimini 100 kattan fazla hızlandırabileceğini, kendi teknolojisinin de buna ek olarak 100 kat hız sağlayabileceğini öne sürdü. Açıklamaya göre aylar veya yıllar sürebilen işler saatlere ya da dakikalara indirilebilir.

Bu hız artışları şirketin açıkladığı performans hedefleri. Kuruluş duyurusunda söz konusu rakamları bağımsız biçimde yeniden üreten bir değerlendirme sonucu yer almadı.

Anthropic, 22 Ekim'de Theorem ile yürüttüğü biçimsel doğrulama araştırmasının sonuçlarını yayımladı. Bu çalışma &Truth'un ürününü veya performansını değerlendirmedi; ayrı bir araştırma olarak yürütüldü.

Araştırmacılar, 123 açık kaynak kütüphanedeki 239 giriş noktası için girdiler 64 MB veya daha küçük olduğunda programların çökmeyeceğini kanıtladı.

Araştırma ekibi, kanıt sürecinde bulduğu kusurları düzelttikten sonra sonuçları doğruladı. Doğrulama, tek iş parçacıklı statik RISC-V ikili dosyaları ve araştırmacıların modellediği Linux ortamı gibi tanımlı koşullarla sınırlıydı.

Anthropic, sonucun kütüphanelerin tamamının hatasız olduğu anlamına gelmediğini belirtti. Kanıt doğrulayıcısı, sunulan kanıtın tanımla uyuşup uyuşmadığını kontrol ediyor; tanımın gerçek gereklilikleri ve ortamı eksiksiz yansıtıp yansıtmadığını değerlendirmiyor.

25 Ekim'de Reddit'in RISC-V topluluğunda yayımlanan bir gönderide, yapay zekânın yazdığı kanıtlara güvenmenin zor olduğunu savunan bir görüşle kanıt doğrulayıcılarının sonuçları değerlendirmek için ölçüt alınması gerektiğini söyleyen bir yanıt yer aldı. Gönderinin 23 olumlu oy alması, bu görüşleri sektörün geneline mal etmek için yeterli değil.

Biçimsel doğrulama, sanal varlık alanında da ayrı örneklerde kullanıldı. Zcash Ironwood'daki bakiye bütünlüğü doğrulaması 2.700'den fazla biçimsel doğrulama teoremi içeriyordu. Bu örnek, &Truth'un ürünü veya müşterileriyle bağlantılı olduğu anlamına gelmiyor.

&Truth birden fazla programlama dilinde kod doğrulamayı hedeflediğini açıkladı; ancak kuruluş duyurusunda akıllı sözleşmelere veya blokzincir koduna özel bir ürün ya da müşteri örneği sunmadı.