AI sekali lagi terlibat dalam dunia matematik, dan kaedah DSP baharu menggandakan kadar kejayaan bukti mesin

Teorem matematik yang membuktikan secara automatik ialah niat asal kecerdasan buatan dan sentiasa menjadi masalah yang sukar. Setakat ini, ahli matematik manusia telah menggunakan dua cara yang berbeza untuk menulis matematik.

Pertama ialah kaedah yang biasa digunakan oleh semua orang, iaitu menggunakan bahasa semula jadi untuk menerangkan pembuktian matematik. Kebanyakan matematik ditulis dengan cara ini, termasuk buku teks matematik, kertas matematik, dsb.

Jenis kedua dipanggil matematik formal. Ini adalah alat yang dicipta oleh saintis komputer sejak setengah abad yang lalu untuk menyemak bukti matematik.

Nampaknya hari ini komputer boleh digunakan untuk mengesahkan bukti matematik, tetapi mereka hanya boleh melakukannya menggunakan bahasa bukti direka khas yang tidak boleh mengendalikan simbol matematik dan campuran teks bertulis yang digunakan oleh ahli matematik. Menukar masalah matematik yang ditulis dalam bahasa semula jadi kepada kod formal supaya komputer lebih mudah menyelesaikannya boleh membantu membina mesin yang boleh meneroka penemuan baharu dalam matematik. Proses ini dipanggil pemformalisasi, dan autoformalisasi merujuk kepada tugas menterjemah secara automatik matematik daripada bahasa semula jadi ke dalam bahasa formal.

Mengautomasi pembuktian formal ialah tugas yang mencabar, dan kaedah pembelajaran mendalam masih belum mencapai kejayaan besar dalam bidang ini, terutamanya disebabkan oleh kekurangan data formal. Malah, pembuktian rasmi itu sendiri sangat sukar dan hanya beberapa pakar yang boleh melakukannya, yang menjadikan usaha anotasi berskala besar tidak realistik. Korpus pembuktian rasmi terbesar ditulis dalam kod Isabelle (Paulson, 1994) dan bersaiz kurang daripada 0.6GB, susunan magnitud lebih kecil daripada set data yang biasa digunakan dalam penglihatan atau pemprosesan bahasa semula jadi. Untuk menangani kekurangan bukti formal, kajian terdahulu telah mencadangkan menggunakan data sintetik, pembelajaran penyeliaan sendiri atau pengukuhan untuk mensintesis data latihan formal tambahan. Walaupun kaedah ini mengurangkan kekurangan data pada tahap tertentu, kaedah ini tidak dapat menggunakan sepenuhnya pembuktian matematik yang ditulis secara manual.

Mari kita ambil model bahasa Minerva sebagai contoh. Selepas latihan dengan data yang mencukupi, kami mendapati bahawa keupayaan matematiknya sangat kuat dan ia boleh mendapat markah yang lebih tinggi daripada purata dalam ujian matematik sekolah menengah. Walau bagaimanapun, model bahasa sebegini juga mempunyai kekurangan Ia hanya boleh meniru, tetapi tidak boleh melatih secara bebas untuk meningkatkan matematik. Sistem bukti formal menyediakan persekitaran latihan, tetapi terdapat sangat sedikit data untuk matematik formal.

Tidak seperti matematik formal, data matematik tidak formal banyak dan tersedia secara meluas. Baru-baru ini, model bahasa besar yang dilatih pada data matematik tidak formal telah menunjukkan keupayaan penaakulan kuantitatif yang mengagumkan. Walau bagaimanapun, mereka sering menghasilkan bukti yang salah, dan secara automatik mengesan alasan yang salah dalam bukti ini adalah mencabar.

Dalam karya baru-baru ini, penyelidik seperti Yuhuai Tony Wu daripada Google telah mereka kaedah baharu yang dipanggil DSP (Draf, Lakar dan Buktikan). kedua-dua ketegasan logik yang disediakan oleh sistem formal dan sejumlah besar data tidak formal.

Pautan kertas: https://arxiv.org/pdf/2210.12283.pdf

