Celah dalam makalah Tao Zhexuan ditemukan oleh AI, dan prediksi 26 tahun akan menjadi kenyataan! Menebak arah penelitian dengan melihat nama teorema, dewa agung menyebut kemampuan AI luar biasa

Sumber artikel: Zhiyuan Baru

Baru-baru ini, Tao Zhexuan, dewa matematika yang tertarik menggunakan GPT-4 dan Copilot untuk melakukan penelitian, menemukan bug tersembunyi di makalahnya dengan bantuan AI!

Tao Zhexuan mengatakan bahwa dalam proses memformalkan argumen di halaman 6 dengan Lean4, ia menemukan ekspresi itu

Pada n = 3 dan k = 2, sebenarnya berbeda.

Bug yang tidak terlalu jelas ini tertangkap tepat waktu berkat Lean4.

Pasalnya, Lean memintanya untuk membangun 02. Akibatnya, Lean tidak dapat didasarkan pada 0 negatif

Untungnya, ini hanyalah bug kecil yang hanya ada ketika nilai-n kecil. Pada titik ini, Anda hanya perlu memodifikasi beberapa konstanta di kertas.

Beberapa penggemar penggemar matematika berseru dalam posting ini: Ini luar biasa, dan sangat bagus untuk melihat penyebaran asisten bukti AI, meletakkan dasar yang lebih kuat untuk masa depan penelitian matematika.

Tao Zhexuan mengatakan bahwa ini sangat mungkin.

Mungkin dalam waktu dekat, kita bisa membangun lapisan AI di atas Lean.
Dengan menjelaskan langkah-langkah dalam pembuktian ke AI, AI dapat menggunakan Lean untuk mengeksekusi bukti, dan dalam prosesnya juga dapat memanggil berbagai paket aljabar komputer.

Pada bulan Juni tahun ini, Tao Zhexuan meramalkan dalam sebuah blog tentang pengalaman uji coba GPT-4 -

Pada tahun 2026, AI akan dikombinasikan dengan alat pencarian dan matematika simbolik untuk menjadi rekan penulis tepercaya dalam penelitian matematika.

Selama periode ini, ada orang yang terus membuktikan hal ini. Sebagai contoh, para sarjana dari Caltech, NVIDIA, MIT dan lembaga lain telah membangun prover teorema berdasarkan LLM open-source.

Dan Tao Zhexuan juga mempraktikkannya, dan makalah baru mulai ditulis dalam GPT-4, dan berulang kali berseru - kemampuan luar biasa GitHub Copilot membuat saya merasa tidak nyaman!

AI memberkati Tuhan Penelitian Matematika

Baru-baru ini, Tao Zhexuan telah sepenuhnya "memasuki lubang" AI.

Dengan bantuan GPT-4, ia mulai belajar menulis makalah dan melakukan penelitian matematika dengan Lean4.

Dia sangat bersemangat tentang proses yang dia posting di Mastodon setiap beberapa jam untuk merekam pembelajaran dan pengalamannya.

Dalam menulis makalah tentang ketidaksetaraan McLaughlin, Tao menggunakan alat AI secara ekstensif seperti GPT-4, Copilot, dan Lean4.

Alamat:

Saat kita pergi, Tao telah menyelesaikan perbaikan argumen di Bagian 2 makalah di Lean4.

Namun, prosesnya jauh lebih membosankan daripada yang dia harapkan, dan setiap baris bukti membutuhkan waktu sekitar satu jam untuk diformalkan.

Selama minggu pertama proyek, hambatannya adalah kurangnya keakraban dengan sintaks dan alat Lean; Tetapi hambatan saat ini terletak pada alat itu sendiri - tidak semaju yang ada dalam paket aljabar komputer.

Misalnya, dalam satu baris makalahnya, ia menyatakan bahwa ketidaksetaraan:

Dapat diatur ulang sebagai:

Dengan asumsi semua penyebut positif, ini adalah tugas yang sangat cepat untuk perhitungan manual dan dapat dilakukan dengan cukup mudah dalam paket aljabar komputer standar.

Lean memiliki alat otomatis yang sangat berguna untuk menangani operasi linier, tetapi saat ini tidak ada alat untuk secara otomatis menyederhanakan ekspresi kompleks yang melibatkan eksponen.

Oleh karena itu, kita harus berurusan dengan hukum eksponensial dan operasi lain yang disebutkan di atas selangkah demi selangkah, dan proses ini sangat memakan waktu.

