Ke Arah AI Boleh Disahkan: Lima Cabaran Kaedah Formal

Kecerdasan buatan ialah sistem pengkomputeran yang cuba meniru kecerdasan manusia, termasuk beberapa fungsi manusia yang secara intuitif berkaitan dengan kecerdasan, seperti pembelajaran, penyelesaian masalah dan pemikiran dan tindakan yang rasional. Ditafsirkan secara meluas, istilah AI merangkumi banyak bidang yang berkait rapat seperti pembelajaran mesin. Sistem yang banyak menggunakan AI mempunyai kesan sosial yang ketara dalam bidang seperti penjagaan kesihatan, pengangkutan, kewangan, rangkaian sosial, e-dagang dan pendidikan.

Impak sosial yang semakin meningkat ini juga telah membawa beberapa siri risiko dan kebimbangan, termasuk ralat dalam perisian kecerdasan buatan, serangan siber dan keselamatan sistem kecerdasan buatan. Oleh itu, isu pengesahan sistem AI, dan topik AI yang boleh dipercayai yang lebih luas, telah mula menarik perhatian daripada komuniti penyelidikan. "AI Boleh Disahkan" telah ditubuhkan sebagai matlamat untuk mereka bentuk sistem AI, sistem AI boleh disahkan dengan jaminan ketepatan yang kukuh dan ideal yang boleh dibuktikan pada keperluan matematik tertentu. Bagaimanakah kita boleh mencapai matlamat ini?

Baru-baru ini, artikel ulasan dalam "The Communications of ACM" cuba memikirkan tentang cabaran yang dihadapi oleh AI yang boleh disahkan dari perspektif pengesahan formal, dan memberikan beberapa penyelesaian berprinsip. Penulisnya ialah Profesor S. Shankar Sastry dan Sanjit A. Seshia, pengerusi Jabatan Kejuruteraan Elektrik dan Sains Komputer di UC Berkeley, dan Dorsa Sadigh, penolong profesor sains komputer di Universiti Stanford.

Dalam sains komputer dan kejuruteraan, kaedah formal melibatkan spesifikasi matematik, reka bentuk dan pengesahan sistem yang ketat. Pada terasnya, kaedah formal adalah mengenai pembuktian: merumuskan spesifikasi yang membentuk kewajipan pembuktian, mereka bentuk sistem untuk memenuhi kewajipan ini, dan mengesahkan melalui carian bukti algoritma bahawa sistem itu memang mematuhi spesifikasinya. Daripada ujian dan simulasi dipacu spesifikasi kepada pemeriksaan model dan pembuktian teorem, pelbagai kaedah formal biasanya digunakan dalam reka bentuk bantuan komputer bagi litar bersepadu dan telah digunakan secara meluas untuk mencari pepijat dalam perisian, menganalisis sistem fizikal siber dan menemui Keselamatan. kelemahan.

Artikel ini menyemak penggunaan tradisional kaedah formal, dan mengenal pasti lima cabaran unik kaedah formal dalam sistem AI, termasuk:

• Membangunkan bahasa dan algoritma tentang alam sekitar
• Mengabstrak dan mewakili komponen dan sistem ML yang kompleks
• Cadangkan kaedah dan sifat rasmi kanonik baharu untuk sistem dan data AI
• Membangunkan untuk inferens automatik Enjin pengkomputeran berskala
• membangunkan algoritma dan teknologi yang direka untuk dipercayai-oleh-pembinaan

Berdasarkan membincangkan kemajuan terkini, penulis mencadangkan prinsip untuk menangani cabaran di atas. Artikel ini bukan sahaja menumpukan pada jenis komponen AI tertentu seperti rangkaian saraf dalam atau kaedah khusus seperti pembelajaran pengukuhan, tetapi cuba untuk merangkumi rangkaian sistem AI yang lebih luas dan proses reka bentuknya. Tambahan pula, kaedah formal hanyalah satu laluan ke arah AI yang boleh dipercayai, jadi idea dalam artikel ini bertujuan untuk melengkapkan kaedah dari bidang lain. Perspektif ini sebahagian besarnya dimaklumkan dengan memikirkan isu yang timbul daripada penggunaan AI dalam sistem autonomi dan separa autonomi, di mana isu keselamatan dan pengesahan lebih menonjol.

Ikhtisar

Rajah 1 menunjukkan proses biasa untuk pengesahan formal, sintesis formal dan daya tahan masa jalan yang dipandu secara formal. Proses pengesahan rasmi bermula dengan tiga input:

Rajah 1: Formal untuk pengesahan, sintesis dan daya tahan masa jalan Kaedah kimiaisasi

1. Model sistem S untuk disahkan
2. Model persekitaran E
3. Atribut untuk disahkan Φ

Pengesah menjana jawapan "ya" atau "tidak" sebagai output untuk menunjukkan Sama ada S memenuhi sifat Φ dalam persekitaran E. Biasanya, output "tidak" disertakan dengan contoh balas, juga dipanggil jejak ralat, yang merupakan pelaksanaan sistem yang menunjukkan bagaimana Φ dipalsukan. Sesetengah alat pengesahan juga termasuk bukti ketepatan atau sijil dengan jawapan "ya". Kami mengambil perspektif yang luas tentang kaedah formal, termasuk sebarang teknik yang menggunakan beberapa aspek spesifikasi formal, pengesahan atau sintesis. Sebagai contoh, kami menyertakan kaedah pengesahan perkakasan berasaskan simulasi atau kaedah ujian perisian berasaskan model kerana mereka juga menggunakan spesifikasi atau model formal untuk membimbing proses simulasi atau ujian.

Untuk menggunakan pengesahan rasmi pada sistem AI, anda mesti boleh mewakili sekurang-kurangnya tiga input S, E dan Φ secara rasmi Prosedur membuat keputusan yang berkesan untuk menjawab soalan ya/tidak yang diterangkan sebelum ini. Walau bagaimanapun, ia bukanlah sesuatu yang remeh untuk membina perwakilan yang baik walaupun untuk tiga input, apatah lagi menangani kerumitan reka bentuk asas dan isu pengesahan.

