Terence Tao menggunakan pembantu kalis model berskala besar Lean untuk menunjukkan keutamaannya

"Saya meramalkan bahawa, jika digunakan dengan betul, AI akan menjadi pengarang bersama yang dipercayai dalam penyelidikan matematik dan banyak bidang lain menjelang 2026, kata Ahli Matematik Terence Tao dalam blog sebelumnya.

Tao Zhexuan berkata ini dan melakukannya.

Beliau baru-baru ini menjalankan penyelidikan matematik menggunakan alatan seperti GPT-4, Copilot dan Lean, dan juga menemui pepijat tersembunyi dalam kertas kerjanya dengan bantuan AI.

Baru-baru ini, Terence Tao berkata bahawa projek Lean4 telah berjaya menyelesaikan pemformalkan bukti Konjektur Polinomial Freiman-Ruzsa (PFR), yang hanya mengambil masa tiga minggu. Pada masa yang sama, pengkompil Lean juga melaporkan bahawa konjektur itu mematuhi aksiom piawai. Ini merupakan satu kejayaan besar bagi pembuktian komputer dan bantuan AI, dan ia menarik

Untuk maklumat lanjut tentang penyelidikan di atas, pembaca yang berminat boleh merujuk kepada "Apakah bukti rasmi Tao Zhexuan menggunakan AI?" Fahami kehidupan masa lalu dan masa kini tekaan PFR dalam satu artikel.

Melihat perkara ini, pembaca yang teliti mungkin telah menemui petunjuk Master Tao menyebut Lean berkali-kali semasa menjalankan penyelidikan matematik. Ringkasnya, Lean ialah bahasa pengaturcaraan yang membantu ahli matematik mengesahkan teorem, di mana pengguna boleh menulis dan mengesahkan bukti. Berbanding dengan Lean yang asal, versi Lean 4 yang terkini mempunyai banyak pengoptimuman, termasuk pengkompil yang lebih pantas, pengendalian ralat yang lebih baik dan penyepaduan yang lebih baik dengan alatan luaran.

Lean digunakan secara meluas dalam bidang matematik Hari ini, apabila model besar (LLM) popular, adakah cara yang lebih baik untuk menggabungkan kedua-duanya?

Seseorang telah melaksanakannya Pasukan LeanDojo platform terbuka (untuk LeanDojo, sila rujuk "Model besar AI membantu Tao Zhexuan menyelesaikan masalah, bolehkah ia juga membuktikan teorem matematik? ") dan penyelidikan dari California Institute of Technology Penulis melancarkan Lean Copilot, alat kerjasama yang direka untuk LLM dan interaksi manusia, bertujuan untuk memberikan 100% bukti matematik formal yang tepat melalui kerjasama manusia-mesin.

Ia perlu diperhatikan bahawa penyelidikan pasukan Leandojo terutamanya memberi tumpuan kepada menggunakan LLM untuk mengautomasikan teorem mengejutkan. . . Kini dengan kemajuan AI, penyelidik telah mula menggunakan kecerdasan buatan untuk menjalankan penerokaan yang mendalam, tetapi masalah ini tidak dapat dielakkan, iaitu, LLM kadang-kadang tidak begitu boleh dipercayai dalam tugasan matematik dan penaakulan, dan terdedah kepada kesilapan dan halusinasi.

Fungsi Lean Copilot adalah untuk membolehkan pengguna menggunakan model bahasa yang besar untuk mengautomasikan proses pembuktian dalam Lean dan meningkatkan kelajuan sintesis bukti. Pengguna juga boleh campur tangan dan mengubah suai dengan lancar apabila diperlukan, mencapai kerjasama seimbang antara kecerdasan mesin dan kecerdasan manusia

Menggunakan Lean Copilot, LLM boleh digunakan dalam Lean untuk mencapai automasi bukti, termasuk cadangan strategi, premis dan Bukti carian

Pengguna boleh memilih untuk menggunakan model terbina dalam yang disediakan oleh LeanDojo, atau mengimport model mereka sendiri. Model ini boleh dijalankan secara tempatan (dengan atau tanpa GPU), atau dalam awan

• LLM dapat mencadangkan langkah pembuktian, mencari pembuktian, dan memilih lema yang berguna daripada perpustakaan matematik yang besar.
• Lean Copilot boleh disediakan sebagai pakej Lean dan berjalan dengan lancar dalam aliran kerja VS Code Lean.
• Pengguna boleh menggunakan model terbina dalam dalam LeanDojo, atau menggunakan model mereka sendiri, yang boleh dijalankan secara setempat (dengan atau tanpa GPU) atau dalam awan.
• Alat ini berjalan pada pelbagai platform termasuk Linux, macOS dan Windows WSL.

Untuk menjadikan LLM lebih mudah diakses oleh pengguna Lean, Lean Copilot berharap untuk memulakan gelung maklum balas yang positif: membuktikan bahawa automasi akan membawa kepada data yang lebih baik dan akhirnya meningkatkan prestasi matematik LLM.

Demonstrasi kesan kopilot

Anda boleh mengkonfigurasi Lean Copilot mengikut tutorial rasmi Selepas konfigurasi selesai, anda boleh memulakan percubaan. Pengarang projek juga menyediakan beberapa contoh rasmi untuk rujukan

penyelesaian yang disyorkan. Selepas mengimport LeanCopilot, anda boleh menggunakan suggest_tactics untuk menjana penyelesaian yang disyorkan. Semasa penggunaan, anda juga boleh mengklik pada penyelesaian yang disyorkan dan menggunakannya dalam bukti (rujuk gambar di bawah)

Anda boleh menggunakan awalan, seperti simp, untuk mengehadkan strategi yang dihasilkan

Cari bukti. Gunakan search_proof untuk menggabungkan dasar yang dijana LLM dengan aesop (projek automasi kotak putih Lean 4) untuk mencari berbilang bukti dasar. Sebaik sahaja anda menemui buktinya, anda boleh klik pada strategi untuk memasukkannya ke dalam editor

Kandungan yang ditulis semula: Memilih premis ialah strategi penting. Tujuan strategi ini adalah untuk mendapatkan semula senarai premis yang berpotensi berguna. Pada masa ini, Lean Copilot menggunakan alat dapatkan semula dalam LeanDojo untuk memilih premis daripada petikan tetap Lean dan mathlib4 (iaitu perpustakaan matematik Lean 4)

Anda boleh menjalankan LLM. Sama ada pembuktian teorem atau alasan lain, anda boleh menjalankan LLM dalam Lean. Anda boleh menjalankan mana-mana model secara tempatan atau jauh (lihat Membawa Model Anda Sendiri)

Beberapa penggunaan lanjutan juga disebut dalam projek. Pembaca yang berminat boleh pergi ke projek asal untuk mengetahui lebih lanjut.

Atas ialah kandungan terperinci Terence Tao menggunakan pembantu kalis model berskala besar Lean untuk menunjukkan keutamaannya. Untuk maklumat lanjut, sila ikut artikel berkaitan lain di laman web China PHP!