Perangkat Kecerdasan Buatan mendefinisikan bentuk pembukti teorema otomatis generasi berikutnya, dan dengannya, hubungan antara matematika dan mesin.
Dikatakan bahwa pada tahun 1970, matematikawan yang sekarang sudah meninggal, Paul Cohen , satu-satunya pemenang Fields Medal untuk karyanya tentang logika matematika , telah membuat prediksi tak berdasar yang masih berlanjut untuk menyenangkan atau mengganggu para ahli matematika: "suatu hari nanti akan menggantikan masa depan matematikawan komputer ". Cohen, yang dikenal dengan metodenya yang berani dalam bekerja dengan teori himpunan, meramalkan bahwa semua matematika dapat diotomatiskan, termasuk penulisan bukti.
Pembuktian adalah penalaran logis langkah demi langkah yang menegaskan kebenaran hipotesis atau asumsi matematika. Setelah bukti muncul, hipotesis menjadi teorema. Keduanya menegaskan kebenaran pernyataan itu, dan menjelaskan mengapa itu benar. Tapi buktinya aneh. Itu abstrak dan tidak terikat pada pengalaman material. "Mereka adalah hasil dari kontak gila antara dunia fiksi, non-fisik dan makhluk yang muncul sebagai hasil evolusi biologis," kata ilmuwan kognitif Simon Dedeo dari Universitas Carnegie Mellon, yang mempelajari kepastian matematika melalui analisis struktur bukti. "Evolusi tidak mempersiapkan kita untuk ini."
Komputer bagus untuk komputasi massal, tetapi pembuktiannya memerlukan sesuatu yang berbeda. Hipotesis muncul dari penalaran induktif - intuisi khusus yang terkait dengan masalah yang menarik - dan bukti biasanya mengikuti logika deduktif langkah demi langkah. Mereka seringkali membutuhkan pemikiran kreatif yang kompleks serta kerja keras untuk mengisi kekosongan, dan mesin tidak dapat menangani kombinasi keterampilan ini.
Penguji teorema terkomputerisasi terbagi dalam dua kategori. Penguji teorema otomatis (ATP) biasanya menggunakan metode brute force untuk menggiling tumpukan angka yang sangat besar. Interactive theorem provers (ITP) berfungsi sebagai asisten manusia, dan mampu memeriksa keakuratan argumen, serta mencari kesalahan dalam pembuktian yang ada. Namun, bahkan jika Anda menggabungkan kedua strategi ini (seperti halnya pembukti yang lebih modern), sistem penalaran otomatis tidak akan muncul dari keduanya.
Ilmuwan kognitif Simon Dedeo dari Universitas Carnegie Mellon membantu mendemonstrasikan bahwa manusia dan mesin membuat bukti matematis dengan cara yang sama.
Selain itu, alat ini sangat sedikit diterima orang, dan sebagian besar ahli matematika tidak menggunakan atau menyetujuinya. "Ini adalah topik kontroversial bagi ahli matematika," kata Dedeo. "Kebanyakan dari mereka tidak menyukai gagasan itu."
Salah satu masalah sulit terbuka di area ini adalah pertanyaan tentang seberapa banyak proses pembuatan bukti dapat diotomatiskan. Akankah sistem dapat menghasilkan hipotesis yang menarik dan membuktikannya dengan cara yang dapat dipahami orang? Serangkaian terobosan terbaru yang dibuat oleh laboratorium di seluruh dunia menawarkan cara kecerdasan buatan (AI) untuk menjawab pertanyaan ini. Joseph Urban dari Institut Ceko untuk Informatika, Robotika, dan Sibernetika di Praha, sedang menjajaki berbagai pendekatan yang menggunakan pembelajaran mesin untuk meningkatkan keefektifan alat pembuktian yang ada. Pada bulan Juli, grupnyamenunjukkan serangkaian hipotesis asli dan bukti yang dibuat dan divalidasi oleh mesin. Pada bulan Juni, sebuah grup di Google Research yang dipimpin oleh Christian Szegedi menerbitkan hasil dari upaya untuk menggunakan kekuatan sistem pemrosesan bahasa alami untuk membuat bukti komputer lebih mirip dalam struktur dan penjelasan dengan yang dimiliki manusia.
Beberapa ahli matematika melihat penguji teorema sebagai alat yang dapat merevolusi cara siswa belajar menulis bukti. Yang lain mengatakan bahwa membuat komputer menulis bukti untuk matematika tingkat lanjut itu tidak perlu, jika bukan tidak mungkin. Namun, sistem yang mampu memprediksi hipotesis yang berguna dan membuktikan teorema baru dapat mencapai sesuatu yang baru - semacam pemahaman versi mesin, kata Szegedi. Dan ini menunjukkan kemungkinan penalaran otomatis.
Mesin yang berguna
Matematikawan, ahli logika, dan filsuf telah lama memperdebatkan bagian mana dari pembuatan bukti yang bersifat manusiawi, dan perdebatan tentang mekanisasi matematika berlanjut hingga hari ini - terutama di mana ilmu komputer menyatu dengan matematika murni.
Bagi ilmuwan komputer, penguji teorema tidak kontroversial. Mereka memberikan cara yang jelas untuk memastikan bahwa program tersebut bekerja, dan argumen tentang intuisi dan kreativitas kurang penting daripada menemukan cara efektif untuk memecahkan masalah. Misalnya, Adam Chlipala , seorang ilmuwan komputer di Massachusetts Institute of Technology, telah mengembangkan alat pembuktian teorema yang menghasilkanalgoritma kriptografi yang melindungi transaksi di Internet - terlepas dari kenyataan bahwa biasanya orang membuat algoritma semacam itu. Kode grupnya sudah digunakan di sebagian besar komunikasi di browser Google Chrome.
Emily Riel dari Johns Hopkins University menggunakan penguji teorema untuk melatih siswa dan asisten komputer.
"Anda dapat mengambil pernyataan matematika apa pun dan mengkodekannya dengan satu alat, lalu menggabungkan semua argumen, dan mendapatkan bukti keamanan," kata Chlipala.
Dalam matematika, penguji teorema membantu menghasilkan pembuktian yang kompleks dan intensif secara komputasi yang seharusnya membutuhkan ribuan tahun matematika. Contoh yang mencolok adalah hipotesis Keplertentang pengepakan bola terpadat dalam ruang tiga dimensi (secara historis, ini adalah bola jeruk atau bola meriam). Pada tahun 1998, Thomas Hales dan muridnya, Sam Ferguson, menyelesaikan pembuktian ini menggunakan berbagai teknik matematika yang terkomputerisasi. Hasilnya sangat rumit - buktinya membutuhkan 3 GB - sehingga 12 ahli matematika menganalisisnya selama beberapa tahun sebelum mengumumkan bahwa mereka 99% yakin akan kebenarannya.
Hipotesis Kepler bukanlah satu-satunya masalah terkenal yang diselesaikan oleh mesin. Dengan teorema empat warna, mengklaim bahwa empat warna selalu cukup untuk melukis peta dua dimensi di mana tidak ada dua area bersentuhan dengan warna yang sama, ditemukan pada tahun 1977 menggunakan program komputer yang memproses peta lima warna dan menunjukkan bahwa semuanya dapat diubah menjadi empat warna. Pada tahun 2016, tiga ahli matematika menggunakan program komputer untuk membuktikan masalah Boolean kembar tiga Pythagoras yang sudah berlangsung lama , tetapi versi pertama dari buktinya adalah 200 TB. Jika Anda memiliki koneksi Internet yang cukup cepat, Anda dapat mendownloadnya dalam tiga minggu.
Perasaan campur aduk
Contoh-contoh ini sering disebut-sebut sebagai kesuksesan, tetapi mereka juga menambah rasa kontroversi. Kode komputer yang membuktikan teorema empat warna lebih dari 40 tahun yang lalu tidak dapat diverifikasi oleh manusia. "Matematikawan telah memperdebatkan apakah ini bukti atau tidak," kata ahli matematika Michael Harris dari Universitas Columbia.
Banyak ahli matematika, bersama dengan Michael Harris dari Universitas Columbia, mempertanyakan kebutuhan untuk membuat penguji teorema terkomputerisasi - dan bahwa yang terakhir akan membuat ahli matematika tidak diperlukan.
Ketidakpuasan lain dari matematikawan terkait dengan fakta bahwa jika mereka ingin menggunakan penguji teorema, pertama-tama mereka perlu mempelajari cara memprogram, dan kemudian mencari cara untuk mengungkapkan masalah mereka dalam bahasa yang dapat dimengerti komputer - dan semua ini mengalihkan perhatian dari melakukan matematika. "Pada saat saya merumuskan ulang pertanyaan dengan cara yang sesuai untuk teknologi ini, saya akan menyelesaikan masalah ini sendiri," kata Harris.
Banyak orang tidak melihat perlunya pemecah teorema. "Mereka memiliki sistem, pensil dan kertas sendiri, dan itu berfungsi," kata Kevin Buzzard, seorang ahli matematika di Imperial College London, yang mengubah arah penelitian tiga tahun lalu dari matematika murni menjadi pembuktian teorema dan pembuktian formal. “Komputer melakukan kalkulasi luar biasa untuk kami, tetapi mereka tidak pernah memecahkan masalah yang sulit sendiri,” katanya. "Dan sampai itu terjadi, ahli matematika tidak akan membelinya."
Tetapi Buzzard dan yang lainnya berpikir mereka mungkin masih perlu melihat lebih dekat pada teknologi. Misalnya, “bukti komputer mungkin tidak asing seperti yang kita kira,” kata Dedeo. Baru-baru ini, bersama dengan Scott Viteri, seorang ilmuwan komputer di Stanford, dia merekayasa balik beberapa bukti kanonik terkenal (termasuk beberapa PermulaanEuclidean) dan puluhan bukti yang dihasilkan oleh program komputer untuk membuktikan teorema Coq mencari persamaan. Mereka menemukan bahwa struktur percabangan bukti mesin sangat mirip dengan struktur bukti yang dibuat oleh manusia. Sifat bersama ini, katanya, dapat membantu peneliti menemukan cara membuat program penolong menjelaskan.
"Bukti mesin mungkin tidak semisterius yang terlihat," kata Dedeo.
Yang lain mengatakan pembuktian teorema dapat menjadi alat yang berguna untuk mengajar ilmu komputer dan matematika. Di ahli matematika Universitas Johns Hopkins, Emily Rieltelah mengembangkan kursus di mana siswa menulis bukti menggunakan pembuktian teorema. “Itu membuat mereka sangat terorganisir dan berpikir jernih,” katanya. "Siswa yang menulis bukti untuk pertama kalinya mungkin tidak segera memahami apa yang diminta dari mereka atau memahami struktur logisnya."
Riel juga mengatakan bahwa dia telah menggunakan pembukti teorema lebih dan lebih dalam karyanya belakangan ini. "Mereka tidak harus digunakan sepanjang waktu, dan tidak akan pernah menggantikan coretan di selembar kertas," katanya, "tetapi menggunakan asisten komputer untuk pembuktian telah mengubah cara saya berpikir tentang bagaimana menuliskan bukti."
Theorem Provers juga menawarkan cara untuk menjaga matematika tetap adil. Pada 1999, seorang ahli matematika Soviet, Rusia, dan AmerikaVladimir Alexandrovich Voevodsky , menemukan kesalahan dalam salah satu pembuktiannya. Sejak saat itu hingga kematiannya pada 2017, ia secara aktif mempromosikan penggunaan komputer untuk memverifikasi bukti. Hales mengatakan bahwa dia dan Ferguson menemukan ratusan kesalahan dalam pembuktian asli mereka dengan mengujinya menggunakan komputer. Bahkan teorema pertama dalam Elemen Euclid tidaklah ideal. Jika mesin dapat membantu ahli matematika menghindari kesalahan seperti itu, mengapa tidak memanfaatkannya? Harris menawarkan keberatan praktis untuk proposal ini, namun, tidak diketahui seberapa masuk akal: jika ahli matematika harus meluangkan waktu untuk memformalkan matematika agar komputer dapat memahaminya, mereka tidak akan dapat menggunakan waktu tersebut untuk matematika baru.
Namun, Timati Gowers, seorang matematikawan dan penerima Fields Prize dari Cambridge, ingin melangkah lebih jauh: Dia membayangkan bagaimana penguji teorema akan menggantikan pengulas manusia di jurnal utama di masa depan. "Saya melihat bagaimana ini bisa menjadi praktik standar - jika Anda ingin pekerjaan Anda diterima, Anda harus menjalankannya melalui peninjau otomatis."
Percakapan dengan komputer
Sebelum komputer dapat menguji atau mengembangkan bukti, para peneliti harus terlebih dahulu mengatasi rintangan yang signifikan: penghalang komunikasi antara bahasa manusia dan komputer.
Penguji teorema hari ini telah dirancang tanpa memperhatikan keramahan matematikawan. Jenis pertama, ATP, biasanya digunakan untuk menguji kebenaran suatu pernyataan, seringkali dengan menguji semua opsi yang memungkinkan. Tanyakan pada ATP apakah mungkin untuk melakukan perjalanan dari Miami ke Seattle, dan dia mungkin akan melewati semua kota yang dilalui jalan dari Miami, dan akhirnya dia akan menemukan kota yang mengarah ke Seattle.
Timati Gowers dari Universitas Cambridge percaya bahwa penguji teorema suatu hari nanti akan menggantikan pemeriksa manusia
Menggunakan ATP, programmer dapat mengkodekan semua aturan, atau aksioma, dan kemudian mengajukan pertanyaan apakah hipotesis tertentu mengikuti aturan tersebut. Dan kemudian komputer melakukan semua pekerjaan itu. “Anda tinggal memasukkan hipotesis yang ingin Anda buktikan dan berharap mendapatkan jawaban,” kata Daniel Huang, seorang ilmuwan komputer yang baru-baru ini meninggalkan UC Berkeley untuk memulai sebuah startup.
Tapi ada masalah: ATP tidak menjelaskan kerjanya. Semua kalkulasi dilakukan di dalam mesin, dan bagi seseorang kalkulasi itu terlihat seperti urutan panjang angka nol dan satu. Huang berkata bahwa tidak mungkin untuk melihat bukti dan memverifikasi alasannya, karena semuanya terlihat seperti sekumpulan data acak. “Tidak ada yang bisa melihat bukti seperti itu dan berkata: Semuanya jelas,” katanya.
Kategori kedua, ITP, memiliki kumpulan data besar yang berisi puluhan ribu teorema dan bukti yang dengannya mereka dapat memeriksa keakuratan suatu bukti. Tidak seperti ATP, yang bekerja di dalam kotak hitam yang hanya mengeluarkan respons, ITP memerlukan interaksi dan terkadang arahan dari seseorang, sehingga mereka tidak begitu tidak dapat didekati. “Seseorang bisa duduk dan mencari tahu teknik apa yang digunakan untuk membuktikan,” kata Huang. Bukti semacam itu dipelajari oleh Dedeo dan Viteri.
Dalam beberapa tahun terakhir, ITP menjadi semakin populer. Pada 2017, trinitas yang membuktikan masalah Boolean dari Pythagoras tiga kali lipat menggunakan ITP yang disebut Coq untuk membuat dan menguji versi formal dari bukti mereka. Pada tahun 2005, Georges Gontier dari Microsoft Research Cambridge menggunakan Coq untuk memformalkan teorema empat warna. Hales juga menggunakan ITP yang disebut HOL Light dan Isabelle untuk secara resmi membuktikan dugaan Kepler (HOL adalah singkatan dari logika orde tinggi).
Hari ini, garis depan bidang ini mencoba menggabungkan pembelajaran dengan penalaran. ATP sering digabungkan dengan ITP untuk mengintegrasikan pembelajaran mesin guna meningkatkan kinerja kedua teknik. Para ahli percaya bahwa program ATP / ITP dapat menggunakan penalaran deduktif dan bahkan bertukar ide matematika dengan cara yang sama seperti yang dilakukan manusia, atau setidaknya dengan cara yang serupa.
Batasan penalaran
Joseph Urban percaya bahwa pendekatan gabungan seperti itu dapat mengawinkan penalaran deduktif dan induktif, yang diperlukan untuk mendapatkan bukti. Kelompoknya menciptakan penguji teorema yang didukung oleh pembelajaran mesin, memungkinkan komputer untuk belajar dari pengalaman mereka sendiri. Selama beberapa tahun terakhir, mereka telah menjelajahi kekuatan jaringan saraf - lapisan unit komputasi yang membantu mesin memproses informasi dengan cara yang kira-kira mirip dengan cara kerja neuron di otak kita. Pada bulan Juli, kelompok mereka melaporkan hipotesis baru yang dihasilkan oleh jaringan saraf yang terlatih untuk membuktikan teorema.
Sebagian, Urban terinspirasi oleh karya Andrei Karpaty, yang beberapa tahun lalu melatih jaringan saraf untuk menghasilkan omong kosong matematika yang tampak meyakinkan bagi non-profesional. Tapi Urban tidak membutuhkan omong kosong - dia dan kelompoknya mengembangkan alat mereka sendiri yang mencari bukti, setelah melatih jutaan teorema. Mereka menggunakan jaringan untuk menghasilkan hipotesis baru dan menguji validitasnya dengan program ATP yang disebut E.
Jaringan telah mengeluarkan lebih dari 50.000 formula baru, meskipun puluhan ribu di antaranya telah diulang. “Sepertinya kita belum bisa membuktikan hipotesis yang lebih menarik,” kata Urban.
Szegedi dari Google Research melihat masalah penalaran otomatis dalam bukti komputer sebagai bagian dari bidang yang lebih luas: pemrosesan bahasa alami, yang mencakup pengenalan pola dalam penggunaan kata dan kalimat. Pengenalan pola juga merupakan ide inti dari visi komputer, yang sebelumnya dikerjakan oleh Szegedi di Google. Seperti kelompok lain, timnya ingin membuat penguji teorema yang dapat mencari bukti yang berguna dan menjelaskannya.
Terinspirasi oleh perkembangan pesat alat AI seperti AlphaZero - perangkat lunak DeepMind yang dapat mengalahkan manusia dalam catur, go, dan shogi - grup Szegedi ingin menggunakan kemajuan terbaru dalam pengenalan bahasa untuk merekam bukti. Dia mengatakan bahwa model bahasa dapat menunjukkan penalaran matematis yang sangat akurat.
Kelompoknya di Google Research baru-baru ini menjelaskan cara menggunakan model bahasa - yang sering digunakan oleh jaringan saraf - untuk menghasilkan bukti baru. Setelah melatih model untuk mengenali struktur pohon dari teorema yang terbukti, mereka meluncurkan eksperimen gratis, hanya meminta jaringan saraf untuk menghasilkan dan membuktikan teorema tanpa pengawasan. Dari ribuan hipotesis yang dihasilkan, 13% ternyata dapat dibuktikan dan baru (tidak mengulangi teorema lain dalam database). Dia mengatakan bahwa eksperimen semacam itu mengatakan bahwa jaringan saraf dapat belajar, dalam arti tertentu, untuk memahami seperti apa buktinya.
“Jaringan saraf mampu mengembangkan kemiripan intuisi buatan,” kata Szegedi.
Tentu saja, masih belum jelas apakah upaya ini akan memenuhi nubuat Cohen 40 tahun lalu. Gowers mengatakan dia yakin komputer dapat melampaui matematikawan dalam penalaran pada tahun 2099. Pada awalnya, katanya, ahli matematika akan menikmati zaman keemasan, “ketika mereka melakukan hal-hal menarik dan komputer itu membosankan. Tapi saya pikir itu tidak akan bertahan lama. "
Lagi pula, jika mesin terus berkembang lebih dan lebih, dan memiliki akses ke sejumlah besar data, mereka harus belajar untuk melakukan hal-hal yang sangat baik dan menarik. “Mereka akan belajar membuat permintaan sendiri,” kata Gowers.
Harris tidak setuju. Dia tidak berpikir bukti komputer diperlukan, atau bahwa mereka pada akhirnya akan "membuat matematikawan manusia tidak diperlukan." Jika ilmuwan komputer, katanya, pernah dapat memprogram intuisi sintetik, itu tetap tidak akan bersaing dengan intuisi manusia. "Bahkan jika komputer mengerti, mereka tidak akan mengerti dalam pengertian manusia."