Di sini kami menggambarkan maksud artikel ini melalui contoh dari bidang pemanduan separa autonomi. Rajah 2 menunjukkan contoh ilustrasi sistem AI: CPS gelung tertutup yang merangkumi kenderaan separa autonomi dengan komponen pembelajaran mesin dan persekitarannya. Secara khusus, anggap bahawa kenderaan "ego" separa autonomi mempunyai sistem brek kecemasan automatik (AEBS) yang cuba mengesan dan mengklasifikasikan objek di hadapan dan menggunakan brek apabila diperlukan untuk mengelakkan perlanggaran. Dalam Rajah 2, AEBS terdiri daripada pengawal (brek autonomi), objek terkawal (subsistem kenderaan terkawal, termasuk bahagian lain tindanan autonomi) dan penderia (kamera), serta komponen persepsi menggunakan DNN . AEBS digabungkan dengan persekitaran kenderaan untuk membentuk CPS gelung tertutup. Persekitaran kenderaan "diri sendiri" termasuk ejen dan objek di luar kenderaan (kenderaan lain, pejalan kaki, dll.) serta di dalam kenderaan (cth., pemandu). Keperluan keselamatan sistem gelung tertutup sedemikian boleh dicirikan secara tidak rasmi dari segi sifat mengekalkan jarak selamat antara kenderaan "ego" yang bergerak dan mana-mana ejen atau objek lain di jalan raya. Walau bagaimanapun, terdapat banyak nuansa dalam spesifikasi, pemodelan, dan pengesahan sistem sedemikian.

Rajah 2: Contoh CPS gelung tertutup dengan komponen pembelajaran mesin

Mula-mula, pertimbangkan untuk memodelkan persekitaran kenderaan separa autonomi. Malah soalan seperti berapa banyak dan ejen yang manakah (manusia dan bukan manusia) berada dalam persekitaran, apatah lagi sifat dan tingkah laku mereka, boleh tertakluk kepada ketidakpastian yang agak besar. Kedua, tugas persepsi menggunakan AI atau ML sukar, jika tidak mustahil, untuk diformalkan. Ketiga, komponen seperti DNN mungkin kompleks, objek berdimensi tinggi yang beroperasi pada ruang input berdimensi tinggi yang kompleks. Oleh itu, adalah sangat mencabar untuk menjana tiga input S, E, Φ proses pengesahan formal walaupun dalam bentuk yang menjadikan pengesahan itu boleh dikendalikan.

Jika sesiapa menyelesaikan masalah ini, ia akan menghadapi tugas sukar untuk mengesahkan CPS berasaskan AI sekompleks seperti Rajah 2. Dalam CPS sedemikian, pendekatan komposisi (modular) adalah penting untuk skalabiliti, tetapi ia boleh menjadi sukar untuk dilaksanakan disebabkan oleh faktor seperti kesukaran spesifikasi komposisi. Akhir sekali, pendekatan yang betul mengikut pembinaan (CBC) menjanjikan AI yang boleh disahkan, tetapi ia masih di peringkat awal dan sangat bergantung pada kemajuan dalam spesifikasi dan pengesahan. Rajah 3 meringkaskan lima bidang mencabar AI boleh disahkan. Untuk setiap kawasan, kami menyaring pendekatan yang menjanjikan semasa ke dalam tiga prinsip untuk mengatasi cabaran, diwakili sebagai nod. Tepi antara nod menunjukkan prinsip AI yang boleh disahkan bergantung antara satu sama lain, dengan benang pergantungan biasa diwakili oleh satu warna. Cabaran dan prinsip yang sepadan ini dihuraikan di bawah.

Rajah 3: Ringkasan 5 bidang cabaran AI boleh disahkan

Pemodelan persekitaran

Berdasarkan AI The persekitaran di mana sistem /ML dijalankan biasanya sangat kompleks, seperti memodelkan pelbagai persekitaran trafik bandar di mana kenderaan autonomi beroperasi. Malah, AI/ML sering diperkenalkan ke dalam sistem ini untuk mengatasi kerumitan dan ketidakpastian persekitaran. Proses reka bentuk ML semasa sering menggunakan data untuk menentukan persekitaran secara tersirat. Matlamat kebanyakan sistem AI adalah untuk menemui dan memahami persekitaran mereka semasa mereka beroperasi, tidak seperti sistem tradisional yang direka untuk persekitaran yang ditentukan secara priori. Walau bagaimanapun, semua pengesahan dan sintesis rasmi adalah berkaitan dengan model persekitaran. Oleh itu, andaian dan sifat tentang data input mesti ditafsirkan ke dalam model persekitaran. Kami menyaring dikotomi ini kepada tiga cabaran untuk memodelkan persekitaran sistem AI dan membangunkan prinsip yang sepadan untuk menangani cabaran ini.

2.1 Pemodelan Ketidakpastian ​

Dalam penggunaan tradisional pengesahan formal, perkara biasa pendekatan adalah untuk memodelkan alam sekitar sebagai proses bukan deterministik yang terkekang, atau "gangguan". "Penghampiran berlebihan" pemodelan alam sekitar membolehkan seseorang menangkap ketidakpastian alam sekitar dengan lebih konservatif tanpa memerlukan model yang terlalu terperinci, yang akan menjadi sangat tidak cekap untuk membuat inferens. Walau bagaimanapun, untuk autonomi berasaskan AI, pemodelan bukan deterministik semata-mata mungkin menghasilkan terlalu banyak laporan ralat palsu, menjadikan proses pengesahan tidak berguna dalam amalan. Sebagai contoh, dalam memodelkan tingkah laku kenderaan di sekeliling kereta autonomi, tingkah laku kenderaan sekeliling adalah pelbagai Jika pemodelan tulen bukan deterministik diguna pakai, kemalangan yang selalu berlaku tanpa diduga tidak boleh diambil kira. Selain itu, banyak sistem AI/ML secara tersirat atau eksplisit membuat andaian pengedaran tentang data atau gelagat daripada persekitaran, yang memerlukan pemodelan kebarangkalian. Oleh kerana sukar untuk menentukan taburan asas dengan tepat, model kebarangkalian yang terhasil tidak boleh diandaikan sebagai sempurna, dan ketidakpastian dalam proses pemodelan mesti dicirikan dalam model itu sendiri.

