Baldur adı verilen bu yeni yöntem, Büyük Dil Modellerinin (LLM’ler) yapay zeka gücünden yararlanıyor ve son teknoloji ürünü Thor aracıyla birleştirildiğinde yaklaşık %66 oranında benzeri görülmemiş bir verimlilik sağlıyor. Ekip yakın zamanda ACM Ortak Avrupa Yazılım Mühendisliği Konferansı ve Yazılım Mühendisliğinin Temelleri Sempozyumu’nda çok beğenilen Seçkin Makale ödülüne layık görüldü.
UMass Amherst Manning Bilgi ve Bilgisayar Bilimleri Fakültesi profesörü ve gazetenin kıdemli yazarı Yuriy Brun, “Ne yazık ki yazılımımızın her yerde olmasına ve onu her gün kullanmamıza rağmen hatalı olmasını beklemeye başladık.” diyor.
Chevrolet iletişim yöneticisi Chad Lyons, yaptığı açıklamada şunları söyledi: “Ekibimiz bir düzeltmeyi uygulamaya koymak için hızlı bir şekilde çalışıyor ve güncellemelerini nasıl planlayacakları konusunda daha fazla bilgi için sahiplerle iletişime…
Hatalı yazılımların etkileri, can sıkıcı biçimlendirme veya ani çökmelerden; güvenlik ihlalleri, uzay araştırmaları ve sağlık bakım cihazlarını kontrol etmek için kullanılan hassas yazılımlar söz konusu olduğunda potansiyel olarak felakete kadar gidebilir.
Elbette, yazılım var olduğundan beri kontrol etmenin de yöntemleri var. Popüler yöntemlerden biri en basiti: Bir insanın kodu satır satır okutarak hiçbir hata olmadığını manuel olarak doğrulamasını sağlarsınız. Veya kodu çalıştırıp yapmasını beklediğiniz şeyle karşılaştırabilirsiniz. Örneğin, kelime işlemci yazılımınızın “geri dön” tuşuna her bastığınızda satırı kırmasını bekliyorsanız ancak bunun yerine soru işareti çıkıyorsa, o zaman kodda bir şeylerin yanlış olduğunu biliyorsunuz demektir.
Her iki yöntemin de sorunu, bunların insan hatasına açık olması ve olası her aksaklığa karşı kontrol yapılmasının olağanüstü derecede zaman alıcı, pahalı ve önemsiz sistemler dışında herhangi bir şey için mümkün olmamasıdır.
Çok daha kapsamlı ama daha zor bir yöntem, kodun yapması beklenen şeyi yaptığını gösteren matematiksel bir kanıt oluşturmak ve ardından kanıtın da doğru olduğundan emin olmak için bir teorem kanıtlayıcı kullanmaktır. Bu yönteme makine kontrolü denir.
Ancak bu kanıtların manuel olarak yazılması inanılmaz derecede zaman alıcı ve kapsamlı uzmanlık gerektirir. UMass Amherst’teki doktora tezinin bir parçası olarak bu araştırmayı tamamlayan makalenin baş yazarı Emily First, “Bu kanıtlar yazılım kodunun kendisinden çok daha uzun olabilir.” diyor.
ChatGPT’nin en sık kullanıldığı yerlerden Yüksek Lisans’ın yükselişiyle birlikte, olası bir çözüm bu tür kanıtları otomatik olarak oluşturmaya çalışmak. Ancak Brun, “LLM’lerdeki en büyük zorluklardan biri her zaman doğru olmamalarıdır.” diyor. “Çöküp size bir şeylerin yanlış olduğunu bildirmek yerine, ‘sessizce başarısızlığa’ eğilimli oluyorlar, yanlış bir cevap üretip bunu doğruymuş gibi sunuyorlar. Ve çoğu zaman yapabileceğiniz en kötü şey sessizce başarısız olmaktır.” Baldur’un devreye girdiği yer burası.
Ekibi Google’da çalışmalarını yürüten First, büyük bir doğal dil metni külliyatı üzerinde eğitim almış bir LLM olan Minerva’yı kullandı ve ardından 118 GB’lık matematiksel makaleler ve ifadeler içeren web sayfalarında ince ayar yaptı. Daha sonra, matematiksel kanıtların yazıldığı Isabelle/HOL adlı bir dil üzerinde LLM’ye daha da ince ayar yaptı.
Baldur daha sonra tam bir kanıt oluşturdu ve çalışmasını kontrol etmek için teorem kanıtlayıcıyla birlikte çalıştı. Teorem kanıtlayıcı bir hata yakaladığında, hatayla ilgili bilgilerin yanı sıra kanıtı da Yüksek Lisans’a geri gönderdi, böylece hatasından ders alıp yeni ve hatasız bir kanıt üretebilir.
Bu işlem doğrulukta dikkate değer bir artış sağlıyor. Otomatik olarak kanıt oluşturmaya yönelik son teknoloji ürünü araca Thor deniyor ve bu araç, %57 oranında kanıt üretebiliyor. Baldur (İskandinav mitolojisine göre Thor’un kardeşi) Thor ile eşleştirildiğinde, ikisi %65,7 oranında kanıt üretebilir.
Hala büyük oranda hata olmasına rağmen Baldur, yazılımın doğruluğunu doğrulamak için şimdiye kadar tasarlanmış en etkili ve verimli yol; yapay zekanın yetenekleri giderek genişletilip iyileştirildikçe Baldur’un etkinliği de artmalı.
Ekipte First ve Brun’un yanı sıra o sırada Google’da çalışan Markus Rabe ve Talia Ringer da yer alıyor.