Pada akhirnya, Tao memutuskan untuk tidak menggunakan notasi asimtotik di bagian argumen ini, tetapi untuk membangun ketidaksetaraan dengan konstanta C yang pasti:

ke dalamnya

Awalnya, Tao berpikir akan "lebih sederhana" untuk membuktikan ketidaksetaraan dengan nilai-nilai seperti C = 7. Namun, sulit untuk menggunakan alat yang ada untuk membuktikan C≤7 secara ketat, sehingga gagasan itu ditinggalkan demi nilai C yang lebih formal operasional. Sekarang dipilih, nilainya sekitar 6,16.

Dalam hal ini, beberapa netizen yang penasaran bertanya, "Bagaimana AI melakukannya dalam membuktikan kecepatan dibandingkan dengan aritmatika tangan?"

Tao Zhexuan mengatakan bahwa berdasarkan pengamatannya sendiri, jenis tugas yang mekanis untuk paket aljabar komputer dan kalkulator belum tentu mekanis untuk asisten bukti formal.

Tetapi dengan munculnya LLM, kita harus dapat menyatukan semua alat yang dibantu komputer menjadi satu alat universal yang mudah digunakan. Dan alat ini akan memiliki semua manfaat dari setiap komponen.

Bahkan, dalam waktu dekat, kita juga dapat membayangkan membangun lapisan AI di atas Lean -

Langkah-langkah dalam bukti dijelaskan kepada AI dalam "Bahasa Inggris Matematika", dan AI kemudian dapat mencoba menjalankannya menggunakan Lean, mungkin memanggil paket aljabar komputer dalam prosesnya.

Copilot bisa menebak langkah selanjutnya

Sebelumnya, dalam makalah tentang penelitian ketidaksetaraan McLaughlin ini, Tao Zhexuan terkejut menemukan bahwa Copilot mampu memprediksi apa yang ingin dia lakukan selanjutnya!

Tidak hanya dapat memprediksi dengan benar beberapa baris kode yang digunakan untuk berbagai verifikasi rutin, tetapi juga dapat menyimpulkan ke arah mana dia ingin melakukan penelitiannya berdasarkan nama teorema yang disediakan oleh Tao Zhexuan.

Ini membuat Tao Zhexuan berseru lagi dan lagi: Luar biasa!

Dalam proses pembuktian teorema 1.3 di makalah, Tao Zhexuan menggunakan Lean4 untuk menyelesaikan formalisasi bukti teorema.

Di koran, hanya ada satu halaman dalam proses pembuktian, tetapi bukti formal menggunakan 200 baris Lean4.

Misalnya, di koran, Tao Zhexuan hanya berasumsi

adalah cembung pada bilangan real a>0 dan ketidaksetaraan Jensen disebut sesudahnya. Tetapi kode ini membutuhkan sekitar 50 baris.

Dalam prosesnya, GitHub Copilot menunjukkan semua jenis prediksi ilahi, dan secara ajaib memprediksi arah penelitian Tao Zhexuan selanjutnya.

Strategi penulisan ulang Lean memungkinkan dia untuk merevisi asumsi atau tujuan yang panjang melalui substitusi yang ditargetkan.

Fitur ini sangat penting karena memungkinkan orang untuk secara bebas memanipulasi ekspresi ini tanpa harus memasukkannya secara keseluruhan sepanjang waktu.

Secara komparatif, di LaTex, operasi ini jauh lebih rumit.

Tao Zhexuan mengatakan bahwa dia perlu secara kasar mensimulasikan strategi penulisan ulang Lean4, dan melakukan pengeditan yang ditargetkan untuk ekspresi panjang dari satu baris ke baris berikutnya melalui operasi seperti memotong dan menempel. Hal ini dapat menyebabkan kesalahan ketik menyebar di beberapa baris dalam dokumen.

Lean4 dapat melakukan penulisan ulang ini dengan cara otomatis dan dapat diverifikasi.

Tentu saja, Lean 4 bukanlah obat mujarab saat ini, dan ada beberapa keterbatasan. Misalnya, menulis ulang ekspresi yang melibatkan variabel kendala tidak selalu mudah.

Tao Zhexuan berkata bahwa dia menantikan ketika mudah menggunakan bahasa alami untuk meminta LLM melakukan konversi seperti itu.

Ke dalam lubang GPT-4 + GitHub Copilot, Crazy Amway

Pada awal September, Tao Zhexuan memposting posting yang memuji efek ChatGPT dalam menghasilkan kode Python - secara langsung menghemat beban kerja setengah jam!