Pemodelan formal kebarangkalian. Untuk menangani cabaran ini, kami mencadangkan satu bentuk yang menggabungkan pemodelan kebarangkalian dan tidak tentu. Pemodelan kebarangkalian boleh digunakan di mana taburan kebarangkalian boleh ditentukan atau dianggarkan dengan pasti. Dalam kes lain, pemodelan tidak tentu boleh digunakan untuk menganggarkan lebihan tingkah laku persekitaran. Walaupun formalisme seperti proses keputusan Markov sudah menyediakan cara untuk mencampurkan pendekatan kebarangkalian dan bukan penentu, kami percaya bahawa formalisme yang lebih kaya seperti paradigma pengaturcaraan kebarangkalian boleh memberikan lebih ekspresif dan prosedural untuk memodelkan persekitaran. Kami meramalkan bahawa dalam banyak kes prosedur kebarangkalian sedemikian perlu dipelajari (sebahagiannya) daripada data atau disintesis. Pada ketika ini, sebarang ketidakpastian dalam parameter yang dipelajari mesti disebarkan ke seluruh sistem dan diwakili dalam model kebarangkalian. Sebagai contoh, proses keputusan Markov cembung menyediakan cara untuk mewakili ketidakpastian dalam nilai kebarangkalian peralihan yang dipelajari dan melanjutkan algoritma untuk pengesahan dan kawalan untuk mengambil kira ketidakpastian ini.

2.2 Pembolehubah tidak diketahui​

Dalam medan pengesahan formal tradisional seperti peralatan pengesahan Dalam pemacu, antara muka antara sistem S dan persekitarannya E ditakrifkan dengan baik, dan E hanya boleh berinteraksi dengan S melalui antara muka ini. Untuk autonomi berasaskan AI, antara muka ini tidak lengkap dan ditentukan oleh komponen sensor dan persepsi yang hanya sebahagian dan bising menangkap persekitaran dan tidak dapat menangkap semua interaksi antara S dan E. Semua pembolehubah (ciri-ciri) persekitaran diketahui, apatah lagi dipersepsikan. Walaupun dalam senario terhad di mana pembolehubah persekitaran diketahui, terdapat kekurangan maklumat yang jelas tentang evolusi mereka, terutamanya pada masa reka bentuk. Selain itu, penderia pemodelan seperti lidar yang mewakili antara muka persekitaran merupakan cabaran teknikal yang ketara.

Pemodelan persekitaran introspektif. Kami mencadangkan untuk menangani masalah ini dengan membangunkan kaedah reka bentuk introspektif dan pengesahan, iaitu, melakukan introspeksi dalam sistem S untuk mengenal pasti secara algoritma andaian A tentang persekitaran E yang mencukupi untuk menjamin bahawa spesifikasi Φ dipenuhi. Sebaik-baiknya, A mestilah yang paling lemah dalam andaian sedemikian, dan juga mesti cukup cekap untuk menjana pada masa reka bentuk, memantau pada masa jalan untuk penderia yang tersedia dan sumber maklumat lain tentang persekitaran, dan memudahkan pengesanan apabila andaian dilanggar diambil. Tambahan pula, jika operator manusia terlibat, seseorang mungkin berharap bahawa A boleh diterjemahkan ke dalam penjelasan yang boleh difahami, iaitu, S boleh "menerangkan" kepada manusia mengapa ia mungkin tidak memenuhi spesifikasi Φ. Mengendalikan pelbagai keperluan ini, bersama-sama dengan keperluan untuk model sensor yang baik, menjadikan pemodelan persekitaran introspektif sebagai masalah yang sangat penting. Kerja awal menunjukkan bahawa pengekstrakan hipotesis boleh dipantau ini boleh dilaksanakan dalam kes mudah, walaupun lebih banyak kerja diperlukan untuk menjadikannya praktikal.

2.3 Mensimulasikan tingkah laku manusia​

Untuk kebanyakan sistem AI, seperti semi- kereta autonomi, ejen manusia adalah bahagian penting dalam persekitaran dan sistem. Model buatan manusia gagal menangkap dengan secukupnya kebolehubahan dan ketidakpastian tingkah laku manusia. Sebaliknya, pendekatan dipacu data untuk memodelkan tingkah laku manusia mungkin sensitif terhadap ekspresi dan kualiti data ciri yang digunakan oleh model ML. Untuk mencapai jaminan tinggi untuk sistem AI manusia, kita mesti menangani batasan teknik pemodelan manusia semasa dan memberikan jaminan tentang ketepatan ramalan dan penumpuannya.

Pemodelan dipacu data proaktif. Kami percaya bahawa pemodelan manusia memerlukan pendekatan dipacu data yang aktif, dan struktur model serta ciri yang diwakili secara matematik adalah sesuai untuk kaedah formal. Bahagian penting dalam pemodelan manusia ialah menangkap niat manusia. Kami mencadangkan pendekatan serampang tiga mata: mentakrifkan templat atau ciri model berdasarkan pengetahuan pakar, menggunakan pembelajaran luar talian untuk melengkapkan model untuk kegunaan masa reka bentuk, dan mempelajari serta mengemas kini model persekitaran pada masa jalan dengan memantau dan berinteraksi dengan persekitaran . Sebagai contoh, telah ditunjukkan bahawa data yang dikumpul daripada simulator memandu melalui eksperimen dengan subjek manusia boleh digunakan untuk menjana model tingkah laku pemandu manusia yang boleh digunakan untuk mengesahkan dan mengawal kenderaan autonomi. Selain itu, latihan lawan dan teknik serangan dalam keselamatan komputer boleh digunakan untuk pembelajaran aktif model manusia dan seterusnya mereka bentuk model untuk tindakan manusia tertentu yang membawa kepada tingkah laku tidak selamat. Teknik ini boleh membantu membangunkan algoritma pengesahan untuk sistem AI manusia.

Spesifikasi Formal

Pengesahan formal sangat bergantung pada spesifikasi formal - penyataan matematik yang tepat tentang perkara yang perlu dilakukan oleh sistem. Walaupun di kawasan di mana kaedah formal telah mencapai kejayaan yang besar, menghasilkan spesifikasi formal berkualiti tinggi adalah satu cabaran, dan sistem AI khususnya menghadapi cabaran yang unik.

