Bend dili, yapay zekanın yazdığı kodu matematiksel kanıtla denetliyor

Bend, yapay zeka ajanlarının yazdığı kodu kanıtla denetlemeyi hedefleyen yeni bir programlama dili. Tanıtım metnine göre dilin tip denetleyicisi aynı zamanda bir kanıt denetleyicisi; Lean ve Rocq'ta olduğu gibi. Aradaki fark hızda: ekip, orta büyüklükte bir kod tabanında bu araçların dakikalar sürebildiğini, Bend'in ise en fazla bir saniye aldığını söylüyor. Böylece bir yapay zeka ajanı her değişiklikten sonra denetim yapabiliyor.

Kuralları bozan kod derlenmiyor

Kuralların yazıldığı yer LAWS.bend dosyası. Burada bir yasa tanımlandıktan sonra, projeye o yasayı bozan tek satır bile giremiyor. Tanıtımda verilen oyun örneğinde LAWS.bend olmadan hata canlıya çıkıyor; dosya devredeyken yapay zeka, yasanın geçerli olduğunu kanıtlayana kadar denemek zorunda kalıyor. Ekip bunu şöyle anlatıyor: hatalı kodun birleştirilmesi matematiksel olarak imkansız, çünkü artık bir teorem. Aynı yaklaşımı AGENTS.md dosyasının kanıtla desteklenmiş hali diye tarif ediyorlar.

Tek çekirdekte C hızı, GPU'da paralellik

Bend yerel koda derleniyor. Tek çekirdekte C'ye yakın hızda çalıştığı, aynı ikili dosyanın on altı çekirdekte ya da GPU'da çalışabildiği belirtiliyor; bu durumda tek çekirdeğe kıyasla yüz kata kadar hızlanma söz konusu. Geliştiricinin iş parçacığı, kilit veya çekirdek kodu yazması gerekmiyor: işi ikiye bölüyorsunuz, Bend çağrıları bulduğu bütün çekirdeklere dağıtıp sonucu birleştiriyor. Tanıtımda pow2 fonksiyonunun 4.096 GPU çekirdeğinde çalıştığı bir örnek gösteriliyor.

Dilin tamamı GUIDE.md dosyasında anlatılıyor, bend guide komutu bunu terminale basıyor. Çekirdeğindeki afin bağımlı tip teorisi BendTT, CPU ve GPU için paralel çalışma zamanı ise BendRT adlı makalelerde açıklanıyor. Ekip projenin genç olduğunu, hata beklendiğini ve bunların bildirilmesini istediğini söylüyor; Bend şimdilik en iyi arka uçta, Linux ve macOS üzerinde çalışıyor. Ayrıntılar proje sitesinde.