Massachusetts Amherst Üniversitesi liderliğindeki bir bilgisayar bilimci ekibi, kısa süre önce, yazılım hatalarını önlemek ve temel kodun doğru olduğunu doğrulamak için kullanılabilecek tüm kanıtları otomatik olarak oluşturmaya yönelik yeni bir yöntemi duyurdu.
Baldur adı verilen bu yeni yöntem, Yüksek Lisans’ların yapay zeka gücünden yararlanıyor ve Thor aracıyla birleştirildiğinde yaklaşık %66 verimlilik sağlıyor.
“Yazılım hatalarının günümüz toplumu üzerinde derin bir etkisi var. Bunlar, iş yapmaya çalıştığımızda veya rahatlamaya çalışırken film izleme uygulamalarımızı çökerttiğimizde ortaya çıkan can sıkıcı ama önemsiz hatalardan, tıbbi cihazları saldırılara karşı duyarlı hale getiren veya bilgisayar korsanlarının kişisel bilgileri çalmasına izin veren güvenlik açıklarına kadar uzanır. UMass Amherst’teki Manning Bilgi ve Bilgisayar Bilimleri Fakültesi profesörü ve makalenin kıdemli yazarı Yuriy Brun, Help Net Security’ye şunları söyledi: “Ekonomik büyümede milyarlarca dolarlık hasara neden oluyor.”
“Yazılımdaki hataları azaltmak, hatta hatasız yazılım üretmek, onlarca yıldır sistem geliştirmenin kutsal kâsesi olmuştur, ancak ne yazık ki toplumumuzdaki uygulama şu ki, tüm yazılımların hatalara sahip olmasını bekliyoruz. Hatasız yazılım oluşturmak inanılmaz derecede zor bir iştir.”
Hatalı yazılımın geniş erişimini anlamak
Hatalı yazılımların etkileri, can sıkıcı biçimlendirme veya ani çökmelerden, potansiyel olarak yıkıcı güvenlik ihlallerine veya uzay araştırmaları veya sağlık bakım cihazlarını kontrol etmek için kullanılan hassas yazılımlara kadar her yerde değişebilir.
Elbette, yazılım var olduğundan beri kontrol etmenin yöntemleri de vardı. Popüler yöntemlerden biri en basitidir: 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ün olağanüstü derecede zaman alıcı, pahalı olması 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ıdır 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 ünlü örneği olduğu Yüksek Lisans’ın yükselişiyle birlikte, olası bir çözüm bu tür kanıtları otomatik olarak oluşturmaya çalışmaktır. Ancak Brun, “LLM’lerdeki en büyük zorluklardan biri her zaman doğru olmamalarıdır” diyor. “Çökmek ve bir şeylerin yanlış olduğunu size 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ı.
Baldur’un gücü
Baldur’un inşası birkaç ay sürdü. Çalışma, Google ile ortaklaşa yapıldı ve önemli miktarda önceki araştırmanın üzerine inşa edildi.
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 bilimsel makaleler ve matematiksel 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ğlar. Otomatik olarak kanıt oluşturmaya yönelik araca Thor denir ve bu araç, %57 oranında kanıt üretebilir. 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 yoldur ve yapay zekanın yetenekleri giderek genişletilip iyileştirildikçe Baldur’un etkinliği de artmalıdır.
“Resmi doğrulama, hatasız yazılım oluşturmak için çok umut verici bir yöntemdir. Mühendisler hala yazılım sistemini oluşturuyorlar, ancak bununla birlikte yazılımın doğru olduğuna dair matematiksel kanıtlar da oluşturuyorlar. Bu kanıtların yazılması oldukça zordur, ancak bu süreci destekleyen, özel diller ve teorem kanıtlayıcıları da dahil olmak üzere çok sayıda araç vardır; bunlar daha sonra kanıtı alır ve yazılımın doğru olduğunu doğrulamak için yazılımla makine kontrolüne tabi tutulur,” yorumunu yaptı Brun.
“Çalışmamız bu kanıtların yazımını otomatikleştirmeye odaklanıyor. Baldur, bir matematik teoremi verildiğinde, o teoremin kanıtlayıcısının daha sonra doğrulayabileceği bir kanıtını otomatik olarak oluşturmak için büyük dil modellerini kullanıyor. Karşılaştırmalı değerlendirmelerden biri olan yöntemimiz, önceki yöntemlerle birleştirildiğinde, kanıtları %65,7 oranında tam otomatik olarak üretir; bu oldukça umut vericidir ve mühendislere bu kanıtları yazarken önemli miktarda manuel çaba tasarrufu sağlayacaktır,” diye bitirdi Brun.
Ekipte First ve Brun’un yanı sıra o dönemde Google’da çalışan Markus Rabe ve Illinois Üniversitesi – Urbana Champaign’de yardımcı doçent olan Talia Ringer da yer alıyor. Bu çalışma Google’da gerçekleştirildi ve Savunma İleri Araştırma Projeleri Ajansı ve Ulusal Bilim Vakfı tarafından desteklendi.