3.1 Tugasan yang sukar untuk diformalkan ​

Dalam pengawal AEBS dalam Rajah 2 Modul persepsi mesti mengesan dan mengelaskan objek, membezakan kenderaan dan pejalan kaki daripada entiti lain. Ketepatan modul ini memerlukan definisi formal bagi setiap jenis pengguna jalan raya dan objek, yang amat sukar dalam pengertian kaedah formal klasik. Masalah ini wujud dalam semua pelaksanaan modul persepsi ini, bukan hanya dalam kaedah berasaskan pembelajaran mendalam. Masalah yang sama timbul dengan tugas lain yang melibatkan persepsi dan komunikasi, seperti pemprosesan bahasa semula jadi. Jadi, bagaimanakah kita menentukan atribut ketepatan untuk modul sedemikian? Apakah bahasa spesifikasi yang sepatutnya? Apakah alat yang boleh kita gunakan untuk membina spesifikasi?

Spesifikasi peringkat hujung ke hujung/peringkat sistem. Untuk menangani cabaran di atas, kita boleh mengubah sedikit masalah ini. Daripada menyatakan secara langsung tugas yang sukar untuk diformalkan, kita harus terlebih dahulu menumpukan pada menentukan dengan tepat kelakuan hujung ke hujung sistem AI. Daripada spesifikasi peringkat sistem ini, kekangan pada antara muka input-output komponen yang sukar untuk diformalkan boleh diperolehi. Kekangan ini berfungsi sebagai spesifikasi peringkat komponen yang berkaitan secara kontekstual dengan keseluruhan sistem AI. Untuk contoh AEBS dalam Rajah 2, ini melibatkan spesifikasi sifat Φ, iaitu untuk mengekalkan jarak minimum dari mana-mana objek semasa gerakan, dari mana kita boleh memperolehi kekangan pada ruang input DNN untuk menangkap secara semantik dalam analisis lawan Ruang input yang bermakna .

3.2 Spesifikasi kuantitatif lwn. spesifikasi Boolean ​

Secara tradisinya, spesifikasi formal cenderung kepada jenis Boolean, yang akan diberikan Tingkah laku sistem dipetakan kepada "benar" atau "salah". Walau bagaimanapun, dalam AI dan ML, spesifikasi sering diberikan sebagai fungsi objektif yang mengawal kos atau ganjaran. Tambahan pula, mungkin terdapat berbilang matlamat, beberapa daripadanya mesti dipenuhi bersama, manakala yang lain mungkin memerlukan pertukaran antara satu sama lain dalam keadaan tertentu. Apakah cara terbaik untuk menyatukan dua pendekatan normatif, Boolean dan kuantitatif? Adakah terdapat formalisme yang secara seragam menangkap sifat umum komponen AI, seperti keteguhan dan keadilan?

Campurkan spesifikasi kuantitatif dan Boolean. Kedua-dua spesifikasi Boolean dan kuantitatif mempunyai kelebihannya: Spesifikasi Boolean lebih mudah untuk dikarang, tetapi fungsi objektif memudahkan pengesahan dan sintesis dengan teknik berasaskan pengoptimuman dan menentukan butiran kepuasan harta benda yang lebih halus. Satu cara untuk merapatkan jurang ini ialah beralih kepada bahasa spesifikasi kuantitatif, seperti menggunakan logik dengan Boolean dan semantik kuantitatif (seperti logik temporal metrik), atau menggabungkan automata dengan fungsi ganjaran untuk RL. Pendekatan lain ialah menggabungkan spesifikasi Boolean dan kuantitatif ke dalam struktur spesifikasi biasa, seperti buku peraturan, di mana spesifikasi boleh disusun, dibandingkan dan diringkaskan dalam struktur hierarki. Penyelidikan telah mengenal pasti beberapa kategori sifat sistem AI, termasuk keteguhan, keadilan, privasi, akauntabiliti dan ketelusan. Penyelidik mencadangkan formalisme baharu yang menghubungkan idea daripada kaedah formal dan ML kepada variasi model sifat ini seperti keteguhan semantik.

3.3 Data lwn. Keperluan Formal​

Pandangan "data ialah spesifikasi "Sangat biasa dalam pembelajaran mesin. Data "sebenar" yang dilabelkan pada set input terhad selalunya merupakan satu-satunya spesifikasi mengenai tingkah laku yang betul. Ini sangat berbeza daripada kaedah formal, yang biasanya diberikan dalam bentuk logik atau automata, yang mentakrifkan set tingkah laku yang betul yang merentasi semua input yang mungkin. Jurang antara data dan norma patut diberi perhatian, terutamanya apabila data adalah terhad, berat sebelah atau datang daripada bukan pakar. Kami memerlukan teknik untuk memformalkan sifat data, kedua-dua data yang tersedia pada masa reka bentuk dan data yang belum ditemui.

Spesifikasi perlombongan. Untuk merapatkan jurang antara data dan spesifikasi formal, kami mencadangkan menggunakan algoritma untuk membuat kesimpulan spesifikasi daripada data dan pemerhatian lain—yang dipanggil teknik perlombongan spesifikasi. Pendekatan jenis ini selalunya boleh digunakan untuk komponen ML, termasuk komponen persepsi, kerana dalam banyak kes ia tidak perlu mempunyai spesifikasi yang tepat atau spesifikasi yang boleh dibaca manusia. Kita juga boleh menggunakan kaedah perlombongan norma untuk menyimpulkan niat manusia dan sifat lain daripada demonstrasi atau bentuk interaksi yang lebih kompleks antara pelbagai ejen (manusia dan AI).

Pemodelan sistem pembelajaran

Dalam kebanyakan aplikasi tradisional pengesahan formal, sistem S adalah tetap dan diketahui pada masa reka bentuk Contohnya, ia boleh menjadi program atau litar yang diterangkan dalam bahasa pengaturcaraan atau bahasa penerangan perkakasan. Masalah pemodelan sistem terutamanya melibatkan pengurangan S kepada saiz yang lebih mudah dikendalikan dengan mengabstrakkan butiran yang tidak berkaitan. Sistem AI membawa cabaran yang sangat berbeza kepada pemodelan sistem, terutamanya berpunca daripada penggunaan pembelajaran mesin:

Ruang input berdimensi tinggi​

Komponen ML untuk persepsi selalunya beroperasi pada ruang input berdimensi sangat tinggi. Sebagai contoh, imej RGB input boleh menjadi 1000 x 600 piksel, yang mengandungi 256 ((1000x600x3)) elemen Input biasanya aliran vektor berdimensi tinggi seperti ini. Walaupun penyelidik telah menggunakan kaedah formal untuk ruang input berdimensi tinggi (seperti dalam litar digital), sifat ruang input untuk persepsi berasaskan ML adalah berbeza .

Parameter/ruang keadaan dimensi tinggi​

Komponen ML seperti deep neural rangkaian mempunyai Ribuan hingga jutaan parameter model dan komponen primitif. Sebagai contoh, DNN tercanggih yang digunakan dalam Rajah 2 mempunyai sehingga 60 juta parameter dan berpuluh-puluh lapisan komponen. Ini mewujudkan ruang carian pengesahan yang besar, dan proses pengabstrakan perlu berhati-hati.

Penyesuaian dan evolusi dalam talian​

Sesetengah sistem pembelajaran, seperti robot menggunakan RL, menyesuaikan diri apabila mereka menghadapi data baharu yang berkembang dengan situasi baru. Untuk sistem sedemikian, pengesahan pada masa reka bentuk mesti mengambil kira evolusi masa depan tingkah laku sistem, atau dilakukan secara berperingkat dalam talian apabila sistem pembelajaran berkembang.

Memodelkan sistem dalam konteks ​

Untuk kebanyakan komponen AI/ML, Spesifikasinya ditakrifkan semata-mata mengikut konteks. Sebagai contoh, untuk mengesahkan keselamatan sistem berasaskan DNN dalam Rajah 2 memerlukan pemodelan persekitaran. Kami memerlukan teknik yang memodelkan komponen ML dan konteksnya supaya sifat yang bermakna secara semantik boleh disahkan.

Dalam beberapa tahun kebelakangan ini, banyak kerja telah menumpukan pada meningkatkan kecekapan untuk mengesahkan keteguhan dan sifat input-output DNN. Walau bagaimanapun, ini tidak mencukupi, kita juga perlu membuat kemajuan dalam tiga aspek berikut:

Abstraksi automatik dan perwakilan yang cekap​

Menjana abstraksi sistem secara automatik telah menjadi kunci kepada kaedah formal dan memainkan peranan penting dalam meluaskan skop kaedah formal kepada sistem perkakasan dan perisian yang besar. Untuk menangani cabaran ruang keadaan campuran ultra-tinggi dimensi dan ruang input untuk sistem berasaskan ML, kita perlu membangunkan teknik yang cekap untuk mengabstraksikan model ML kepada model yang lebih mudah yang lebih sesuai dengan analisis formal. Beberapa arahan yang menjanjikan termasuk: menganalisis DNN menggunakan tafsiran abstrak, membangunkan abstraksi untuk fabrikasi sistem fizikal siber dengan komponen ML dan mereka bentuk perwakilan baharu untuk pengesahan (seperti set bintang).

Penjelasan dan Sebab dan Akibat

Jika pelajar memasukkan dalam ramalan mereka penerangan tentang bagaimana ramalan itu datang daripada data dan pengetahuan konteks, kita boleh memudahkan tugas memodelkan sistem pembelajaran. Idea ini bukanlah sesuatu yang baru, dengan istilah seperti "pengertian berasaskan penjelasan" telah pun dikaji oleh komuniti ML, tetapi baru-baru ini, terdapat minat yang diperbaharui untuk menggunakan logik untuk menerangkan output sistem pembelajaran. Penjanaan penjelasan membantu menyahpepijat reka bentuk dan spesifikasi pada masa reka bentuk dan membantu mensintesis sistem AI teguh yang memberikan jaminan pada masa jalan. ML termasuk penaakulan kausal dan kontrafaktual juga boleh membantu menjana penjelasan untuk kaedah formal.

Ruang ciri semantik​

Apabila input dan contoh balas yang dihasilkan adalah analisis Adversarial dan pengesahan formal model ML lebih masuk akal apabila konteks di mana model ML digunakan mempunyai makna semantik. Contohnya, teknik yang menganalisis pengesan objek DNN untuk perubahan kecil dalam warna kereta atau masa dalam sehari adalah lebih berguna daripada teknik yang menambah hingar pada sebilangan kecil piksel yang dipilih secara sewenang-wenangnya. Pada masa ini, kebanyakan kaedah gagal pada ketika ini. Kami memerlukan analisis permusuhan semantik, iaitu, menganalisis model ML dalam konteks sistem yang dimilikinya. Langkah utama ialah mewakili ruang ciri semantik yang memodelkan persekitaran di mana sistem ML beroperasi, dan bukannya ruang ciri khusus yang mentakrifkan ruang input untuk model ML. Ini selaras dengan gerak hati bahawa ruang terpendam yang dibentuk oleh bahagian ruang ciri konkrit yang bermakna secara semantik (seperti imej pemandangan lalu lintas) adalah jauh lebih rendah daripada ruang ciri konkrit yang lengkap. Ruang ciri semantik dalam Rajah 2 ialah ruang berdimensi rendah yang mewakili dunia 3D di sekeliling kenderaan autonomi, manakala ruang ciri khusus ialah ruang piksel berdimensi tinggi. Memandangkan dimensi ruang ciri semantik adalah lebih rendah, ia boleh dicari dengan lebih mudah. Walau bagaimanapun, kami juga memerlukan "penyampai" yang memetakan titik dalam ruang ciri semantik ke titik dalam ruang ciri konkrit. Sifat pemapar, seperti kebolehbezaan, menjadikannya lebih mudah untuk menggunakan kaedah formal untuk melakukan carian berorientasikan matlamat bagi ruang ciri semantik.

Enjin pengiraan untuk reka bentuk dan pengesahan