Sebagai percobaan, ia meminta ChatGPT untuk menulis sepotong kode Python yang menghitung panjang M(n) dari urutan terpanjang 1,...,n untuk setiap bilangan asli n, di mana φ fungsi mahakuasa Euler tidak berkurang.

Misalnya, M(6)=5 karena φ tidak menurun pada 1,2,3,4,5 (atau 1,2,3,4,6) tetapi tidak pada 1,2,3,4,5,6.

Menariknya, itu menghasilkan sepotong kode yang sangat cerdik untuk menghitung fungsi mahakuasa, yang sangat cerdik sehingga Tao harus menatapnya selama beberapa menit sebelum dia mengerti apa prinsip di balik kode itu.

Tentu saja, kode ini juga bias - hanya mempertimbangkan suburutan bilangan bulat kontinu, bukan urutan sewenang-wenang.

Namun, ini cukup dekat, menggunakan kode awal yang dihasilkan oleh ChatGPT ini sebagai titik awal, Tao Zhexuan akhirnya secara manual menghasilkan kode yang diinginkannya, yang menyelamatkannya sekitar setengah jam kerja.

Karena hasil yang diberikan oleh ChatGPT sangat bagus, Tao Zhexuan mengatakan bahwa dia akan sering menggunakannya di masa mendatang untuk memberikan kode awal untuk perhitungan serupa.

Segera, Tao Zhexuan memposting lagi bahwa dia telah memasuki GitHub Copilot di bawah rekomendasi netizen!

Tidak mengherankan, penampilan Copilot selanjutnya adalah kejutan nyata baginya – hanya memberikan paragraf pembuka dan menambahkan kalimat, AI merekomendasikan sesuatu yang sangat dekat dengan visinya sendiri.

Tao Zhexuan hanya perlu membuat sedikit modifikasi pada saran-saran ini, dan dia dapat menyelesaikannya dalam waktu kurang dari separuh waktu yang direncanakan semula.

Pada bulan Oktober, Tao Zhexuan menemukan bahwa meskipun GPT-4 tidak dapat memberikan bantuan langsung untuk permainan, ketika ia mulai menggunakan Lean, GPT-4 menjadi sangat berguna.

Ketika level menjadi semakin sulit, peran GPT mulai menunjukkan dirinya.

Dalam kasus di mana jelas bahwa Z adalah hasil dari X dan Y, bertanya kepada GPT "Bagaimana saya bisa membuktikan Z jika saya sudah tahu X dan Y?" dapat menyelesaikan segala macam masalah tata bahasa halus dalam prosesnya.

Selain konten yang berhubungan dengan profesional, Tao Zhexuan menemukan bahwa dia dapat menggunakan DALL· E 3 dan segera mulai bermain.

** Netizen: LLM dapat membuat orang-orang hebat 10.000 kali lebih baik **

Fakta bahwa dewa agung begitu terobsesi dengan alat AI dalam penelitian matematika juga telah memicu diskusi panas di kalangan netizen.

Beberapa orang mengatakan bahwa Okami mulai belajar Lean4 dengan bantuan GPT-4 awal bulan ini, dan dari waktu ke waktu dia akan mencatat kemajuan belajarnya di mastodon.

Ini juga menunjukkan bahwa bagi orang-orang yang paling sukses, LLM dapat mempercepat pekerjaan mereka.

Beberapa orang mengatakan bahwa bahkan orang yang tidak dapat menulis kode, selama mereka adalah komunikator LLM yang baik, dapat dengan cepat mengotomatiskan fungsi.

Namun, jika hanya individu yang sangat terampil yang dapat menggunakan LLM secara efektif, hasilnya adalah ketidaksetaraan antara orang-orang dapat meningkat.

Seseorang segera maju untuk mengatakan bahwa itu benar, temannya tidak dapat menulis apa pun kecuali rumus Excel, tetapi sekarang, dia dapat menulis aplikasi Python dengan GPT-4!

Sebagai pembuat kode dengan pengalaman pengembangan selama 30 tahun, dia juga perlu memintanya untuk mengajarinya teknologi ini.

Keberhasilannya mungkin karena kemampuannya untuk berkomunikasi dengan LLM.

Telah diprediksi bahwa seiring waktu, orang yang menggunakan LLM akan menuai manfaat luar biasa, terlepas dari kecerdasan mereka sendiri, dan mereka akan naik lebih tinggi dan lebih tinggi menaiki tangga untuk menjadi ahli ujian.

Untuk elit, mereka mungkin mendapatkan dorongan 100 kali lipat dari LLM, dan untuk insinyur top, itu sekitar 10.000 kali dorongan.

Sumber daya: