İlk dəfə: &Truth və Harmonic süni intellektlə formal doğrulamada inqilab yaradır

Formal doğrulama və süni intellektin yeni üfüqləri

Proqram təminatının etibarlılığını təmin edən formal doğrulama prosesi ənənəvi olaraq uzun və zəhmətli olurdu. Lakin bu il Stanford tədqiqatçısı Chuyue Sun və həmkarları süni intellektdən istifadə edərək mühəndislik layihəsini yarım gündən az müddətdə, 500 dollardan az (təxminən 850 AZN) xərclə tamamladılar. Bu, formal doğrulama sahəsində sürətli və sərfəli dönüşün mümkünlüyünü göstərdi.

&Truth və Harmonic startaplarının yüksəlişi

Avqust ayında yaranan &Truth startapı formal doğrulama prosesini avtomatlaşdırmaq məqsədilə 70 milyon dollar (təxminən 119 milyon AZN) investisiya cəlb etdi. Harmonic startapı isə 295 milyon dollar (təxminən 502 milyon AZN) maliyyələşmə aldı. Harmonic-in AI agenti Aristotle C proqramlaşdırma dilində və Verilog hardware dizaynında proqramları doğrulayır. Nvidia-nın sərmayə bölməsi də bu layihəyə dəstək verir.

Formal doğrulamanın praktiki tətbiqləri

Apple "corecrypto" kitabxanasındakı problemləri formal doğrulama vasitəsilə aşkar edib. Amazon Web Services isə bu texnologiyanın bulud təhlükəsizliyini artırdığını və böyük səhvlərin erkən mərhələdə aradan qaldırılmasına kömək etdiyini vurğulayır. Lakin bir çox orta səviyyəli texnologiya şirkətləri mühəndis çatışmazlığı, yüksək xərclər və formal doğrulamanın uzun müddət tələb etməsi səbəbindən bu prosesi geniş tətbiq etmirlər.

AI ilə formal doğrulamanın gələcəyi və çağırışlar

Anthropic və Theorem startapları AI-dan istifadə edərək açıq mənbə proqramlarda səhvləri aşkar edir və Claude üçün əlavə alətlər təqdim edirlər. Formal doğrulama hələ prototip mərhələsindədir və geniş yayılması sual altındadır. Müştərilərin texnologiyanı necə qəbul edəcəyi və ödəniş məsələləri hələ tam aydın deyil.

Ekspertlərin fikirləri və insan təsiri

Proofcraft şirkətinin rəhbərləri formal doğrulama sahəsinə marağın artdığını bildirir. Microsoft Research-dən ayrılan Madan Musuvathi Truidic startapını quraraq bu sahədə innovasiyaları davam etdirir. Formal doğrulama proqram təminatının etibarlılığını artırmaqla, təhlükəsiz və dayanıqlı sistemlərin yaradılmasına xidmət edir. Bu isə insanların gündəlik həyatında daha az təhlükə və daha çox etibar deməkdir.

Süni intellektin formal doğrulama ilə birləşməsi texnologiya dünyasında yeni bir səhifə açır. Bu, həm mühəndislər, həm də istifadəçilər üçün daha sürətli, sərfəli və etibarlı proqram təminatı vəd edir.