Keberkesanan kaedah formal untuk sistem perkakasan dan perisian ditentukan oleh "enjin pengiraan" yang mendasarinya dengan kemajuan dalam - contohnya, Penyelesaian Kepuasan Boolean (SAT), Teori Modular Kepuasan (SMT) dan semakan model. Memandangkan skala sistem AI/ML, kerumitan alam sekitar dan spesifikasi baru yang terlibat, kelas enjin pengiraan baharu diperlukan untuk latihan, ujian, reka bentuk dan pengesahan yang cekap dan berskala, cabaran utama yang mesti diatasi untuk mencapai kemajuan ini.

5.1 Reka Bentuk Set Data​

Data ialah titik permulaan asas untuk pembelajaran mesin untuk meningkatkan kualiti sistem ML. anda mesti meningkatkan perkara yang dipelajari Kualiti data. Bagaimanakah kaedah formal boleh membantu dalam pemilihan sistematik, reka bentuk dan pengayaan data ML?

Penjanaan data untuk ML mempunyai persamaan dengan masalah penjanaan ujian untuk perkakasan dan perisian. Kaedah formal telah terbukti berkesan untuk penjanaan ujian berasaskan kekangan yang sistematik, tetapi ini berbeza daripada keperluan untuk sistem kecerdasan buatan, di mana jenis kekangan boleh menjadi lebih kompleks - contohnya, untuk penggunaan penderia untuk mengekstrak data daripada persekitaran yang kompleks seperti sebagai keadaan trafik) untuk mengekod keperluan bagi "ketulenan" data yang ditangkap. Kami bukan sahaja perlu menjana item data dengan ciri khusus (seperti ujian yang mencari pepijat), tetapi kami juga perlu menjana koleksi yang memenuhi kekangan pengedaran penjanaan data mesti memenuhi saiz set data dan matlamat kepelbagaian untuk latihan dan generalisasi yang berkesan; Keperluan ini memerlukan pembangunan set baru teknik formal.

Rawak terkawal dalam kaedah formal. Terdapat banyak aspek kepada masalah reka bentuk dataset ini Pertama, ruang input "sah" mesti ditakrifkan supaya contoh dibentuk dengan betul mengikut semantik aplikasi kedua, kekangan pada ukuran persamaan dengan keperluan data dunia sebenar ditangkap; ketiga, selalunya terdapat keperluan untuk menjana Pengedaran contoh dikekang untuk mendapatkan jaminan bahawa algoritma pembelajaran menumpu kepada konsep sebenar.

Kami percaya aspek ini boleh ditangani dengan kaedah formal stokastik - algoritma stokastik untuk menjana data tertakluk kepada kekangan formal dan keperluan pengedaran. Kelas teknik baharu yang menjanjikan dipanggil improvisasi terkawal, yang menghasilkan rentetan rawak (contoh) x yang memenuhi tiga kekangan:

• Kekangan keras yang mentakrifkan ruang x yang sah
• Kekangan lembut yang mentakrifkan bagaimana x yang dihasilkan mesti menyerupai contoh dunia sebenar
• Mentakrifkan keperluan stokastik untuk kekangan pengagihan output

Pada masa ini, teori improvisasi kawalan masih di peringkat awal, kami baru bermula untuk memahami kerumitan pengiraan dan reka bentuk algoritma yang cekap. Penambahbaikan, sebaliknya, bergantung pada kemajuan terkini dalam masalah pengiraan seperti pensampelan rawak terhad, pengiraan model, dan kaedah generatif berdasarkan pengaturcaraan kemungkinan.

5.2 Pengesahan Kuantitatif​

Selain penunjuk tradisional (nyatakan dimensi ruang, komponen Kuantiti, dsb.) Di luar mengukur saiz sistem AI, jenis komponen boleh menjadi lebih kompleks. Sebagai contoh, kenderaan autonomi dan separa autonomi dan pengawalnya mesti dimodelkan sebagai sistem hibrid, menggabungkan dinamik diskret dan berterusan tambahan pula, wakil dalam persekitaran (manusia, kenderaan lain) mungkin perlu dimodelkan sebagai proses kebarangkalian; Akhir sekali, keperluan mungkin melibatkan bukan sahaja spesifikasi Boolean tradisional mengenai keselamatan dan keaktifan, tetapi juga keperluan kuantitatif mengenai keteguhan dan prestasi sistem, namun kebanyakan kaedah pengesahan sedia ada bertujuan untuk menjawab soalan pengesahan Boolean. Untuk menangani jurang ini, enjin berskala baharu untuk pengesahan kuantitatif mesti dibangunkan.

Analisis semantik kuantitatif. Secara umum, kerumitan dan kepelbagaian sistem AI bermakna pengesahan rasmi berkanun (Boolean atau kuantitatif) tidak dapat ditentukan—sebagai contoh, walaupun menentukan sama ada keadaan sistem hibrid linear boleh dicapai adalah tidak dapat ditentukan. Untuk mengatasi halangan yang ditimbulkan oleh kerumitan pengiraan ini, seseorang mesti menggunakan teknik baru pengesahan kebarangkalian dan kuantitatif pada ruang ciri semantik untuk meningkatkan pendekatan abstraksi dan pemodelan yang dibincangkan sebelum ini dalam bahagian ini. Untuk formalisme kanonik dengan kedua-dua semantik Boolean dan kuantitatif, dalam formalisme seperti logik masa metrik, merumuskan pengesahan sebagai pengoptimuman adalah penting untuk menyatukan kaedah pengiraan daripada kaedah formal dan kaedah pengiraan daripada literatur pengoptimuman. Contohnya dalam pemalsuan logik temporal berasaskan simulasi, walaupun ia mesti digunakan pada ruang ciri semantik untuk kecekapan, teknik pemalsuan tersebut juga boleh digunakan untuk menjana data latihan secara sistematik dan bertentangan untuk komponen ML. Teknik untuk pengesahan kebarangkalian harus melangkaui bentuk tradisional seperti rantai Markov atau MDP untuk mengesahkan program kebarangkalian pada ruang ciri semantik. Begitu juga, kerja pada penyelesaian SMT mesti dilanjutkan untuk mengendalikan kekangan kos dengan lebih cekap—dengan kata lain, menggabungkan penyelesaian SMT dengan kaedah pengoptimuman.