Awal tahun ini, Wu Yuhuai dan beberapa rakan usaha sama menggunakan rangkaian saraf OpenAI Codex untuk melaksanakan kerja pemformalkan automatik, menunjukkan bahawa model bahasa yang besar boleh digunakan untuk menterjemah kenyataan tidak formal secara automatik kepada Kebolehlaksanaan kenyataan rasmi. DSP melangkah lebih jauh, menggunakan model bahasa yang besar untuk menghasilkan lakaran bukti formal daripada bukti tidak formal. Lakaran bukti terdiri daripada langkah-langkah penaakulan aras tinggi yang boleh ditafsirkan oleh sistem formal seperti prover teorem interaktif. Ia berbeza daripada bukti rasmi yang lengkap kerana ia mengandungi urutan sangkaan pertengahan yang tidak wajar. Dalam langkah terakhir DSP, lakaran bukti formal dihuraikan menjadi bukti rasmi yang lengkap, menggunakan pengesah automatik untuk membuktikan semua sangkaan pertengahan.

Wu Yuhuai berkata: Sekarang, kami telah menunjukkan bahawa LLM boleh menukar bukti tidak rasmi yang dijananya kepada bukti rasmi yang disahkan!

Kaedah

Bahagian Kaedah menerangkan kaedah DSP untuk automasi bukti formal, yang menggunakan pembuktian tidak formal untuk membimbing pembuktian teorem rasmi automatik Lakaran bukti peranti. Diandaikan di sini bahawa setiap masalah mempunyai proposisi tidak formal dan proposisi formal yang menerangkan masalah tersebut. Saluran paip keseluruhan terdiri daripada tiga peringkat (ditunjukkan dalam Rajah 1).

Rajah 1.

Bukti tidak rasmi Peringkat permulaan merangka pendekatan

DSP melibatkan mencari bukti tidak formal bagi masalah berdasarkan penerangannya dalam bahasa matematik semula jadi (mungkin menggunakan LATEX). Bukti tidak rasmi yang terhasil dianggap sebagai draf kasar untuk peringkat seterusnya. Dalam buku teks matematik, bukti teorem biasanya disediakan, tetapi kadangkala ia hilang atau tidak lengkap. Oleh itu, penyelidik mempertimbangkan dua situasi yang sepadan dengan kehadiran atau ketiadaan bukti tidak rasmi.

Dalam kes pertama, penyelidik mengandaikan bahawa terdapat bukti tidak formal "sebenar" (iaitu, bukti yang ditulis oleh manusia), yang merupakan amalan formal teori matematik sedia ada. situasi tipikal. Dalam kes kedua, penyelidik membuat andaian yang lebih umum bahawa tiada bukti tidak formal sebenar diberikan, dan menggunakan model bahasa besar yang dilatih pada data matematik tidak formal untuk merangka calon bukti. Model bahasa menghapuskan pergantungan pada bukti manusia dan boleh menjana pelbagai penyelesaian alternatif untuk setiap masalah. Walaupun tiada cara mudah untuk mengesahkan ketepatan bukti ini secara automatik, bukti tidak formal hanya perlu berguna pada peringkat seterusnya dalam menghasilkan lakaran bukti formal yang baik.

Peta bukti tidak rasmi ke dalam lakaran formal

Lakaran bukti rasmi mengekod struktur penyelesaian dan mengetepikan butiran peringkat rendah. Secara intuitif, ia adalah bukti separa yang menggariskan pernyataan tekaan peringkat tinggi. Rajah 2 ialah contoh konkrit lakaran bukti. Walaupun pembuktian tidak formal sering mengetepikan butiran peringkat rendah, butiran ini tidak boleh dikecualikan dalam pembuktian formal, menjadikan penukaran langsung bukti tidak rasmi kepada bukti formal sukar. Sebaliknya, kertas kerja ini mencadangkan pemetaan bukti tidak formal pada lakaran bukti rasmi yang berkongsi struktur aras tinggi yang sama. Butiran peringkat rendah yang hilang daripada lakaran bukti boleh diisi oleh prover automatik. Memandangkan korpora selari tidak formal-formal besar tidak wujud, kaedah terjemahan mesin standard tidak sesuai untuk tugas ini. Sebaliknya, keupayaan pembelajaran beberapa pukulan model bahasa yang besar digunakan di sini. Khususnya, beberapa pasangan contoh yang mengandungi bukti tidak rasmi dan lakaran rasmi yang sepadan digunakan untuk menggesa model, diikuti dengan bukti tidak rasmi untuk ditukar, dan kemudian biarkan model menjana token seterusnya untuk mendapatkan lakaran formal yang diperlukan. Model ini dipanggil "pemformal automatik".

Rajah 2.

Bukti pendedahan dalam lakaran Konjektur

Sebagai bahagian akhir proses ini, penyelidik melaksanakan prover automatik di luar rak untuk mengisi butiran yang hilang dalam lakaran bukti Istilah "prover automatik" di sini merujuk kepada keupayaan untuk menghasilkan bukti yang boleh disahkan secara rasmi. Rangka kerja adalah agnostik kepada pilihan khusus prover automatik: ia boleh menjadi prover simbolik (seperti alat automasi bukti heuristik), prover berasaskan rangkaian saraf, atau pendekatan hibrid. Jika prover automatik berjaya mengisi semua jurang dalam lakaran bukti, ia mengembalikan bukti rasmi akhir yang boleh disemak berdasarkan spesifikasi masalah. Jika prover automatik gagal (contohnya, ia melebihi had masa yang diperuntukkan), penilaian dianggap tidak berjaya.

Eksperimen

Para penyelidik menjalankan satu siri eksperimen, termasuk bukti formal masalah yang dijana daripada set data miniF2F, dan menunjukkan bahawa sebahagian besar teorem boleh dibuktikan secara automatik menggunakan kaedah ini. Dua persekitaran dikaji di sini, di mana bukti tidak formal ditulis oleh manusia atau dirangka oleh model bahasa besar yang dilatih pada teks matematik. Kedua-dua tetapan ini sesuai dengan situasi yang sering berlaku dalam pemformalkan teori yang sedia ada, iaitu, selalunya terdapat bukti tidak rasmi, tetapi ia kadang-kadang dibiarkan sebagai latihan kepada pembaca, atau hilang kerana kekangan di pinggir.

Jadual 1 menunjukkan bahagian bukti rasmi yang berjaya ditemui pada set data miniF2F. Hasilnya termasuk empat garis dasar daripada eksperimen kami, serta kaedah DSP dengan bukti tulisan manusia dan bukti yang dijana model.

Ia boleh dilihat bahawa prover automatik dengan 11 strategi heuristik telah banyak meningkatkan prestasi Sledgehammer kadar kejayaan daripada 9.9% kepada 18.0% pada set pengesahan dan daripada 10.4% kepada 20.9% pada set ujian. Dua garis dasar menggunakan model bahasa dan carian bukti mencapai kadar kejayaan masing-masing sebanyak 29.9% dan 35.2% pada set ujian miniF2F.

Berdasarkan bukti tidak rasmi yang ditulis oleh manusia, pendekatan DSP mencapai kadar kejayaan 42.6% dan 39.3% pada set pengesahan dan ujian miniF2F. Sebanyak 200 daripada 488 masalah boleh dibuktikan dengan cara ini. Model Codex dan model Minerva (8B) memberikan hasil yang hampir sama apabila menyelesaikan masalah pada miniF2F: kedua-duanya membimbing pengesah automatik untuk menyelesaikan 40.6% dan 35.3% masalah pada set pengesahan dan ujian masing-masing.

Apabila bertukar kepada model Minerva (62B), kadar kejayaan meningkat masing-masing kepada 43.9% dan 37.7%. Berbanding dengan bukti tidak rasmi yang ditulis manusia, kadar kejayaannya adalah 1.3% lebih tinggi pada set pengesahan dan 1.6% lebih rendah pada set ujian. Secara keseluruhan, model Minerva (62B) dapat menyelesaikan 199 masalah pada miniF2F, satu kurang daripada bukti bertulis manusia. Model Minerva (540B) menyelesaikan 42.6% dan 38.9% masalah dalam set pengesahan dan set ujian miniF2F, masing-masing, dan juga menghasilkan 199 bukti yang berjaya.

Kaedah DSP membimbing pembukti automatik secara berkesan dalam kedua-dua kes: pembuktian tidak formal menggunakan manusia atau pembuktian tidak formal yang dihasilkan oleh model bahasa. DSP hampir menggandakan kadar kejayaan prover dan menghasilkan prestasi SOTA pada miniF2F menggunakan Isabelle. Tambahan pula, model Minerva yang lebih besar hampir sama membantu manusia dalam membimbing peribahasa rasmi automatik.

Seperti yang ditunjukkan dalam rajah di bawah, kaedah DSP meningkatkan prestasi Sledgehammer + heuristik prover dengan ketara (~20% -> ~40%), mencapai SOTA baharu pada miniF2F .

Minerva versi 62B dan 540B menjana bukti yang hampir serupa dengan bukti manusia.

Untuk maklumat lanjut, sila rujuk kertas asal.

Atas ialah kandungan terperinci AI sekali lagi terlibat dalam dunia matematik, dan kaedah DSP baharu menggandakan kadar kejayaan bukti mesin. Untuk maklumat lanjut, sila ikut artikel berkaitan lain di laman web China PHP!