ეს გარანტია მხოლოდ კონკრეტულ ტექნიკურ პირობებში მოქმედებს და პროგრამებს ყველა შესაძლო ხარვეზისგან სრულად არ აზღვევს.
Anthropic-ის უსაფრთხოების გუნდმა, Frontier Red Team-მა, კომპანია Theorem-თან ერთად 22 ოქტომბერს ახალი კვლევა გამოაქვეყნა. დოკუმენტის მიხედვით, ხელოვნური ინტელექტის მოდელმა Claude-მა მათემატიკურად დაამტკიცა, რომ 123 პოპულარული ღია კოდის ბიბლიოთეკა შემოწმებულ პირობებში მუშაობისას არ გაითიშება. მოდელმა ასევე იპოვა და გაასწორა ძველი ხარვეზები, რომლებიც წლების განმავლობაში მიმდინარე ტესტირებებს გამორჩა. ეს ბიბლიოთეკები Google-ის პროექტ OSS-Fuzz-იდან შეირჩა.
როგორ მუშაობს ფორმალური ვერიფიკაცია
ჩვეულებრივი ტესტირების დროს პროგრამას უამრავ სხვადასხვა მონაცემს აწვდიან და ამოწმებენ, ხომ არ გაითიშება ის. პრობლემა ის არის, რომ ყველა შესაძლო ვარიანტის სათითაოდ მოსინჯვა შეუძლებელია. ფორმალური ვერიფიკაცია სხვანაირად მუშაობს. ის სკოლის მათემატიკური თეორემის დამტკიცებას ჰგავს და ლოგიკურად აჩვენებს, რომ შეცდომა არცერთ შემთხვევაში არ მოხდება. ადრე ასეთი მტკიცებულების დაწერას ექსპერტები წლებს ანდომებდნენ, ამიტომ ამ მეთოდს თითქმის არავინ იყენებდა.
რამდენად რთულია ასეთი შემოწმება? წარმოიდგინეთ, რომ ერთი ჩვეულებრივი პროგრამის უსაფრთხოების დასაბუთებას Rocq-ის სისტემაში დაახლოებით 600 000 ხაზი მტკიცებულების კოდი სჭირდება. Claude-მა ეს სამუშაო სულ რამდენიმე კვირაში შეასრულა. მან არა მხოლოდ საწყისი კოდი, არამედ უკვე კომპილირებული, ანუ უშუალოდ პროცესორისთვის გასაგები RISC-V ასემბლერის კოდიც შეამოწმა. Anthropic-ის ცნობით, ეს პირველი შემთხვევაა, როცა AI-მ რეალური პროგრამები ასემბლერის დონეზე ასეთი მასშტაბით გადაამოწმა. პროცესში მოდელმა ისეთი შეცდომებიც აღმოაჩინა, რომლებიც „ტრილიონობით სატესტო გაშვების“ მიუხედავად, წლების განმავლობაში შეუმჩნეველი რჩებოდა.
მკვლევრებმა მეორე ექსპერიმენტიც ჩაატარეს. Claude-მა პროგრამირების ენა Rust-ზე ააწყო Python-ის ინტერპრეტატორი, ანუ პროგრამა, რომელიც Python-ის კოდს კითხულობს და ასრულებს, და მისი გამართულობა მათემატიკურად დაასაბუთა. როცა კოდში სპეციალურად ჩასვეს ხარვეზები, შემთხვევითმა ტესტებმა მათი მხოლოდ მცირე ნაწილი იპოვა, მათემატიკურმა მტკიცებულებამ კი ყველა მათგანი გამოავლინა.
სად გადის შესაძლებლობების ზღვარი
მიღებული გარანტიები მხოლოდ მკაცრად განსაზღვრულ პირობებში მოქმედებს. მტკიცებულება ითვალისწინებს, რომ პროგრამა მუშაობს ერთ ნაკადად, აქვს ფიქსირებული მეხსიერება და გაშვებულია RISC-V-ის პროცესორსა და Linux-ის სისტემაზე. გარდა ამისა, თავად RISC-V-ისა და Linux-ის მოდელებიც უშეცდომო უნდა იყოს. ეს იმას ნიშნავს, რომ შემოწმებული ბიბლიოთეკები ყველა სახის ხარვეზისგან სრულად დაცული მაინც არ არის.
Anthropic-მა მტკიცებულებების ნაწილი უკვე გაასაჯაროვა, რათა სხვებმაც შეძლონ მათი გადამოწმება და გამოყენება. პარტნიორი კომპანია Theorem-ი კი სხვა ღია პროექტებსაც სთავაზობს იმავე სისტემით შემოწმებას და დეველოპერებისთვის Claude-ის სპეციალურ უნარს აქვეყნებს. დღეს ხელოვნურ ინტელექტს პროგრამული სისუსტეების პოვნა და ჰაკერული თავდასხმებისთვის გამოყენება მარტივად შეუძლია. სწორედ ამიტომ სისტემების დამცველებს ახლა უბრალო ტესტებზე მეტად მათემატიკური სიზუსტე სჭირდებათ.
| შემოწმებული ბიბლიოთეკები | 123 ღია კოდის ბიბლიოთეკა (Google OSS-Fuzz) |
| შესასვლელი წერტილები | 239 (entry points) |
| შემოწმებული მონაცემების ზომა | ნებისმიერი შემავალი მონაცემი 64 MB-მდე |
| მტკიცებულებების საერთო მოცულობა | დაახლოებით 180 მილიონი ხაზი Rocq-ის სისტემაში |
| ერთი ტიპური მტკიცებულება | დაახლოებით 600 000 ხაზი |
| პროგრამების მედიანური ზომა | 18 000 RISC-V-ის ინსტრუქცია |
| სულ დაწერილი კოდი მცდელობებისას | დაახლოებით 1 მილიარდი ხაზი |
| Rust-ის ექსპერიმენტის შედეგი | მტკიცებულებამ იპოვა 7-იდან 7 ხელოვნური ხარვეზი, ტესტებმა კი მხოლოდ 2 |
წყარო: Anthropic: LLMs are making formal software verification feasible at a much larger scale | Anthropic: technical appendix (PDF) | Interesting Engineering | Unite.AI
ეს სტატია შეიქმნა AI ხელსაწყოებით, პროცესში ადამიანის ჩართულობა დაახლოებით 10%-ია.
