Terence Tao menyukainya! ChatGPT secara otomatis membuktikan terobosan besar, dan AI akan mendominasi dunia matematika dalam 10 tahun

**Sumber:**Xinzhiyuan

**Panduan:**Meskipun banyak orang tidak mau mengakuinya, sangat mungkin AI akan menyusul matematikawan manusia dalam waktu sepuluh tahun.

Beberapa hari yang lalu, sebuah makalah oleh peneliti Caltech dan MIT menggunakan ChatGPT untuk membuktikan teorema matematika meledak dan menarik perhatian besar di lingkaran matematika.

Jim Fan, kepala ilmuwan Nvidia, meneruskannya dengan penuh semangat, mengatakan bahwa kopilot matematika AI telah tiba, dan orang berikutnya yang menemukan teorema baru akan menjadi ahli matematika AI yang sepenuhnya otomatis!

The New York Times juga menerbitkan sebuah artikel baru-baru ini, mengatakan bahwa ahli matematika sudah siap, dan AI akan mengejar atau bahkan melampaui ahli matematika manusia terbaik dalam sepuluh tahun.

Dan Tao Zhexuan sendiri mem-posting ulang artikel ini.

Siobhan Roberts berpartisipasi dalam lokakarya IPAM tahun ini yang diadakan oleh Machine Assisted Proofs, dan kemudian dia menulis artikel ini tentang AI dan matematika berdasarkan pengalaman dan wawancaranya sendiri

**AI juga datang untuk menumbangkan dunia matematika! **

Hari ini, ahli matematika harus menghadapi kekuatan revolusioner terbaru — AI.

Pada tahun 2019, ilmuwan komputer Christian Szegedy, mantan karyawan Google yang sekarang bekerja di perusahaan rintisan Bay Area, meramalkan bahwa sistem komputer akan menyamai atau melampaui kemampuan pemecahan masalah dari ahli matematika manusia terbaik dalam satu dekade. Tahun lalu, dia merevisi target tanggal menjadi 2026.

Ahli logika Universitas Carnegie Mellon Jeremy Avigad (berbaju biru) bersama siswa di Sekolah Musim Panas Matematika Formal

Akshay Venkatesh, pemenang Fields Medal 2018 dan ahli matematika di Institute for Advanced Study di Princeton, saat ini tidak tertarik menggunakan AI, tetapi dia sangat tertarik untuk membahas topik terkait AI.

Dalam sebuah wawancara tahun lalu, Venkatesh berkata, "Saya ingin murid-murid saya menyadari bahwa bidang ini akan banyak berubah."

Dan baru-baru ini sikapnya adalah: "Saya tidak keberatan dengan penggunaan AI yang disengaja, bahkan disengaja untuk membantu pemahaman manusia. Tapi saya sangat yakin bahwa kita perlu berhati-hati dan berhati-hati tentang cara kita menggunakannya."

Pada bulan Februari tahun ini, Institut Matematika Teoritis dan Terapan di UCLA mengadakan lokakarya tentang "Bukti dengan Bantuan Mesin".

Penyelenggara utama seminar tersebut adalah Tao Terence, seorang ahli matematika yang memenangkan Fields Medal pada tahun 2006 dan bekerja di UCLA.

Ia mencontohkan, penggunaan AI untuk membantu pembuktian matematis sebenarnya merupakan fenomena yang patut mendapat perhatian.

Hanya dalam beberapa tahun terakhir matematikawan mulai mengkhawatirkan potensi ancaman AI, apakah itu penghancuran estetika matematika oleh AI atau ancaman terhadap matematikawan itu sendiri.

Dan anggota komunitas yang luar biasa mengangkat masalah ini ke atas meja dan mulai mengeksplorasi cara "melanggar tabu".

Penyelenggara sekolah musim panas, dari kiri ke kanan: Avigad, Patrick Massot, dan Heather Macbeth

Dari primitif geometri Euclidean hingga kode komputer

Selama ribuan tahun, ahli matematika telah beradaptasi dengan kemajuan terbaru dalam logika dan penalaran. Tapi apakah mereka siap untuk AI?

Potret ahli matematika Yunani abad ke-17 Euclid di Museum Getty di Los Angeles: dia berpakaian compang-camping dan mengangkat risalahnya tentang geometri, Elemen

Selama lebih dari 2.000 tahun, teks Euclid telah menjadi paradigma argumen dan penalaran matematis.

Ahli logika Universitas Carnegie Mellon Jeremy Avigad mengatakan Euclid memulai dengan "definisi" yang hampir puitis untuk membangun matematika pada masanya—menggunakan konsep dasar, definisi, dan teorema sebelumnya, masing-masing berurutan. Semua langkah "mengikuti dengan jelas" langkah sebelumnya, dalam sedemikian rupa untuk membuktikan sesuatu.

