Bend. լեզու, որն արգելափակում է AI-ի սխալները ապացույցով

Bend-ը ներկայացվում է մեկ տողով. արագ լեզու, որն արգելափակում է AI-ի սխալները ապացույցով և միավորում է C-ի արագությունը, CUDA-ի զուգահեռականությունը, Lean-ի ապացույցները և Python-ի շարահյուսությունը։ Ծրագրի տրամաբանությունը սա է. AGI-ից հետո տնտեսության մեջ մարդիկ ի վերջո կդադարեն գրել ու կարդալ կոդ, բայց դեռ պետք է մեքենաներին աներկիմաստ ձևով փոխանցել, թե ինչ կառուցել։ Օրենքները մտադրությունն ավելի ճշգրիտ են արտահայտում, քան բնական լեզուն, ապացույցները հաստատում են, որ մոդելը ճիշտ է կատարել առաջադրանքը, իսկ արագ կոմպիլյատորը արդյունքը գործարկում է արագ։

Արագ է գործարկվում, արագ է ստուգվում

Bend-ը կոմպիլվում է բնիկ կոդի. մեկ միջուկում այն գրեթե C-ի արագությամբ է աշխատում, իսկ նույն բինարը տարածվում է տասնվեց միջուկում կամ GPU-ում՝ մինչև հարյուր անգամ ավելի արագ, քան մեկ միջուկում։ Արագությունը կարևոր է նաև ստուգման կողմում. Bend-ի տիպերի ստուգիչը ապացույցների ստուգիչ է՝ Lean-ի և Rocq-ի ավանդույթով, որտեղ միջին նախագծի ստուգումը կարող է րոպեներ տևել։ Bend-ին, կայքի պնդմամբ, առավելագույնը մեկ վայրկյան է պետք, և դա է պատճառը, որ ագենտը կարող է ամեն փոփոխությունից հետո ստուգել աշխատանքը։

Զուգահեռականություն առանց թելերի ու միջուկների

Այստեղ չկան թելեր, կողպեքներ և ձեռքով գրվող GPU միջուկներ։ Աշխատանքը բաժանում ես երկուսի, լեզուն կանչերը տարածում է բոլոր հասանելի միջուկների վրա, ապա արդյունքները միավորում։ Դեմոյում ցուցադրվում է երկուսի աստիճանի հաշվարկ 4 096 GPU միջուկում։

Օրենքները՝ որպես ապացույցով ամրացված AGENTS.md

Հարցին, թե ինչպես վստահել կոդին, որը ոչ ոք չի կարդացել, Bend-ը պատասխանում է ապացույց պահանջելով։ Օրենքները հայտարարվում են LAWS.bend ֆայլում, և դրանից հետո, ըստ կայքի, ոչ մի ագենտ չի կարող անցկացնել դրանք խախտող տող։ Օրինակում խաղի կանոնը պնդում է, որ քայլերի ոչ մի հաջորդականություն չի հանգեցնում հաղթանակի. օրենքը գրվում է քայլերի կամայական ցանկի վրա, տախտակը վերարտադրվում է սկզբից և ապացուցվում է, որ հաղթանակ երբեք չի լինում։ Զուգակից PROOF.bend ֆայլը, որը գրում է AI-ը, ապացուցում է, որ օրենքը պահպանվում է։ Օրինակում տախտակի «շուրջը փաթաթվելու» ֆունկցիան իրական սխալ բաց թողեց, իսկ օրենքից հետո ագենտը կրկնեց փորձերը, մինչև սահմանափակումն ապացուցվեց։ Սխալ հանելը, կայքի ձևակերպմամբ, դառնում է մաթեմատիկորեն անհնար — դա թեորեմ է։

Ինչպես սկսել

Տեղադրումը մեկ shell հրաման է, որից հետո հրահանգները ուղղված են կոդ գրող ագենտներին. AGENTS.md-ում ավելացվում է կարճ բլոկ, որը ագենտին ասում է գործարկել bend guide, կարևոր կանոնները պահել LAWS.bend-ում, ամեն commit-ից առաջ ստուգել bend PROOF.bend և հնարավորության դեպքում զուգահեռացնել կոդը։ Կայքը խորհուրդ է տալիս օրենքներ պահանջել այն ամենի համար, ինչը երբեք չպետք է կոտրվի, և սկսել back-end-ից՝ Linux-ում կամ macOS-ում։ Bend-ը երիտասարդ է, զգուշացնում են հեղինակները, ուստի սխալներ պետք է սպասել և դրանք հայտնել. մանրամասները լեզվի ուղեցույցում են՝ ինչպես նաև աֆին կախյալ տիպերի տեսության և CPU-ի ու GPU-ի զուգահեռ գործարկման միջավայրի մասին երկու աշխատանքներում։