Kita perlu memahami perkara yang boleh dijamin pada masa reka bentuk, bagaimana proses reka bentuk menyumbang kepada operasi yang selamat pada masa larian, dan bagaimana masa reka bentuk dan teknologi masa jalan boleh Kebolehoperasian secara berkesan.

5.3 Penaakulan Gabungan untuk AI/ML​

Untuk pendekatan formal yang menskalakan kepada sistem besar, penaakulan gabungan (modular) adalah penting. Dalam pengesahan komposisi, sistem besar (cth., atur cara) dipecahkan kepada komponennya (cth., atur cara), setiap komponen disahkan terhadap spesifikasi, dan kemudian spesifikasi komponen diambil bersama untuk menghasilkan spesifikasi peringkat sistem. Pendekatan biasa untuk pengesahan gabungan ialah menggunakan kontrak jaminan-andaian Sebagai contoh, sesuatu proses menganggap sesuatu tentang keadaan permulaannya (prasyarat), yang seterusnya menjamin keadaan akhir (postconditions Paradigma jaminan-andaian yang serupa telah digunakan Develop). dan menggunakan sistem perisian dan perkakasan serentak.

Walau bagaimanapun, paradigma ini tidak meliputi sistem kecerdasan buatan, sebahagian besarnya disebabkan oleh fakta bahawa sistem kecerdasan buatan dibincangkan dalam penyeragaman bahagian "Spesifikasi Formal". cabaran. Pengesahan boleh gubah memerlukan spesifikasi gubahan—iaitu, komponen mesti boleh diformalkan. Walau bagaimanapun, seperti yang diterangkan dalam "Spesifikasi Formal", mungkin tidak mungkin untuk menentukan secara rasmi kelakuan yang betul bagi komponen persepsi. Oleh itu, salah satu cabaran adalah untuk membangunkan teknik penaakulan kombinatorial yang tidak bergantung kepada mempunyai spesifikasi gabungan yang lengkap. Tambahan pula, sifat kuantitatif dan kebarangkalian sistem AI memerlukan pengembangan teori penaakulan gabungan kepada sistem dan spesifikasi kuantitatif.

Simpulkan kontrak komponen. Reka bentuk gabungan dan analisis sistem AI memerlukan kemajuan dalam pelbagai bidang. Pertama, terdapat keperluan untuk membina beberapa kerja awal yang menjanjikan untuk membangunkan teori untuk reka bentuk dan pengesahan jaminan kebarangkalian untuk ruang semantik sistem ini. Kedua, teknik sintesis induktif baharu mesti direka untuk menjana kontrak jaminan hipotesis secara algoritma yang mengurangkan beban normatif dan memudahkan penaakulan gabungan. Ketiga, untuk mengendalikan kes seperti persepsi di mana komponen tidak mempunyai spesifikasi formal yang tepat, kami mencadangkan teknik untuk membuat kesimpulan kekangan peringkat komponen daripada analisis peringkat sistem dan menggunakan kekangan tersebut untuk memfokuskan analisis peringkat komponen, termasuk analisis lawan, pada carian Enter bahagian ruang yang "berkaitan".

Pembetulan sistem pintar semasa ia dibina

Dalam dunia yang ideal, pengesahan akan disepadukan dengan proses reka bentuk, jadi sistem itu "dalam pembinaan" Dibetulkan". Sebagai contoh, pengesahan boleh disisipkan dengan langkah kompilasi/sintesis, dengan mengandaikan aliran reka bentuk tahap pemindahan daftar (RTL) biasa dalam litar bersepadu, dan mungkin ia boleh disepadukan ke dalam algoritma sintesis untuk memastikan pelaksanaan memenuhi spesifikasi. Bolehkah kita mereka bentuk proses reka bentuk yang sesuai untuk sistem kecerdasan buatan yang disemak secara beransur-ansur semasa pembinaan?

6.1 Reka bentuk dipacu spesifikasi komponen ML

Memandangkan spesifikasi rasmi, bolehkah kita mereka bentuk mesin Demonstrate a komponen pembelajaran (model) yang memenuhi spesifikasi ini? Terdapat banyak aspek untuk reka bentuk komponen ML baharu ini: (1) mereka bentuk set data, (2) mensintesis struktur model, (3) menjana set ciri yang mewakili, (4) mensintesis hiperparameter dan pilihan lain aspek algoritma ML, dan (5) teknik untuk mengautomasikan penyahpepijatan model atau spesifikasi ML apabila sintesis gagal.

Sintesis formal komponen ML. Penyelesaian kepada beberapa masalah yang disenaraikan sebelum ini muncul Sifat boleh dikuatkuasakan pada model ML menggunakan fungsi kehilangan semantik atau keteguhan yang diperakui Teknik ini boleh digabungkan dengan kaedah seperti carian seni bina saraf untuk menghasilkan model yang dibina dengan betul. Pendekatan lain adalah berdasarkan kepada teori yang muncul bagi sintesis induktif formal, iaitu, sintesis daripada contoh program yang memenuhi spesifikasi formal. Cara paling biasa untuk menyelesaikan masalah sintesis induktif formal ialah menggunakan pendekatan berpandukan oracle, di mana pelajar dipasangkan dengan oracle yang menjawab pertanyaan seperti dalam Rajah 2 dalam contoh, oracle boleh menjadi pemalsu yang menjana contoh balas itu menunjukkan bagaimana komponen pembelajaran gagal Pelanggaran spesifikasi peringkat sistem. Akhir sekali, menggunakan teorem yang membuktikan untuk memastikan ketepatan algoritma yang digunakan untuk melatih model ML juga merupakan langkah penting ke arah membina komponen ML yang diubah suai.

6.2 Reka bentuk sistem berdasarkan pembelajaran mesin ​

Cabaran kedua ialah Reka bentuk a sistem holistik yang merangkumi komponen pembelajaran dan bukan pembelajaran. Beberapa persoalan kajian telah timbul: Bolehkah kita mengira had selamat di mana komponen ML boleh dihadkan untuk beroperasi? Bolehkah kita mereka bentuk algoritma kawalan atau perancangan yang mengatasi batasan komponen sedar ML yang diterimanya sebagai input? Bolehkah kita mencipta teori reka bentuk gabungan untuk sistem kecerdasan buatan? Apabila dua model ML digunakan untuk mengesan dua jenis data penderia yang berbeza (cth., LiDAR dan imej visual), dan setiap model memenuhi spesifikasinya di bawah andaian tertentu, dalam keadaan apakah kedua-duanya boleh digunakan bersama untuk Meningkatkan kebolehpercayaan sistem secara keseluruhan?