Beberapa orang mengeluh bahwa beberapa langkah Euclid yang "jelas" tidak begitu jelas, tetapi Dr. Avigad mengatakan bahwa sistem tersebut berhasil.

Tapi setelah abad ke-20, ahli matematika tidak lagi mau mendasarkan matematika pada basis geometris intuitif ini.

Sebaliknya, mereka mengembangkan sistem formal dengan representasi simbolik yang tepat dan aturan mekanis.

Akhirnya, di bawah sistem seperti itu, matematika dapat diterjemahkan ke dalam kode komputer.

Pada tahun 1976, teorema empat warna menjadi teorema besar pertama yang dibuktikan dengan bantuan perhitungan brute force.

Teorema empat warna: Empat warna cukup untuk mengisi peta sehingga tidak ada dua wilayah yang berdekatan memiliki warna yang sama

Komplain AI: Maaf, saya tidak mengerti teorema Anda

Ada gadget matematika yang disebut Proof Assistant, atau Interactive Theorem Prover.

Selangkah demi selangkah, ahli matematika mengubah bukti menjadi kode, dan kemudian menggunakan program perangkat lunak untuk memeriksa apakah penalarannya benar.

Proses verifikasi terakumulasi dalam pustaka referensi spesifikasi dinamis, yang tersedia untuk orang lain.

Dr. Avigad, direktur Pusat Hoskinson untuk Matematika Formal, mengatakan jenis formalisasi ini menjadi dasar bagi matematika saat ini, sama seperti Euclid mencoba mentranskodekan matematika pada masa itu, dengan demikian memberikannya landasan.

Baru-baru ini, Lean, sistem asisten bukti sumber terbuka, sekali lagi menarik banyak perhatian.

Lean dikembangkan oleh ilmuwan komputer Amazon saat ini Leonardo de Moura saat berada di Microsoft.

Lean menggunakan penalaran otomatis, didukung oleh AI GOFAI jadul, AI simbolis yang terinspirasi oleh logika.

Sejauh ini, Lean telah memverifikasi teorema menarik yang mengubah bola dari dalam ke luar, serta teorema kunci yang menyatukan skema di seluruh bola matematika.

Namun, asisten pembuktian juga memiliki kekurangan: ia sering mengeluh bahwa ia tidak memahami definisi, aksioma, atau langkah-langkah penalaran yang dimasukkan oleh ahli matematika, sehingga disebut juga "pengadu bukti".

Keluhan tersebut akan membuat penelitian menjadi rumit, tetapi jenis fungsionalitas yang memberikan umpan balik baris demi baris juga akan membuat sistem berguna untuk pengajaran, kata Heather Macbeth, ahli matematika di Universitas Fordham.

Musim semi ini, Dr. Macbeth merancang kursus "dwibahasa". Dia menerjemahkan setiap masalah di papan tulis ke dalam kode Lean di catatan kuliah, dan siswa harus menyerahkan solusi dalam bahasa Lean dan alami.

"Itu memberi mereka kepercayaan diri," kata Dr. Macbeth, karena mereka akan menerima umpan balik instan saat pembuktian selesai dan apakah setiap langkah di sepanjang jalan itu benar atau salah.

Dan setelah mengikuti lokakarya, matematikawan Emily Riehl dari Universitas Johns Hopkins mencobanya.

Emily Riehl, seorang ahli matematika di Universitas Johns Hopkins, telah menggunakan asisten pembuktian eksperimental

Dia menggunakan applet asisten bukti untuk membuktikan teorema dalam artikelnya yang diterbitkan sebelumnya.

Setelah menggunakannya, dia terkejut. "Sekarang saya memahami proses pembuktian jauh lebih dalam daripada yang pernah saya lakukan. Pemikiran saya sangat jelas sehingga saya dapat menjelaskannya ke komputer paling bodoh sekalipun."

Proyek kelompok yang diikuti siswa selama Sekolah Musim Panas Formalisasi Matematika

**Penalaran keras - ini bukan "matematis" **

Alat lain yang sering digunakan ilmuwan komputer untuk menyelesaikan beberapa masalah matematika disebut "penalaran keras", tetapi komunitas matematika sering mencemooh metode ini.

Namun, ilmuwan AI tampaknya tidak terlalu peduli dengan ide-ide matematikawan, dan terus menggunakan metode mereka yang sudah dikenal untuk menangkap "dataran tinggi" matematika.

Heule, seorang ilmuwan komputer di Universitas Carnegie Mellon, menggunakan file "pemecah SAT" 200T untuk memecahkan "masalah rangkap tiga Boolean Pythagoras" pada tahun 2016.

Majalah "Nature" mengatakan dalam artikelnya: Pembuktian 200T adalah proses pembuktian terbesar dalam sejarah. Apakah matematika benar-benar menggunakan alat ini untuk memecahkan masalah?

Namun dalam pandangan ilmuwan komputer Heule, penulis makalah tentang pemecahan masalah itu sendiri, "pendekatan ini diperlukan untuk memecahkan masalah di luar jangkauan kemampuan manusia."

