Bend: AI səhvini sübutla bloklayan dil

Bend bir cümləlik təqdimatla gəlir: AI səhvlərini sübutla bloklayan sürətli dil; C sürətini, CUDA paralelliyini, Lean sübutlarını və Python sintaksisini birləşdirir. Layihənin gedişatı belədir: AGI-dən sonrakı iqtisadiyyatda insanlar sonda kodu yazmağı və oxumağı dayandıracaq, amma maşınlara nə qurmalı olduqlarını birmənalı çatdırmağın yolu yenə lazımdır. Saytın fikrincə, qanunlar niyyəti təbii dildən daha dəqiq ifadə edir, sübutlar modelin niyyəti düzgün tətbiq etdiyini yoxlayır, sürətli kompilyator isə nəticəni sürətlə işlədir.

Sürətli işləyir, sürətli yoxlanılır

Bend yerli koda kompilyasiya olunur. Tək nüvədə göstərici C-yə yaxındır; həmin binar on altı nüvədə və ya GPU-da paylanır və bir nüvədən yüz dəfəyə qədər sürətli işləyir. Sürət yoxlama tərəfində də önəmlidir: Bend-in tip yoxlayıcısı Lean və Rocq ənənəsində sübut yoxlayıcısıdır, orada orta ölçülü kod bazasının yoxlanması dəqiqələr çəkə bilir. Saytın iddiasına görə Bend ən çoxu bir saniyə sərf edir və buna görə agent hər dəyişiklikdən sonra işini yoxlaya bilir.

Thread və nüvə yazmadan paralellik

Burada thread, kilid və əl ilə yazılan GPU nüvəsi yoxdur. İşi ikiyə bölürsən, dil çağırışları tapa bildiyi bütün nüvələrə yayır, sonra nəticələri birləşdirir. Demoda ikinin qüvvəti hesabı 4 096 GPU nüvəsində göstərilir.

Sübutla dəstəklənən AGENTS.md kimi qanunlar

Heç kimin oxumadığı koda etibar sualına Bend sübut tələbi ilə cavab verir. Qanunlar LAWS.bend faylında elan olunur və sayta görə bundan sonra heç bir agent onları pozan sətri keçirə bilməz. Nümunədə oyun qaydası heç bir gediş ardıcıllığının qələbəyə aparmadığını bildirir: qanun ixtiyari gediş siyahısı üzərində yazılır, lövhə əvvəldən təkrar oynanılır və qazanmanın heç vaxt baş vermədiyi sübut olunur. AI-ın yazdığı cüt PROOF.bend faylı qanunun qüvvədə olduğunu təsdiqləyir. Nümunədə lövhənin öz ətrafından dolanması funksiyası canlı səhv kimi buraxılmışdı; qanun elan edildikdən sonra isə agent məhdudiyyəti sübut edənə qədər yenidən cəhd etməli oldu. Səhvi buraxmaq, saytın ifadəsi ilə, riyazi olaraq mümkünsüz olur — bu teoremdir.

Necə başlamaq olar

Quraşdırma bir shell əmridir, sonra təlimatlar kod yazan agentlərə ünvanlanır: AGENTS.md faylına agentin bend guide işlətməsini, vacib qaydaları LAWS.bend-də saxlamasını, hər commit-dən əvvəl bend PROOF.bend yoxlamasını və mümkün olan hər yerdə kodu paralelləşdirməsini söyləyən qısa blok əlavə olunur. Sayt heç vaxt pozulmamalı olan hər şey üçün qanun istəməyi və işə Linux və ya macOS-da back-end-dən başlamağı tövsiyə edir. Bend gəncdir, deyə xəbərdarlıq edilir: səhvlər gözlənilməlidir və bildirilməlidir; təfərrüatlar GitHub-dakı dil təlimatında və iki məqalədə — Bend-in nüvəsini təşkil edən afin asılı tip nəzəriyyəsi və CPU ilə GPU üçün paralel işləmə mühiti barədədir.