Contoh kemajuan yang menonjol dalam cabaran ini ialah kerja kawalan berasaskan pembelajaran yang selamat. Pendekatan ini pra-mengira sampul keselamatan dan menggunakan algoritma pembelajaran untuk menala pengawal dalam sampul surat itu, yang memerlukan teknik untuk mengira sampul keselamatan sedemikian dengan cekap berdasarkan, sebagai contoh, analisis kebolehcapaian, bidang RL Kemajuan penting juga telah dibuat .

Walau bagaimanapun, ini tidak menangani sepenuhnya cabaran yang ditimbulkan oleh pembelajaran mesin untuk persepsi dan ramalan - contohnya, pembelajaran peneguhan mendalam hujung ke hujung yang selamat telah belum dapat dicapai.

6.3 Merapatkan masa reka bentuk dan masa jalan untuk AI yang berdaya tahan ​

Seperti dalam “Persekitaran Seperti yang dibincangkan dalam bahagian Pemodelan, banyak sistem AI beroperasi dalam persekitaran yang tidak boleh ditentukan secara priori, jadi akan sentiasa ada persekitaran di mana ketepatan tidak dapat dijamin. Teknologi yang melaksanakan toleransi kesalahan dan pemulihan ralat pada masa jalan memainkan peranan penting dalam sistem kecerdasan buatan. Kami memerlukan pemahaman yang sistematik tentang perkara yang boleh dijamin pada masa reka bentuk, cara proses reka bentuk menyumbang kepada operasi sistem AI yang selamat dan betul semasa masa jalan, dan cara teknologi masa reka bentuk dan masa jalan boleh saling beroperasi dengan berkesan.

Dalam hal ini, literatur tentang sistem toleran kesalahan dan boleh dipercayai memberi kita asas untuk membangunkan teknik jaminan masa jalan – iaitu, pengesahan masa jalan dan teknik pengurangan ; cth. Pendekatan Simplex menyediakan cara untuk menggabungkan modul yang kompleks tetapi mudah ralat dengan modul sandaran yang selamat dan disahkan secara rasmi. Baru-baru ini, teknik yang menggabungkan pendekatan jaminan masa reka bentuk dan masa jalan telah menunjukkan bahawa komponen yang tidak disahkan, termasuk yang berdasarkan AI dan ML, boleh dibungkus dalam rangka kerja jaminan masa jalan untuk memberikan jaminan operasi yang selamat. Tetapi pada masa ini ini terhad kepada kelas sistem tertentu, atau mereka memerlukan reka bentuk manual pemantau masa jalan dan strategi mitigasi Terdapat lebih banyak pendekatan yang akan datang seperti pemodelan persekitaran introspektif, pemantau berasaskan kecerdasan buatan dan sintesis strategi sandaran yang selamat. Banyak kerja yang perlu dilakukan.

Pendekatan reka bentuk untuk mengubah suai sistem pintar dalam pembinaan yang dibincangkan di sini mungkin memperkenalkan overhed yang menjadikannya lebih sukar untuk memenuhi keperluan prestasi dan masa nyata. Tetapi kami percaya (mungkin bertentangan dengan intuisi) bahawa kaedah formal malah boleh membantu meningkatkan prestasi atau kecekapan tenaga sistem dalam erti kata berikut.

Penalaan prestasi tradisional cenderung kepada konteks-agnostik – contohnya, tugasan perlu memenuhi tarikh akhir secara bebas daripada persekitaran di mana tugasan itu dijalankan. Tetapi jika persekitaran ini dicirikan secara rasmi pada masa reka bentuk, dipantau pada masa jalan, dan jika operasi sistem mereka disahkan secara rasmi sebagai selamat, maka dalam persekitaran sedemikian, model ML boleh menukar ketepatan untuk kecekapan yang lebih tinggi. Pertukaran ini mungkin merupakan bidang yang bermanfaat untuk penyelidikan masa depan.

Kesimpulan

Dari perspektif kaedah formal, kami membedah masalah mereka bentuk sistem kecerdasan buatan jaminan tinggi. Seperti yang ditunjukkan dalam Rajah 3, kami mengenal pasti lima cabaran utama dalam menggunakan kaedah formal pada sistem AI dan membangunkan tiga prinsip reka bentuk dan pengesahan untuk setiap lima cabaran yang berpotensi untuk menangani cabaran ini.

Tepi dalam Rajah 3 menunjukkan kebergantungan antara prinsip ini, seperti jaminan masa jalan yang bergantung pada introspeksi dan pemodelan persekitaran dipacu data untuk mengekstrak andaian boleh dipantau dan model persekitaran . Begitu juga, untuk melaksanakan analisis peringkat sistem, kita perlu melibatkan diri dalam penaakulan gabungan dan abstraksi, di mana sesetengah komponen AI mungkin memerlukan spesifikasi perlombongan manakala yang lain menjana struktur yang betul melalui sintesis induktif formal.

Beberapa penyelidik, termasuk pengarang, telah mengusahakan cabaran ini sejak 2016, apabila versi asal artikel ini yang diterbitkan memperkenalkan beberapa contoh kemajuan. Kami telah membangunkan alat sumber terbuka VerifAI dan Scenic yang melaksanakan teknik berdasarkan prinsip yang diterangkan dalam artikel ini dan telah digunakan pada sistem berskala industri dalam pemanduan autonomi dan aeroangkasa. Keputusan ini hanyalah permulaan, dan banyak lagi yang perlu dilakukan. AI yang boleh disahkan dijangka akan terus menjadi bidang penyelidikan yang bermanfaat pada tahun-tahun akan datang.

Atas ialah kandungan terperinci Ke Arah AI Boleh Disahkan: Lima Cabaran Kaedah Formal. Untuk maklumat lanjut, sila ikut artikel berkaitan lain di laman web China PHP!