Demikian pula, setelah mengalahkan manusia dalam permainan catur (AlphaZero), DeepMind merancang algoritme pembelajaran mesin untuk memecahkan pelipatan protein (AlphaFold).

DeepMind menerbitkan makalah yang menyatakan bahwa cara mereka mencapai hasil ini adalah dengan menggunakan AI untuk memandu intuisi manusia untuk memajukan matematika.

Yuhuai Wu, mantan ilmuwan komputer Google yang kini memulai bisnis di Bay Area, juga mengatakan bahwa arah bisnisnya adalah menggunakan pembelajaran mesin untuk memecahkan masalah matematika.

Proyeknya saat ini, Minerva, adalah model bahasa besar yang disempurnakan untuk memecahkan model matematika.

Di masa depan, ia berharap proyek tersebut akan berkembang menjadi "ahli matematika otomatis" yang dapat "memecahkan masalah matematika secara mandiri" sebagai asisten peneliti umum.

Matematika adalah tes lakmus

Di sisi lain, banyak matematikawan yang telah mendalami kontak dengan teknologi AI juga mengemukakan kekhawatiran bahwa AI tidak dianggap serius dalam penelitian matematika.

Mereka percaya bahwa teknologi kecerdasan buatan seringkali dapat "secara langsung" membantu ahli matematika "menemukan" jawaban yang mereka inginkan.

Meskipun matematikawan atau pakar AI tidak tahu bagaimana AI menemukan jawaban ini.

Geordie Williamson, seorang ahli matematika yang pernah bekerja dengan DeepMind, pernah berbagi pengalaman bekerja dengan DeepMind.

Dalam proses kerjasamanya dengan DeepMind, sebuah jaringan saraf yang ditemukan oleh DeepMind dapat memprediksi nilai data yang menurutnya sangat penting, dan sangat akurat.

Dia berusaha sangat keras untuk memahami bagaimana AI melakukannya, karena itu bisa menjadi dasar teorema.

Tapi dia masih tidak bisa memahami logika AI pada akhirnya, dan orang-orang di DeepMind juga tidak bisa melakukannya.

Seperti Euclid, jaringan saraf entah bagaimana menemukan kebenaran, tetapi alasan logisnya sulit dipahami.

Inferensi, di sisi lain, dari sudut pandang ahli matematika, adalah inti dari matematika tetapi merupakan bagian dari teka-teki yang hilang dalam pembelajaran mesin.

Di dunia teknologi, dunia teknologi akan sangat puas jika ada kotak hitam yang sering memberikan solusi untuk suatu masalah.

AI adalah kotak hitam.

Tetapi ahli matematika tidak puas dengan situasi ini.

Menurut ahli matematika itu, mencoba memahami cara kerja jaringan saraf menimbulkan pertanyaan matematika yang menarik.

Dan memecahkan masalah ini akan memungkinkan ahli matematika untuk "memberikan kontribusi yang berarti bagi dunia".

Jika AI dapat membuktikan teorema matematika

Apa yang akan kita lakukan jika dunia dibanjiri dengan hipotesis buatan AI?

Netizen mengirimkan siksaan jiwa untuk ini, dan saya ragu tentang hipotesis / formula baru sistem AI sebagai langkah pertama, karena DeepMind telah melakukannya dalam teori simpul.

Saya bertanya-tanya bagaimana komunitas akan menanggapi banjir asumsi baru yang dihasilkan oleh AI. Mengecek argumen logis yang dibuat oleh AI adalah satu hal; kewalahan oleh jutaan saran "oh, ini mungkin benar" adalah hal lain. Saya rasa sistem ulasan dan publikasi kami yang ada belum siap untuk ini.

Bagaimana hal ini memengaruhi kepercayaan orang terhadap matematika?

Telah diperdebatkan bahwa mesin tidak akan dapat melakukan matematika dalam waktu dekat, tetapi dapat terlihat mengubah cara penelitian dilakukan dengan cara yang sama seperti model pembelajaran mesin dan kekuatan komputasi telah mengubah bidang biologi.

Beberapa netizen mengatakan bahwa sejak AlphaDev, saya telah memikirkan masalah ini, tetapi program yang sama dapat membuat algoritme pengurutan, dan juga dapat menggunakan pemeriksa bukti otomatis untuk membuktikan teorema matematika. Pertanyaan sebenarnya adalah apakah itu bisa digunakan untuk membuktikan sesuatu yang penting, bukan hanya penemuan sepele.

Namun, beberapa netizen masih ragu apakah alat seperti GPT benar-benar dapat mengungkap kebenaran yang berharga.

Beberapa netizen juga menunjukkan bahwa mungkin ada perbedaan antara manusia dan AI dalam memahami dan memperhatikan matematika, AI membuktikan apa yang benar, sedangkan manusia selalu fokus pada mengapa itu benar.

Referensi: