OpenAI'nin Lean 4 İspat Kodlarını Nasıl Doğruladılar?

OpenAI geçen dönemde on-proofs adlı bir depo yayımladı; yapay zeka ile çözülen karmaşık matematik ispatlarını Lean 4 dilinde sunuyor. Fakat kimse 37.000 satır kodu elle okuyamıyor. Başka bir LLM'ye "bunu kontrol et" demek de işe yaramıyor, sadece halüsinasyonla "tamam" diyor. Peki, bu tür iddiaları gerçekten nasıl doğrulayabiliriz?

Bir geliştirici bu soruya cevap vermek için harness-audit-sidecar adlı açık kaynak aracını kullanarak OpenAI'nin ispatlarını yerel ortamda denetledi. Yöntem basit ama etkili: LLM'nin "bu doğru mu?" sorusundan çok "bunun fiziksel kanıtı var mı?" sorusunu sordu. Derleyici (Lean) gibi davranmak yerine, gerçek bir tanık olmak.

Denetim süreci 7,2 GB'lık Mathlib kütüphanesini indirmeyi, 8.687 derleme işini yerel makinede çalıştırmayı ve sonra LeanProofAuditor aracını uygulamayı içerdi. Sonuç: 23 ispattan 11'i geçti, 12'si başarısız oldu. Başarısız olanlar eksik tanımlar, yanlış referanslar veya tamamlanmamış mantıksal adımlar içeriyordu. Hiçbir halüsinasyon yok, derleyici ya "evet, bu işe yaradı" ya da "hayır, burada sorun var" dedi.

Bu yaklaşım önemli çünkü AI laboratuvarlarının iddialarını doğrulamak için artık uzman matematikçi beklemek zorunda değiliz. Otomatik denetim, herkese (özellikle açık kaynak katkıcılarına) AI tarafından üretilen kodun gerçekten işe yarayıp yaramadığını görmek için bir yol sunuyor. Derleyici yalan söylemez; ama LLM'ler söyler.