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 ახალგაზრდაა — ხარვეზები მოსალოდნელია და GitHub-ის issue-ს სახით უნდა შეტყობინდეს; დეტალები ენის გიდშია და ორ ნაშრომში: ერთი Bend-ის ბირთვზე — აფინურ, დამოკიდებულ ტიპებზე — და მეორე CPU-სა და GPU-ს პარალელურ გარემოზე.