Basis, LLM'lerin yazdığı dil semantiğini derlenmiş bir RISC-V yorumlayıcısına karşı kanıtladı

Ekibin yaptığı iş

Basis'teki araştırmacılar, büyük dil modellerinin küçük bir imperatif dil için — bir programlama dilinin nasıl davrandığını tanımlayan kesin matematiksel kurallar bütününden oluşan — biçimsel bir semantik yazdığı ve ardından Lean ispat asistanı kullanılarak bu kuralların dilin gerçek uygulamasıyla, makine koduna kadar örtüştüğünün gösterildiği bir deneyi raporluyor.

Kiran Gopinathan, Nikhil Pimpalkhare, Yiyun Liu ve Zenna Tavares tarafından kaleme alınan ve "Ship Your Interpreter" başlığını taşıyan Basis blog yazısına göre hedef, ders kitaplarındaki imperatif dil olan WHILE'ın genişletilmiş bir sürümü. Bu sürüm tam sayılar, dizeler, closure'larla birinci sınıf fonksiyonlar, if, while ve for döngüleri ile runtime hataları ekliyor; tam sayı işlemlerinde 64-bit sarmalanmış aritmetik kullanılıyor. Yorumlayıcı 1.855 satırlık C kodundan oluşuyor ve bir LLM, dili tanımlayan yaklaşık 400 satırlık Lean kuralı üretti — her ifade ve ifade türü için bir kural.

Otorite olarak yorumlayıcı

Ekibin yöntemi, sevk edilen yorumlayıcıyı dildeki programların anlamı konusunda otorite olarak ele alıyor. C yorumlayıcısını, zaten biçimsel bir tanıma sahip bir komut seti olan RISC-V'ye derlediler; bu da yorumlayıcının herhangi bir programla ne yaptığına dair tam ama okunması zor bir hesap ortaya koyuyor. Bunun ardından LLM ajanları, okunabilir kurallarının derlenmiş yorumlayıcının olası her program için ne yazdıracağını tam olarak öngördüğünü Lean'de kanıtlamak zorundaydı. Bir kural yanlışsa ispat tamamlanamıyor — süreç sessizce geçmek yerine tıkanıyor. Basis, semantik ve ispat dahil tamamının GitHub'da yayımlandığını söylüyor.

Test paketi neden yeterli değildi

Yazı, bu ispat adımının neden önemli olduğunu açıklıyor. Üretilen semantiğin ilk sürümlerinden biri, yorumlayıcının tüm test paketini geçtiği halde derlenmiş binary ile bir durumda ayrışıyor: bir fonksiyonun adı 59 karaktere ulaştığında binary, adı yazdırılan çıktıda keserken semantik adı eksiksiz yazdırıyordu. Test ayrışmayı tamamen gözden kaçırdı; binary'ye karşı kontrol edilen bir ispat bunu yapamaz, çünkü herhangi bir uyuşmazlık ispatın tamamlanmasını engeller.

Daha geniş bir çabanın parçası

Basis, deneyi makul biçimde tüm yazılımı kapsayabilecek doğrulamaya giden yolda bir adım olarak konumlandırıyor. Yazıda anlatıldığı üzere Nisan ayında ajanları bir JavaScript'ten WebAssembly'a derleyici geliştirdi ama program davranışını koruduğunu kanıtlayamadı; aylar sonra ajanlar, güvenlik duvarı kurallarını çekirdeğin çalıştırdığı komutlara çeviren Linux'un nftables derleyicisini doğruladı. Eylül ayında MIT araştırmacıları Frans Kaashoek ve Nickolai Zeldovich, AI ajanları kullanarak xv6 eğitim işletim sistemini makine koduna kadar doğruladı.

Daha geniş engel, biçimsel semantiğin yalnızca bir avuç dil için var olması — C için CompCert, ML için CakeML, JavaScript için JSCert ve RISC-V komut seti — ve her birinin yıllarca süren uzman emeği gerektirmesi, çoğu zaman dilin yalnızca bir alt kümesini kapsaması. Çoğu dilin hiç semantiği yok ve bu da programların karşılaştırılabileceği kesin bir şey bırakmıyor. Basis'e göre LLM'ler ispat kurmada iyileştikçe zor problem şartnamaya kayıyor: kanıtlanan ifadelerin insanların gerçekten önem verdiği davranışı yakaladığından emin olmak.

Neden önemli

Makine tarafından kontrol edilen ispatlar hataları örneklemek yerine bütün kategorilerini ortadan kaldırıyor ve Basis'in açıkladığı motivasyon açıkça çekişmeye dayalı: LLM'ler üretim yazılımındaki hataları bulma ve istismar etme konusunda belirgin biçimde daha iyi hale geliyor ve doğrulanmış yazılım, ayak uydurabilen az sayıdaki savunmadan biri.

Buradaki özel teknik — bir dilin biçimsel semantiğini mevcut yorumlayıcısından türetmek ve ispatı testler değil derlenmiş makine koduna karşı kontrol etmek — hiç olmamış diller için titiz, makine tarafından kontrol edilen tanımlara giden bir yol sunuyor. Bu da üzerine doğrulanmış derleyiciler, yorumlayıcılar ve analiz araçları inşa etmek için bir ön koşul. Açık soru ölçek: bu deney küçük bir ders kitabı dilini kapsıyor, üretim dilini değil; aynı hattın gerçek dillerin yüzey alanına karşı ayakta kalıp kalmayacağı henüz gösterilmeli.