სტენფორდის უნივერსიტეტის მკვლევარმა ჩუიუ სუნმა შეიმუშავა AI ინსტრუმენტი, რომელმაც საინჟინრო პროექტი ნახევარ დღეზე ნაკლებ დროში და 500 დოლარზე ნაკლებ ფასად დაასრულა. შედარებისთვის, იგივე სამუშაოს სამი მაღალკვალიფიციური ექსპერტი ხუთი თვის განმავლობაში ასრულებდა. ეს შედეგი ყურადღებას ამახვილებს ფორმალური ვერიფიკაციის სფეროზე, რომელიც პროგრამული უზრუნველყოფის მათემატიკური მეთოდებით შემოწმებას გულისხმობს.
ათწლეულების განმავლობაში, დეველოპერები ცდილობდნენ მათემატიკის გამოყენებით დაემტკიცებინათ, რომ მათი კოდი შეცდომებისგან თავისუფალია. ეს პროცესი შრომატევადია და მოითხოვს კოდის ფორმულებად გარდაქმნას. ახლა სტარტაპების ტალღა, მათ შორის &Truth და Harmonic, ფსონს დებს იმაზე, რომ გენერაციული AI ამ პროცესს პრაქტიკულსა და აუცილებელს გახდის.
მიუხედავად პერსპექტივებისა, ტექნოლოგია ჯერ კიდევ პროტოტიპირების ეტაპზეა. ექსპერტები, მათ შორის Antithesis-ის დამფუძნებელი უილ უილსონი, აფრთხილებენ ბაზარს, რომ ფორმალური ვერიფიკაცია არ არის უნივერსალური გადაწყვეტა. უილსონის თქმით, ეს პროცესი რთულია და მხოლოდ ამომწურავ ტესტირებას შეუძლია სრული გარანტიის მიცემა. ეთერიუმის შემქმნელი ვიტალიკ ბუტერინიც აღნიშნავს, რომ ეს მეთოდი არ არის პანაცეა, თუმცა ის მნიშვნელოვანი თავდაცვა იქნება AI-ს მიერ განხორციელებული კიბერშეტევების წინააღმდეგ.
ამჟამად ფორმალური ვერიფიკაცია ძირითადად კრიტიკულ სისტემებში გამოიყენება, როგორიცაა Apple-ის ან Amazon-ის სერვერები. თუმცა, ბევრი კომპანია თავს იკავებს მისი ფართო დანერგვისგან მაღალი ხარჯებისა და ინოვაციების შენელების შიშის გამო. მიუხედავად ამისა, კიბერუსაფრთხოების სფეროს წარმომადგენლები მიიჩნევენ, რომ AI-ს დახმარებით ავტომატიზებული ვერიფიკაცია მომავალში შესაძლოა სტანდარტად იქცეს, რაც პროგრამულ უზრუნველყოფას უფრო საიმედოს გახდის.
წყარო: wired.com
