“Anthropic” şirkəti süni intellekt modeli “Claude” vasitəsilə proqram təminatındakı gizli səhvlərin aşkarlanması istiqamətində genişmiqyaslı eksperiment keçirib. “Theorem” şirkətinin mütəxəssisləri ilə birgə 123 açıq kodlu kitabxana təhlil edilib və nəticədə yüzlərlə proqram qüsuru müəyyən olunub. Maraqlısı odur ki, bu səhvlərin bəziləri trilyonlarla avtomatlaşdırılmış testlərə baxmayaraq, illərlə sistemlərdə qalmağa davam edib.
Formal verifikasiya nə üçün vacibdir?
Tədqiqatın əsas yeniliyi “formal verifikasiya” metodunun tətbiqidir. Adi testlərdən fərqli olaraq, bu yanaşma proqramın müəyyən edilmiş tələblərə cavab verdiyini riyazi cəhətdən sübut etməyə imkan verir. “Google” şirkətinin “OSS-Fuzz” layihəsindən götürülən kitabxanalar üzərində aparılan sınaqlarda “Claude” mövcud testləri riyazi şərtlərə çevirərək, onların icrasını sübut edib.
Süni intellekt hansı problemləri aşkar edib?
Yoxlamalar RISC-V arxitekturasının maşın təlimatları səviyyəsində, yəni artıq kompilyasiya edilmiş proqramlar üzərində aparılıb. Bir neçə həftə ərzində sistem 123 kitabxana üçün 239 giriş nöqtəsində sübutlar hazırlayıb. Aşkar edilən problemlər arasında məlumatların emalı zamanı yaddaşın sərhədlərindən kənara çıxma halları və “libexpat” XML kitabxanasındakı məlum boşluqlar kimi kritik xətalar yer alıb.
Bu yanaşmanın gələcəyi nədir?
“Claude” təkcə səhvləri tapmaqla kifayətlənməyib, həm də onların düzəldilməsi üçün təkliflər irəli sürüb və yenilənmiş versiyalar üçün təkrar sübutlar hazırlayıb. Tədqiqatçılar vurğulayırlar ki, bu metod proqram təminatının etibarlılığını artırmaq üçün böyük potensiala malikdir. Gələcəkdə süni intellektin köməyi ilə kritik sistemlərdəki boşluqların daha sürətli və effektiv şəkildə aradan qaldırılması hədəflənir.
