Dengan menukar masalah matematik kepada kod, penyelidikan Google telah meningkatkan ketepatan pembuktian mesin.

Komputer telah digunakan untuk mengesahkan pembuktian matematik untuk beberapa lama, tetapi mereka hanya dapat melakukannya jika masalah disediakan menggunakan bahasa pembuktian yang direka khas dan tidak dapat mengendalikan campuran notasi matematik dan teks bertulis yang digunakan oleh ahli matematik .

Jika anda menukar masalah matematik yang ditulis dalam bahasa semula jadi kepada kod formal dan memudahkan komputer untuk menyelesaikannya, ini mungkin membantu membina mesin yang boleh meneroka penemuan baharu dalam matematik.

Proses ini dipanggil pemformalkan, tetapi hanya pembuktian boleh mengambil masa bertahun-tahun, jadi hanya sebahagian kecil pengetahuan matematik diformalkan dan kemudian dibuktikan oleh mesin.

Autoformalisasi merujuk kepada tugas menerjemahkan matematik secara automatik daripada bahasa semula jadi kepada bahasa formal . Implikasi praktikal dan falsafah daripada alat pemformalkan automatik yang berjaya akan menjadi sangat besar, ia boleh mengurangkan kos pemformalan yang berlebihan semasa, dan dalam jangka panjang, ia boleh menghubungkan aspek automatik penaakulan matematik dalam pelbagai bidang penyelidikan.

Dalam kajian baru-baru ini, Yuhuai Wu dari Google dan rakan usaha samanya menggunakan rangkaian saraf daripada OpenAI Codex untuk mengautomasikan kerja pemformalkan . Codex telah dilatih mengenai sejumlah besar teks dan data pengaturcaraan daripada web, dan pengaturcara boleh menggunakannya untuk menjana kod yang boleh dipercayai.

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

Memformalkan 12,500 masalah pertandingan matematik sekolah menengah

Satu siri kemajuan terkini dalam model bahasa berskala besar menunjukkan potensi model untuk memahami bahasa formal. Walau bagaimanapun, kejayaan sedia ada terhad kepada bahasa formal (seperti Python) yang wujud korpora besar di web. Sebaliknya, data matematik formal sangat terhad. Salah satu perpustakaan bahasa matematik rasmi terbesar, Arkib Bukti Formal, hanya bersaiz 180mb, iaitu kurang daripada 0.18% daripada data latihan model bahasa besar Codex.

Tambahan pula, tidak seperti kes untuk bahasa pengaturcaraan tujuan umum, di mana docstring bahasa semula jadi tersedia secara meluas, terdapat sedikit penjajaran data antara bahasa semula jadi dan bahasa matematik formal. Oleh itu, masih tidak diketahui sama ada kejayaan model bahasa berskala besar secara langsung boleh menggalakkan pembangunan pemformalkan automatik.

Memandangkan persamaan antara bahasa bukti dan bahasa pengaturcaraan, pasukan memutuskan untuk melihat sama ada Codex boleh merasmikan perpustakaan 12,500 masalah pertandingan matematik sekolah menengah. Ia mampu menukar satu perempat daripada masalah kepada format yang serasi dengan penyelesai bukti formal Isabelle.

Wu menyatakan bahawa banyak transformasi yang tidak berjaya adalah akibat sistem tidak memahami konsep matematik tertentu. "Jika anda menunjukkan model dengan contoh yang menerangkan konsep, maka model itu boleh memahaminya dengan cepat."

Kerja ini meneroka prospek pemformalkan automatik model bahasa besar mempunyai keupayaan yang cukup baik untuk memformalkan matematik bahasa semula jadi dalam prover teorem interaktif.

Rajah 1 di bawah ialah contoh sempurna pemformalkan automatik. Model bukan sahaja menukar kod Isabelle yang betul secara sintaksis, ia juga mampu menangkap titik penaakulan penting dalam bahasa semula jadi.

Untuk menguji keberkesanan prosedur pemformalan automatik ini, pasukan itu kemudiannya menggunakan Codex kepada satu set masalah yang sudah mempunyai versi rasmi manusia, yang mana Codex turut dijana Dibangunkan versi rasminya sendiri. Pasukan itu menggunakan AI lain yang dipanggil MiniF2F untuk menyelesaikan kedua-dua versi masalah.

Memformalkan masalah secara automatik meningkatkan kadar kejayaan MiniF2F daripada 29% kepada 35%, menunjukkan bahawa Codex telah mencapai kemajuan penting dalam pemformalkan masalah.

Perlu diperhatikan bahawa pembentangan untuk banyak pertandingan matematik cenderung berbentuk: seseorang diminta untuk mencari jawapan kepada masalah tertentu, dan bukannya membuktikan cadangan yang diberikan . Walau bagaimanapun, pernyataan matematik formal adalah dalam bentuk proposisi, bukan soalan.

Untuk menukar soalan kepada cadangan, penyelidik melampirkan "Jawapan Akhir" selepas soalan:

untuk pemformalkan automatik Format segera ialah :

Adakah AI akan bersaing dengan ahli matematik manusia?

Ini adalah perkembangan yang menarik, tetapi Wu berkata kerja pasukan hanyalah bukti konsep. "Jika matlamatnya adalah untuk melatih mesin yang setanding dengan ahli matematik manusia terbaik, maka pemformalkan automatik nampaknya menjadi laluan utama untuk mencapai matlamat ini." berkata jika kadar kejayaan dipertingkatkan lagi, AI akan mampu bersaing dengan ahli matematik manusia. "

Jika kami mencapai 100%, kami pasti akan mencipta ejen AI yang memenangi pingat emas Olimpik Matematik Antarabangsa.

"Matlamat segera pasukan adalah untuk menambah baik model formal automatik dan bukti automasi mesin, tetapi kesan masa depan hasil penyelidikan akan menjadi jauh lebih mendalam. Wu berkata model ini boleh mendedahkan bidang matematik yang kini tidak diketahui oleh manusia.

Keupayaan penaakulan mesin ini juga sangat sesuai untuk tugas pengesahan dalam julat bidang yang lebih luas. "Anda boleh mengesahkan sama ada perisian melakukan apa yang anda mahukan, atau anda boleh mengesahkan cip perkakasan, supaya ia mempunyai aplikasi dalam algoritma perdagangan kewangan dan reka bentuk perkakasan

Menggunakan mesin untuk meneroka matematik adalah sesuatu yang teruja. perkembangan itu, kata Yang-Hui He dari Institut Sains Matematik di London, tetapi cabaran sebenar adalah menggunakan model dalam penyelidikan matematik yang kebanyakannya ditulis dalam LaTex. "Kami hanya menggunakan LaTex kerana ia lancar untuk menaip, tetapi ia adalah bahasa semula jadi dalam erti kata dan mempunyai peraturannya sendiri

Katanya, kerana pengguna boleh menentukan fungsi dan Notasi mereka sendiri, fungsi dan fungsi ini." simbol hanya boleh digunakan dalam satu kertas matematik, yang boleh menjadi rumit untuk rangkaian saraf yang dilatih hanya pada teks biasa.

Atas ialah kandungan terperinci Dengan menukar masalah matematik kepada kod, penyelidikan Google telah meningkatkan ketepatan pembuktian mesin.. Untuk maklumat lanjut, sila ikut artikel berkaitan lain di laman web China PHP!