Anthropic-მა Claude-ის დახმარებით 123 ბიბლიოთეკის უსაფრთხოება დაადასტურა

Anthropic-ის განცხადებით, მისმა მოდელმა Claude-მა დაწერა მანქანურად შემოწმებული მათემატიკური მტკიცებულებები, რომლებიც ადასტურებს, რომ 123 ღია კოდის ბიბლიოთეკიდან მიღებული კომპილირებული კოდი განსაზღვრულ პირობებში არ იწვევს კრახს. კომპანიის Frontier Red Team-ის მიერ 22 ოქტომბერს გამოქვეყნებული კვლევის თანახმად, მოდელმა პროცესის მიმდინარეობისას აღმოაჩინა შეცდომები, რომლებიც ტრილიონობით ტესტის მიუხედავად, წლების განმავლობაში შეუმჩნეველი რჩებოდა. კვლევა ჩატარდა ფორმალური მეთოდების ფირმა Theorem-თან ერთად.anthropic.com

კომპანია ამას უწოდებს "პირველ ფართომასშტაბიან მცდელობას, გამოიყენოს ხელოვნური ინტელექტი ფორმალური ვერიფიკაციისთვის საწარმოო პროგრამულ უზრუნველყოფაში, ასამბლეის კოდის დონეზე". Anthropic-ის თქმით, ხელოვნურ ინტელექტს უკვე შეუძლია შეცდომების მარტივად პოვნა და გამოყენება, ამიტომ მხოლოდ ტესტირება პროგრამული უზრუნველყოფის დასაცავად საკმარისი აღარ არის.anthropic.com

ფაზ-ტესტებიდან მტკიცებულებებამდე

გუნდმა მუშაობა დაიწყო Google-ის OSS-Fuzz პროგრამის ფაზ-ტესტებით და თითოეული მათგანი ფორმალურ სპეციფიკაციად აქცია. წესი მდგომარეობდა იმაში, რომ ტესტი არ უნდა ჩავარდნილიყო 64 მბ-ზე მცირე ზომის ნებისმიერ მონაცემზე, როდესაც ის კომპილირდება RISC-V მანქანურ კოდში. რამდენიმე კვირის განმავლობაში Claude-მა ეს დაამტკიცა 123 ბიბლიოთეკის 239 საწყისი წერტილისთვის. მტკიცებულებები ჯამში Rocq-ის ენაზე დაახლოებით 180 მილიონ სტრიქონს შეადგენს, ხოლო ერთი ტიპური მტკიცებულება დაახლოებით 600 000 სტრიქონია. როგორც Interesting Engineering იტყობინება, Rocq-ის შემმოწმებელი ადასტურებს, რომ თითოეული მტკიცებულება შეესაბამება მის სპეციფიკაციას, ამიტომ დეველოპერებს არ სჭირდებათ გენერირებული კოდის სტრიქონ-სტრიქონ გადამოწმება.interestingengineering.com+1

Anthropic-ის თქმით, მტკიცებულებების ნაწილი ქვეყნდება RISC-V და Linux სემანტიკასთან ერთად. Unite.AI-ის ცნობით, Theorem სთავაზობს უფასო მომსახურებას კვალიფიციური ღია კოდის პროექტებისთვის თავისი OSS Verify პროგრამის ფარგლებში. Theorem-მა ასევე გამოუშვა Claude-ის სპეციალური უნარი, რომელიც პროექტის მფლობელებს რეგისტრაციაში ეხმარება.unite.ai+1

შეცდომები, რომლებიც ფაზერებმა ვერ შენიშნეს

მტკიცებულებების წერამ ასობით შეცდომა გამოავლინა, რომლებიც Claude-მა გამოასწორა კოდის დამტკიცებამდე. დეკომპრესორში მან აღმოაჩინა მრიცხველის ნაკლებობა, რაც იწვევდა საზღვრებს გარეთ ჩაწერას, თუმცა მხოლოდ 20 მბ-მდე მონაცემებზე და ერთ იშვიათ განლაგებაზე. გამოსახულების დეკოდერში აღმოჩენილ სხვა შეცდომას, რომელიც საზღვრებს გარეთ კითხვას უკავშირდება, ესაჭიროებოდა 64 მბ მონაცემი და 2 გბ-ზე მეტი მეხსიერება. კვლევის თანახმად, Claude-მა ასევე ხელახლა აღმოაჩინა libexpat-ში არსებული ცნობილი მოწყვლადობა და ლოგიკური ხარვეზი, სადაც ფუნქცია, რომელიც უნდა ზღუდავდეს აპლიკაციის მიერ ჩასატვირთ ფაილებს, ყოველთვის არ იყო აღსრულებული.anthropic.com

გარანტიის შეზღუდვები

Anthropic-მა გააფრთხილა, რომ ეს მტკიცებულებები არ ნიშნავს, რომ ბიბლიოთეკები სრულად არის დაცული შეცდომებისგან. ისინი ეფუძნება ერთნაკადიან სტატიკურ ბინარულ ფაილს ფიქსირებული მეხსიერების ბიუჯეტით, რომელიც მუშაობს RISC-V პროცესორზე Linux-ის გარემოში. დარჩენილი შეცდომები ან მტკიცებულებების ფარგლებს გარეთაა, ან სანდო კომპონენტებშია, როგორიცაა აპარატურა, ოპერაციული სისტემის მოდელები, თეორემების განცხადებები და თავად Rocq-ის შემმოწმებელი. Interesting Engineering აღნიშნავს, რომ დანერგილი სისტემების უმეტესობა იყენებს სხვა პროცესორულ არქიტექტურებს ან კონფიგურაციებს.interestingengineering.com+1

Anthropic მაინც მიიჩნევს, რომ ეკონომიკური გარემო იცვლება. "ჩვენ მოვუწოდებთ ყველა დეველოპერს, შეისწავლონ ფორმალური ვერიფიკაცია LLM-ების გამოყენებით, განსაკუთრებით მათ, ვინც ადრე სცადა ეს ნაკლებად მძლავრი მოდელებით და შედეგი ვერ მიიღო," – წერს გუნდი.anthropic.com