Sebuah proyek yang baru saja diumumkan yang mengklaim menyediakan verifikasi formal untuk model pembelajaran mesin telah menimbulkan skeptisisme yang signifikan dari komunitas teknis. Proyek Formal Verification of Machine Learning Models in Lean mengklaim menawarkan kerangka kerja untuk membuktikan properti seperti ketahanan, keadilan, dan interpretabilitas model ML menggunakan pembuktian teorema Lean 4.
Proyek ini mempresentasikan dirinya sebagai solusi komprehensif dengan fitur-fitur termasuk pustaka Lean dengan definisi formal untuk berbagai arsitektur jaringan saraf, penerjemah model untuk mengkonversi model terlatih ke kode Lean, dan antarmuka web untuk visualisasi dan manajemen bukti. Namun, para ahli di bidang ini telah mengajukan kekhawatiran substansial tentang kelayakan dan keaslian klaim tersebut.
Keterbatasan Teknis dan Janji Berlebihan
Anggota komunitas dengan keahlian dalam verifikasi formal telah menunjukkan keterbatasan mendasar dalam pendekatan tersebut. Verifikasi formal model ML yang kompleks menghadapi tantangan inheren yang tampaknya diabaikan oleh proyek ini. Membuktikan properti yang bermakna tentang jaringan saraf terkenal sulit, terutama untuk aplikasi dunia nyata.
Ini tampaknya tidak ada gunanya... bagian yang benar-benar sulit tentu saja adalah bukti itu sendiri, yang tampaknya tidak mereka selesaikan. Teorema jenis model X selalu melakukan hal yang diinginkan ini hampir selalu salah (karena itu adalah model yang tidak tepat), dan teorema jenis model X selalu melakukan hal yang diinginkan ini Y% dari waktu tampaknya sangat sulit untuk dibuktikan.
Contoh-contoh dalam repositori telah dikritik karena bersifat sepele dan tidak mewakili tantangan verifikasi dunia nyata. Salah satu komentator mencatat bahwa contoh keadilan hanya membuktikan bahwa pengklasifikasi yang selalu mengembalikan ya akan memiliki persentase klasifikasi yang sama di semua demografi—hasil yang secara matematis sepele tanpa signifikansi praktis.
Pertanyaan Tentang Keaslian
Beberapa komentator telah mengajukan kekhawatiran tentang keaslian proyek itu sendiri. Kode Lean dalam repositori telah digambarkan sebagai campuran yang dihasilkan AI dari Lean 3 dan 4 yang kemungkinan tidak dapat dikompilasi dengan benar. Tidak adanya karya ilmiah yang dikutip atau makalah penelitian terkait semakin melemahkan kredibilitas proyek.
Salah satu anggota komunitas menyatakan keterkejutan bahwa proyek tersebut mencapai halaman depan Hacker News meskipun tampaknya dipenuhi dengan stub yang dihasilkan AI dan janji-janji daripada konten substantif. Kurangnya landasan ilmiah sangat mengkhawatirkan mengingat kompleksitas domain masalah.
Masalah Utama yang Diangkat oleh Komunitas:
- Kekhawatiran Kualitas Kode: Digambarkan sebagai "campuran Lean 3 dan 4 yang dihasilkan oleh AI" yang kemungkinan tidak dapat dikompilasi
- Bukti Terbatas: Contoh hanya membuktikan properti sepele (misalnya, pengklasifikasi yang selalu mengembalikan "ya" memiliki tingkat klasifikasi 100% untuk semua kelompok)
- Kurangnya Dasar Ilmiah: Tidak ada kutipan makalah penelitian atau kerangka teoretis
- Tantangan yang Belum Ditangani:
- Penanganan elemen stokastik dalam AI generatif
- Mendefinisikan metrik objektif untuk konsep seperti "keadilan"
- Membuktikan properti bermakna tentang jaringan neural yang kompleks
Pendekatan Alternatif yang Disebutkan:
- ANSR dari DARPA (Assured Neuro-Symbolic Reasoning)
- TIAMAT dari DARPA (Transfer from Imprecise Models for Assured Tactical Autonomy)
Tantangan Mendasar dalam Verifikasi ML
Diskusi menyoroti beberapa tantangan mendasar dalam memverifikasi model ML secara formal yang tidak ditangani secara memadai oleh proyek tersebut. Untuk model stokastik—yang mencakup sebagian besar sistem AI generatif—verifikasi menjadi lebih rumit. Seperti yang ditanyakan oleh salah satu komentator, Bagaimana mereka menangani model dengan elemen stokastik? Tidak yakin bagaimana Anda bermaksud membuktikan sampling.
Bahkan mendefinisikan properti apa yang harus diverifikasi menghadirkan tantangan yang signifikan. Konsep seperti keadilan pada dasarnya ambigu dan sulit untuk didefinisikan secara objektif dalam istilah matematika. Sementara itu, membuktikan bahwa model bahasa tidak menghasilkan pernyataan palsu tampaknya menjadi masalah yang sulit dipecahkan.
Meskipun ada skeptisisme seputar proyek tertentu ini, komunitas mengakui pentingnya pekerjaan ke arah ini. Pendekatan alternatif yang disebutkan termasuk program DARPA yaitu ANSR (Assured Neuro-Symbolic Reasoning) dan TIAMAT (Transfer from Imprecise Models for Assured Tactical Autonomy), yang menangani tantangan terkait dalam verifikasi AI dengan dukungan ilmiah yang lebih ketat.
Diskusi ini berfungsi sebagai pengingat tentang kesenjangan antara klaim ambisius dalam keamanan AI dan realitas teknis saat ini. Sementara verifikasi formal properti sederhana untuk model ML tertentu adalah mungkin, kerangka verifikasi komprehensif yang dapat menangani sistem pembelajaran mendalam modern tetap menjadi tantangan penelitian terbuka daripada masalah yang telah terpecahkan.
Referensi: Formal Verification of Machine Learning Models in Lean