Tao Zhexuan bermula: Luar biasa, ia boleh meneka arah yang saya mahu dari nama teorem

Selepas mencuba GPT-4, Terence Tao menggunakan Github Copilot sekali lagi.

Kali ini, senario percubaannya adalah untuk mempelajari bahasa Lean dan menggunakannya untuk memformalkan teorem matematik.

Untuk model besar, pembuktian teorem formal juga merupakan satu cabaran. Bukti rasmi pada asasnya ialah program komputer, tetapi tidak seperti program tradisional dalam C++ atau Python, ketepatan bukti boleh disahkan menggunakan pembantu bukti seperti bahasa Lean. Pembuktian teorem ialah satu bentuk khas penjanaan kod yang sangat ketat dalam penilaiannya, tidak meninggalkan ruang untuk ilusi dalam model.

Teorem yang disebut oleh Terence Tao berasal daripada kertas kerja pada 9 Oktober:

Bukti dalam kertas itu kurang daripada satu muka surat, tetapi bukti rasmi Terence Tao menggunakan 200 baris bahasa Lean.

Sebagai contoh, dalam makalah Terence Tao hanya menegaskan bahawa untuk mana-mana a>0, ialah cembung dalam nombor nyata, kerana ini adalah latihan kalkulus biasa, dan kemudian memanggil ketaksamaan Jensen, tetapi menulis semua butiran Ia mengambil masa kira-kira 50 baris kod.

Tao Zhexuan berkata bahawa keupayaan copilot Github untuk meramalkan berbilang baris kod dengan betul untuk pelbagai pengesahan rutin dan membuat kesimpulan arah yang dia inginkan daripada petunjuk seperti nama teorem adalah "luar biasa".

Strategi "tulis semula" Lean amat diperlukan, membolehkan anda mengubah suai andaian atau matlamat yang panjang dengan penggantian disasarkan yang beroperasi pada ungkapan tanpa perlu menaipnya sepenuhnya.

"Apabila menulis bukti dalam LaTeX, saya sering mensimulasikan kaedah ini secara kasar dengan memotong dan menampal ungkapan panjang yang saya uruskan dari satu baris ke baris seterusnya dan kemudian mengeditnya dengan sewajarnya, tetapi ini kadangkala mengakibatkan kesilapan menaip. Ia tersebar merentasi pelbagai baris dalam dokumen, jadi adalah baik untuk dapat menulis semula secara automatik dan boleh disahkan "

Kertas itu juga menyebut ketidaksamaan, iaitu, untuk mana-mana k, l, n, jika berpuas hati, maka

.

Tao Zhexuan berkata bahawa matlamat seterusnya adalah untuk mewujudkan versi mudah ketidaksamaan ini, iaitu ketaksamaan (1.8) dalam kertas:

Bahagian bukti ini terutamanya menggunakan pengetahuan kalkulus, tetapi satu kesukaran adalah keperluan untuk menggunakan simbol asimptotik. Tao Zhexuan berkata walaupun demonstrasi berikutnya akan memakan masa, ia tidak begitu sukar.

Tetapi alatan semasa masih mempunyai beberapa had, contohnya, menulis semula ungkapan yang melibatkan pembolehubah terikat (seperti jumlah pembolehubah dalam urutan) tidak selalu mudah untuk dicapai. Dia menantikan hari apabila seseorang hanya boleh meminta LLM bahasa semula jadi untuk melakukan transformasi sedemikian...

^{Pautan rujukan: https://mathstodon.xyz/@tao/111271244206606941}

Atas ialah kandungan terperinci Tao Zhexuan bermula: Luar biasa, ia boleh meneka arah yang saya mahu dari nama teorem. Untuk maklumat lanjut, sila ikut artikel berkaitan lain di laman web China PHP!