Anthropic-ը Claude-ի միջոցով ապացուցել է 123 գրադարանների անվտանգությունը

Anthropic-ը հայտնում է, որ իր Claude մոդելը գրել է մեքենայական ստուգման ենթարկված մաթեմատիկական ապացույցներ, որոնք ցույց են տալիս, որ 123 բաց կոդով գրադարաններից ստացված կոմպիլացված կոդը չի կարող խափանվել սահմանված պայմաններում: Ըստ հոկտեմբերի 22-ին հրապարակված հետազոտության, մոդելը նաև հայտնաբերել է սխալներ, որոնք տարիներ շարունակ աննկատ էին մնացել՝ չնայած տրիլիոնավոր թեստային գործարկումներին: Հետազոտությունը իրականացվել է ընկերության Frontier Red Team-ի կողմից՝ ֆորմալ մեթոդների մասնագիտացված Theorem ընկերության հետ համատեղ.anthropic.com

Ընկերությունն այն անվանում է "առաջին լայնածավալ փորձը՝ օգտագործելու արհեստական բանականությունը արտադրական ծրագրային ապահովման մեջ ֆորմալ վերիֆիկացիա կիրառելու համար՝ ասեմբլերի կոդի մակարդակում": Anthropic-ը նշում է, որ ԱԲ-ն այժմ կարող է հեշտությամբ գտնել և օգտագործել սխալներ, ուստի միայն թեստավորումն այլևս բավարար չէ ծրագրային ապահովումը պաշտպանելու համար.anthropic.com

Fuzz-թեստերից մինչև ապացույցներ

Թիմը սկսել է Google-ի OSS-Fuzz ծրագրի fuzz-թեստերից և յուրաքանչյուրը վերածել է ֆորմալ բնութագրի: Կանոնն այն էր, որ թեստը չպետք է խափանվի 64 ՄԲ-ից փոքր ցանկացած մուտքային տվյալի դեպքում, երբ այն կոմպիլացվում է RISC-V մեքենայական կոդի: Մի քանի շաբաթվա ընթացքում Claude-ը դա ապացուցել է 123 գրադարանների 239 մուտքային կետերի համար: Ապացույցները կազմում են մոտ 180 միլիոն տող Rocq ապացույցների լեզվով, և մեկ տիպիկ ապացույցը կազմում է մոտ 600,000 տող, ըստ Anthropic-ի: Rocq ապացույցների ստուգիչը հաստատում է, որ յուրաքանչյուր ապացույց համապատասխանում է իր բնութագրին, ուստի մշակողները կարիք չունեն ստուգելու գեներացված կոդը տող առ տող, հայտնում է Interesting Engineering-ը.interestingengineering.com+1

Anthropic-ը հայտնել է, որ ապացույցների մի մասը հրապարակվում է՝ դրանց հիմքում ընկած RISC-V և Linux սեմանտիկայի հետ միասին: Unite.AI-ի հաղորդմամբ՝ Theorem-ը առաջարկում է անվճար իրականացնել նույն գործընթացը որակավորված բաց կոդով նախագծերի համար իր OSS Verify ծրագրի շրջանակներում: Theorem-ը նաև թողարկել է Claude-ի հմտություն, որը օգնում է մշակողներին գրանցվել.unite.ai+1

Fuzzers-ի կողմից բաց թողնված սխալներ

Ապացույցների գրումը բացահայտել է հարյուրավոր սխալներ, որոնք Claude-ը շտկել է նախքան ուղղված կոդը ապացուցելը: Դեկոմպրեսորում այն հայտնաբերել է հաշվիչի թերություն, որը հանգեցրել է սահմաններից դուրս գրման, բայց միայն մոտ 20 ՄԲ մուտքային տվյալների և մեկ հազվադեպ դասավորության դեպքում: Պատկերի դեկոդերում սահմաններից դուրս ընթերցման մեկ այլ սխալ պահանջում էր 64 ՄԲ մուտքային տվյալ և 2 ԳԲ-ից ավելի հիշողություն: Հետազոտության համաձայն՝ Claude-ը նաև վերահայտնաբերել է libexpat-ում հայտնի խոցելիություն և գտել է տրամաբանական թերություն, որտեղ ֆունկցիան, որը պետք է սահմանափակի, թե որ ֆայլերը կարող է բեռնել հավելվածը, միշտ չէ, որ կիրառվել է.anthropic.com

Երաշխիքի սահմանափակումները

Anthropic-ը զգուշացրել է, որ ապացույցները չեն նշանակում, որ գրադարանները զերծ են սխալներից: Դրանք ենթադրում են մեկ հոսքային ստատիկ բինար ֆայլ՝ ֆիքսված հիշողության բյուջեով, որն աշխատում է RISC-V պրոցեսորի վրա Linux-ի ներքո: Մնացած սխալները կամ ապացույցների շրջանակից դուրս են, կամ գտնվում են վստահելի բաղադրիչներում, ինչպիսիք են սարքավորումը, օպերացիոն համակարգի մոդելները, թեորեմների հայտարարությունները և հենց Rocq ստուգիչը: Interesting Engineering-ը նշում է, որ տեղակայված համակարգերի մեծ մասն օգտագործում է այլ պրոցեսորային ճարտարապետություններ կամ կոնֆիգուրացիաներ.interestingengineering.com+1

Anthropic-ը դեռ կարծում է, որ տնտեսական իրավիճակը փոխվում է: "Մենք խրախուսում ենք բոլոր մշակողներին ուսումնասիրել ֆորմալ վերիֆիկացիան LLM-ների միջոցով, հատկապես նրանց, ովքեր նախկինում փորձել են դա ավելի քիչ կարողություններ ունեցող մոդելներով և արդյունքի չեն հասել," — գրել է թիմը.anthropic.com