Bend: yapay zekâ hatalarını ispatla engelleyen dil

Bend tek cümlelik bir tanıtımla geliyor: yapay zekâ hatalarını ispatla engelleyen hızlı bir dil; C hızı, CUDA paralelliği, Lean ispatları ve Python sözdizimini bir araya getiriyor. Projenin çerçevesi şu: AGI sonrası ekonomide insanlar bir noktada kodu yazmayı ve okumayı bırakacak, ancak makinelere ne inşa edeceklerini belirsizlik olmadan anlatmanın bir yolu gerekli. Siteye göre yasalar niyeti doğal dilden daha kesin ifade ediyor, ispatlar modelin niyeti doğru uyguladığını doğruluyor ve hızlı derleyici sonucu çalıştırıyor.

Hızlı çalışır, hızlı denetlenir

Bend yerel koda derleniyor. Tek çekirdekte başarım C'ye yakın; aynı ikili on altı çekirdeğe ya da GPU'ya yayılıyor ve tek çekirdekten yüz kata kadar hızlı çalışıyor. Hız denetleme tarafında da önemli: Bend'in tip denetleyicisi Lean ve Rocq geleneğinde bir ispat denetleyicisi; o sistemlerde orta boy bir kod tabanının denetimi dakikalar alabiliyor. Sitenin iddiasına göre Bend en fazla bir saniye harcıyor, bu da bir ajanın her değişiklikten sonra işini doğrulamasını mümkün kılıyor.

İş parçacığı ve çekirdek yazmadan paralellik

Burada iş parçacığı, kilit ve elle yazılacak GPU çekirdeği yok. İşi ikiye bölersiniz, dil çağrıları bulabildiği her çekirdeğe dağıtır ve sonuçları geri birleştirir. Demoda ikinin kuvveti hesabı 4.096 GPU çekirdeğinde çalıştırılıyor.

İspatla desteklenen AGENTS.md olarak yasalar

Kimsenin okumadığı koda güvenme sorusuna Bend ispat talebiyle yanıt veriyor. Yasalar LAWS.bend adlı dosyada bildirilir ve siteye göre bundan sonra hiçbir ajan onları bozan bir satırı geçiremez. Örnekte bir oyun kuralı, hiçbir hamle dizisinin zafere götürmediğini söylüyor: yasa rastgele bir hamle listesi üzerinde yazılıyor, tahta baştan oynatılıyor ve kazanmanın asla gerçekleşmediği kanıtlanıyor. AI'ın yazdığı eş dosya PROOF.bend yasanın geçerli olduğunu ortaya koyuyor. Sitedeki örnekte tahtanın kendi etrafından dolanmasını sağlayan özellik canlı bir hata olarak yayına girmiş; yasa bildirildikten sonraysa ajan, kısıtı kanıtlayana kadar yeniden denemek zorunda kalmış. Hata yayına almak, sitenin ifadesiyle, matematiksel olarak imkânsız hale geliyor: bu bir teorem.

Nasıl başlanır

Kurulum tek bir shell komutu; ardından talimatlar kodlama ajanlarına yönelik: AGENTS.md dosyasına ajanın bend guide çalıştırmasını, önemli kuralları LAWS.bend'de tutmasını, her commit öncesi bend PROOF.bend denetlemesini ve mümkün olan her yerde kodu paralelleştirmesini söyleyen kısa bir blok ekleniyor. Site, asla bozulmaması gereken her şey için yasa istenmesini ve işe Linux ya da macOS'ta arka uçtan başlanmasını öneriyor. Bend genç, diye uyarıyor: hatalar beklenmeli ve bildirilmeli; ayrıntılar GitHub'daki dil kılavuzunda ve biri Bend'in çekirdeğini oluşturan afin bağımlı tip teorisi, diğeri CPU ve GPU için paralel çalışma ortamı üzerine iki makalede.