Sebuah projek yang baru diumumkan yang mendakwa menyediakan pengesahan formal untuk model pembelajaran mesin telah menimbulkan skeptisisme yang ketara daripada komuniti teknikal. Projek Pengesahan Formal Model Pembelajaran Mesin dalam Lean mendakwa menawarkan rangka kerja untuk membuktikan sifat-sifat seperti ketahanan, keadilan, dan kebolehinterpretasian model ML menggunakan pembuktian teorem Lean 4.
Projek ini menampilkan dirinya sebagai penyelesaian komprehensif dengan ciri-ciri termasuk perpustakaan Lean dengan definisi formal untuk pelbagai seni bina rangkaian neural, penterjemah model untuk menukar model terlatih kepada kod Lean, dan antara muka web untuk visualisasi dan pengurusan bukti. Walau bagaimanapun, pakar dalam bidang ini telah mengemukakan kebimbangan yang ketara mengenai kedua-dua kemungkinan dan kesahihan dakwaan tersebut.
Batasan Teknikal dan Janji Berlebihan
Ahli komuniti dengan kepakaran dalam pengesahan formal telah menunjukkan batasan asas dalam pendekatan tersebut. Pengesahan formal model ML yang kompleks menghadapi cabaran yang sedia ada yang projek ini nampaknya tidak mengambil kira. Membuktikan sifat-sifat bermakna tentang rangkaian neural terkenal sukar, terutamanya untuk aplikasi dunia sebenar.
Ini nampaknya tidak berguna... bahagian yang sebenarnya sukar sudah tentu adalah bukti itu sendiri, yang mereka nampaknya tidak selesaikan. Teorem jenis model X sentiasa melakukan perkara yang diingini ini hampir selalu salah (kerana ia adalah model yang tidak tepat), dan teorem jenis model X sentiasa melakukan perkara yang diingini ini Y% masa nampaknya sangat sukar untuk dibuktikan.
Contoh-contoh dalam repositori telah dikritik kerana menjadi remeh dan tidak mewakili cabaran pengesahan dunia sebenar. Seorang pengulas menyatakan bahawa contoh keadilan hanya membuktikan bahawa pengelas yang sentiasa mengembalikan ya akan mempunyai peratusan klasifikasi yang sama merentasi semua demografi—hasil yang secara matematik remeh tanpa kepentingan praktikal.
Persoalan Tentang Kesahihan
Beberapa pengulas telah mengemukakan kebimbangan tentang kesahihan projek itu sendiri. Kod Lean dalam repositori telah digambarkan sebagai campuran Lean 3 dan 4 yang dihasilkan oleh AI yang mungkin tidak dikompilasi dengan betul. Ketiadaan sebarang kerja saintifik yang dirujuk atau kertas penyelidikan berkaitan seterusnya melemahkan kredibiliti projek.
Seorang ahli komuniti menyatakan kejutan bahawa projek itu mencapai halaman depan Hacker News walaupun kelihatan dipenuhi dengan stub yang dihasilkan AI dan janji-janji dan bukannya kandungan substantif. Kekurangan asas saintifik adalah sangat membimbangkan memandangkan kerumitan domain masalah.
Isu-Isu Utama yang Dibangkitkan oleh Komuniti:
- Kebimbangan Kualiti Kod: Digambarkan sebagai "campuran Lean 3 dan 4 yang dihasilkan oleh AI" yang berkemungkinan tidak dapat dikompilasi
- Bukti Terhad: Contoh-contoh hanya membuktikan sifat-sifat remeh (contohnya, pengelas yang sentiasa mengembalikan "ya" mempunyai kadar pengelasan 100% untuk semua kumpulan)
- Kekurangan Asas Saintifik: Tiada kertas penyelidikan atau rangka kerja teori yang dirujuk
- Cabaran yang Tidak Ditangani:
- Mengendalikan elemen stokastik dalam AI generatif
- Menentukan metrik objektif untuk konsep seperti "keadilan"
- Membuktikan sifat-sifat bermakna tentang rangkaian neural yang kompleks
Pendekatan Alternatif yang Disebut:
- ANSR (Assured Neuro-Symbolic Reasoning) oleh DARPA
- TIAMAT (Transfer from Imprecise Models for Assured Tactical Autonomy) oleh DARPA
Cabaran Asas dalam Pengesahan ML
Perbincangan menyoroti beberapa cabaran asas dalam pengesahan formal model ML yang projek ini tidak menangani secukupnya. Untuk model stokastik—yang termasuk kebanyakan sistem AI generatif—pengesahan menjadi lebih rumit. Seperti yang ditanya oleh seorang pengulas, Bagaimana mereka menangani model dengan unsur stokastik? Tidak pasti bagaimana anda bercadang untuk membuktikan persampelan.
Bahkan menentukan sifat-sifat yang perlu disahkan menimbulkan cabaran yang ketara. Konsep seperti keadilan secara semulajadinya kabur dan sukar untuk ditakrifkan secara objektif dalam istilah matematik. Sementara itu, membuktikan bahawa model bahasa tidak menghasilkan pernyataan palsu nampaknya menjadi masalah yang sukar diselesaikan.
Walaupun terdapat skeptisisme mengenai projek tertentu ini, komuniti mengiktiraf kepentingan kerja dalam arah ini. Pendekatan alternatif yang disebut termasuk program DARPA iaitu ANSR (Assured Neuro-Symbolic Reasoning) dan TIAMAT (Transfer from Imprecise Models for Assured Tactical Autonomy), yang menangani cabaran berkaitan dalam pengesahan AI dengan sokongan saintifik yang lebih ketat.
Perbincangan ini berfungsi sebagai peringatan tentang jurang antara dakwaan bercita-cita tinggi dalam keselamatan AI dan realiti teknikal semasa. Walaupun pengesahan formal sifat-sifat mudah untuk model ML tertentu adalah mungkin, rangka kerja pengesahan komprehensif yang boleh mengendalikan sistem pembelajaran mendalam moden kekal sebagai cabaran penyelidikan terbuka dan bukannya masalah yang telah diselesaikan.
Rujukan: Formal Verification of Machine Learning Models in Lean