Lean4 Membantu Menemukan Bug Kecil dalam Makalah Terbaru Terence Tao

• Terence Tao menemukan kesalahan kecil tetapi tidak sepele dalam makalahnya saat mengerjakan proyek formalisasi Lean4
• Kesalahan itu muncul dalam argumen di halaman 6 makalah arXiv 2310.05328, ketika 1/2 log((n - 1)/(n - k - 1)) divergen pada n = 3, k = 2
• Masalah ini terbatas pada nilai n kecil; untuk n >= 8 argumen lama tetap bekerja, dan untuk n kecil kasusnya bisa ditangani langsung dengan metode yang lebih kasar
• Lean meminta pembuktian 0 < n - 3, tetapi asumsi yang tersedia hanya n > 2, sehingga taktik linarith tidak bisa memperoleh kontradiksi yang diperlukan
• Tao berencana memperbaiki argumen dengan menyesuaikan beberapa konstanta numerik, dan menambahkan catatan kaki pada versi baru bahwa ketidakakuratan dalam argumen sebelumnya ditemukan saat mencoba memformalkannya di Lean

---

Kesalahan yang Terungkap oleh Formalisasi Lean4

• Terence Tao menemukan adanya bug kecil tetapi tidak sepele dalam makalahnya selama proses proyek formalisasi Lean4 miliknya
• Target formalisasi adalah argumen di halaman 6 dari makalah arXiv 2310.05328
• Bentuk ekspresi yang menjadi masalah adalah sebagai berikut
  • 1/2 log((n - 1)/(n - k - 1))
• Ekspresi ini divergen dalam kasus n = 3, k = 2

Cakupan Kesalahan dan Cara Memperbaikinya

• Masalah ini hanya muncul pada nilai n yang kecil
  • Untuk n >= 8, argumen tersebut tetap bekerja
  • Untuk n kecil, kasusnya bisa ditangani langsung dengan metode yang lebih kasar, tetapi konstantanya menjadi lebih buruk
• Tao menilai argumen tersebut bisa diperbaiki dengan mengubah beberapa konstanta numerik pada halaman itu
• Dalam versi baru makalahnya, ia berencana menambahkan catatan kaki bahwa argumen sebelumnya agak tidak akurat, dan hal itu ditemukan saat mencoba memformalkannya dengan Lean

Titik Spesifik Saat Lean Terhenti

• Pada titik ketika formalisasi gagal, Lean meminta pembuktian 0 < n - 3
  • Asumsi yang tersedia hanya n > 2
  • Taktik linarith tidak dapat menurunkan kontradiksi dari negasi 0 < n - 3

[GN⁺]

Komentar Hacker News

• Ia mulai belajar Lean4 dengan bantuan GPT-4 awal bulan ini: https://mathstodon.xyz/@tao/111208692505811257
  Cukup banyak tulisan Mastodon-nya bulan ini membahas progres belajarnya, dan ini merupakan contoh menarik tentang seberapa jauh model bahasa besar dapat mempercepat pekerjaan bahkan bagi para pencapai tingkat teratas

  • Ternyata orang yang punya kemampuan komunikasi baik, meski tidak bisa coding, dapat dengan cepat membuat otomasi yang berjalan dengan model bahasa besar
    Menariknya, alat seperti ini juga bisa memperlebar ketimpangan jika hanya orang-orang berketerampilan tinggi yang mampu memanfaatkannya secara efektif
  • GPT-4 luar biasa. Belakangan ini saya hampir tidak lagi memakai Google saat mulai mengajukan pertanyaan terkait pemrograman
  • Saya cukup setuju, tetapi Terry adalah sosok yang terlalu luar biasa, jadi menurut saya sulit menggeneralisasi kasus ini. Tentu saja ia juga orang yang murah hati dan rendah hati
  • Bagi kalangan elite, ini dengan mudah menjadi alat 100x. Kini engineer paling atas adalah orang-orang dengan produktivitas 10000x

• Kalau ingin mulai mengenal Lean4 dengan mudah, Natural Number Game bagus: https://adam.math.hhu.de/#/g/hhu-adam/NNG4
  Kalau hanya ingin membaca tanpa gim, di sini: https://lean-lang.org/theorem_proving_in_lean4/introduction.html

  • Saya pemula, jadi penasaran: apa bedanya Lean4 dengan TLA+ atau Alloy? Saya juga penasaran apakah memang layak dibandingkan sejak awal
    Awalnya saya sempat menulis Alloy sebagai Allow

• Beberapa tahun lalu, saat mencari cara mengurangi kesalahan dalam program yang saya tulis, saya menemukan TLA+ dari Lamport, lalu belajar menulis spesifikasi formal dengan memikirkan perilaku program sebagai state machine
  TLA+ membantu saya memahami abstraksi dengan jelas, dan setelah itu saya juga menemukan seri Software Foundations, yang menggunakan asisten pembuktian Coq untuk membuat software yang benar secara formal. Soal latihannya dibuat seperti gim kecil, jadi cukup menyenangkan untuk dikerjakan: https://softwarefoundations.cis.upenn.edu/

  • Ketepatan kode sudah menjadi keterampilan yang hilang. Tuntutan untuk berpikir secara abstrak membuat banyak developer gentar
    Spesifikasi formal sebagai abstraksi tingkat tinggi berfokus pada bahasa khusus untuk menjelaskan kode, sedangkan kontrak kode sebagai abstraksi tingkat rendah lebih mendekati penggantian logika verifikasi dengan model yang lebih baik. C# dulu pernah punya Code Contracts[1], pendekatan sederhana tetapi kuat yang memeriksa kontrak pada waktu kompilasi dengan Z3 SMT solver[2], tetapi beberapa tahun kemudian dihentikan[3], lalu secara praktis berakhir ketika dihapus dari .NET Runtime. Saat ini yang paling dekat di C# mungkin Dafny[4], dan sisi pengembangan C# masih memikirkan cara memasukkannya langsung ke dalam bahasa[5]
    [1] https://www.microsoft.com/en-us/research/project/code-contracts/
    [2] https://github.com/Z3Prover/z3
    [3] https://github.com/microsoft/CodeContracts
    [4] https://github.com/dafny-lang/dafny
    [5] https://github.com/dotnet/csharplang/issues/105
  • Saya penasaran apakah Anda juga sudah melihat Idris2. Setiap kali melihat pembukti teorema seperti ini, rasanya ada ketidakcocokan impedansi dengan pemrograman umum
    Idris2 tampaknya menargetkan bahasa serbaguna sekaligus menyediakan sistem tipe yang lebih maju untuk pembuktian teorema: https://github.com/idris-lang/Idris2
  • Saya juga punya pengalaman positif yang sama dengan Software Foundations
    Ada juga buku yang agak turunan, menggunakan Agda alih-alih Coq: https://plfa.github.io/
    Saya belum sempat membacanya, tetapi sudah saya masukkan ke daftar, dan menurut saya Agda atau Idris kemungkinan lebih terasa seperti bahasa pemrograman dibanding Coq

• Dependent types benar-benar membuat saya antusias. Namun tampaknya sulit hadir dalam waktu dekat
  Dependent Haskell sedang berjalan, tetapi katanya sulit disisipkan belakangan ke bahasa yang sudah ada, dan pembuat Idris juga mengatakan berharap Idris menjadi model bagi bahasa lain, sementara adopsi arus utama tampaknya sulit. Coq, Agda, F* juga tidak dirancang sebagai bahasa serbaguna. Implementasi compiler rumit dan sintaksnya bisa menjadi bertele-tele, tetapi yang saya inginkan adalah kesederhanaan. Saya ingin mengodekan semua hal yang diketahui tentang input dan output. Dalam bahasa arus utama saat ini, sering kali kita tahu lebih banyak tentang argumen atau output daripada yang bisa diekspresikan oleh sistem tipe

  • Saya sepenuhnya memahami antusiasme terhadap dependent types, tetapi berbeda dari sistem tipe yang biasa kita pakai, teorema tentang dependent types jauh lebih sulit dibuktikan, jadi tampaknya tidak nyaman digunakan untuk keseluruhan program
    Akan bagus jika, dengan cara bertahap seperti TypeScript, kita bisa menambahkan informasi pembatasan nilai tingkat tipe di lokasi mana pun tanpa harus membuktikan semuanya di semua tempat
  • Penjelasan sederhana tentang dependent types: konsep bahwa tipe suatu variabel dapat bergantung pada nilai variabel lain
    Misalnya, jika kita mengetahui daftar angka beserta panjangnya, dengan dependent types kita dapat membuat tipe daftar yang secara eksplisit menyertakan panjang, dan pada waktu kompilasi memastikan bahwa operasi menjaga panjang tersebut. Jika kita menetapkan fungsi yang hanya menerima daftar panjang 3 tetapi memberinya daftar panjang 4, itu tidak akan dikompilasi, sehingga kesalahan dapat ditangkap sebelum runtime. Rasanya seperti lapisan pemeriksaan keamanan tambahan yang membuat tipe lebih ekspresif dan bahkan dapat mengodekan relasi kompleks antarvariabel

• Jika salah satu intelektual paling menonjol di generasi kita bisa memperluas cakupan pekerjaannya lewat kombinasi model bahasa besar dan pembuktian otomatis, masa depan kombinasi teknologi ini tampak sangat optimistis.
  Awalnya berupa perbaikan bug, lalu membantu verifikasi, dan pada akhirnya tampaknya akan mendorong penemuan baru serta memperluas batas-batasnya. Kita butuh istilah untuk fenomena ketika dinamika seperti Hukum Moore “menginfeksi” bidang-bidang yang semula tidak memiliki sifat akumulatif semacam itu. Sebagai konteks tambahan, Terence Tao memakai Copilot untuk belajar Lean: https://mathstodon.xyz/@tao/111271244206606941
  Ia mungkin bisa melakukannya tanpa Copilot, tetapi gesekan dalam mengadopsi alat baru mungkin saja membuatnya tidak mulai. Model bahasa besar punya potensi besar dalam situasi semacam “sepeda untuk pikiran” ini.

  • Lean 4 adalah bahasa pemrograman sekaligus pembukti teorema, dan sejauh yang saya tahu tidak terkait dengan model bahasa besar.
  • Model bahasa besar adalah kompiler untuk bahasa alami seperti bahasa Inggris.

• Beberapa tahun lalu saya juga pernah menemukan satu bug di tulisan blog matematika Terence Tao. Saya memberi tahu dia, lalu ia memperbaikinya dan mengucapkan terima kasih.
  Tentu saja itu tidak sampai masuk halaman depan Hacker News.

  • Untuk yang berminat, saya menulis lebih rinci di tulisan blog saya: https://news.ycombinator.com/item?id=38040982

• Saya sempat khawatir Lean4 adalah model bahasa besar lain, tetapi ternyata ia alat yang cukup kokoh dan dapat diandalkan.

  • Kalau alat itu membantu Terence Tao menemukan bug dalam makalahnya, menurut standar saya itu sudah cukup kokoh dan dapat diandalkan.
  • Komunitas Lean 4 cukup optimistis dalam menggabungkan model bahasa besar dan pembukti teorema untuk bantuan pembuktian serta formalisasi.
  • Kalau beritanya adalah “Terry Tao memakai ChatGPT dan merasa itu sangat berguna untuk membuktikan teorema baru”, secara pribadi itu mungkin akan terasa sebagai berita yang lebih besar daripada kabar ini.
  • Ia menilai Copilot berguna untuk pekerjaan formalisasi: https://mathstodon.xyz/@tao/111271244206606941

• Saya penasaran apakah mungkin menggabungkan pemeriksa bukti formal seperti pemeriksa bukti Lean dengan model bahasa yang menghasilkan pasangan konjektur-bukti sintetis dalam bahasa formal seperti Lean.
  Pemeriksa bukti Lean dapat memverifikasi otomatis apakah bukti sintetis yang ditulis model bahasa itu benar, lalu informasi tersebut bisa dipakai sebagai sinyal reward reinforcement learning untuk diterapkan kembali ke model bahasa semula agar ia menulis bukti yang lebih baik. Atau, bukti sintetis yang benar dari putaran sebelumnya dapat dijadikan data latih untuk melatih model baru. Ini juga bisa dibuat lebih adversarial. Pisahkan menjadi model pembuat konjektur dan model pembukti/penyangkal, lalu tambahkan model yang memprediksi apakah bukti sintetis akan diverifikasi oleh pemeriksa bukti Lean. Semakin rendah probabilitas jawaban benar yang diprediksi, semakin besar reward yang diterima model pembuat bukti ketika ia benar-benar menghasilkan bukti yang valid. Terakhir, jika ditambahkan model yang memprediksi reward yang akan diterima model pembuat bukti untuk konjektur sintetis tertentu, maka model pembuat konjektur diberi reward untuk membuat konjektur dengan perkiraan reward tinggi yang tidak terlalu sulit maupun terlalu mudah bagi model pembuat bukti. Seluruh sistem dapat menghasilkan bukti sintetis yang semakin sulit, dan ini bisa mengarah pada self-learning yang lebih baik bagi model pembuat bukti. Secara prinsip, ini bisa diskalakan hingga kemampuan superhuman dalam pembuatan bukti, mirip dengan GAN atau self-play AlphaGo Zero. Bagian yang sulit adalah bootstrapping awal: pelatihan pertama model generatif memerlukan data bukti Lean yang disediakan manusia. Namun jika bukti sintetis sudah cukup baik, sistem dapat melanjutkan self-learning secara otomatis

  • Alur kerja ini adalah tujuan eksplisit para pengembang Lean 4. Di chat Zulip resmi juga ada kanal yang membahas antarmuka antara keduanya: https://leanprover.zulipchat.com/#streams/219941/Machine%20Learning%20for%20Theorem%20Proving
  • Menarik juga jika model seperti ini dilatih dengan seluruh literatur matematika. Orang akan tergoda memakainya untuk menerjemahkan bukti dalam literatur matematika ke bentuk yang dapat diverifikasi, lalu memverifikasinya.
    Pada akhirnya kita bisa mendapatkan model yang mengetahui semua teorema dan semua bukti yang benar dalam literatur matematika
  • Sepertinya kita sudah memasuki dunia sintesis bukti berbasis machine learning. Saya tidak menganggap keseluruhan sistem yang dijelaskan itu sudah selesai, tetapi ada banyak sistem dan komponen serupa.
    Untuk tahap awal yang memulai dengan supervised learning dari bukti yang sudah ada lalu mencari bukti baru, ada TacticToe (https://arxiv.org/abs/1804.00596), Tactician (https://arxiv.org/pdf/2008.00120.pdf), CoqGym/ASTactic (https://arxiv.org/abs/1905.09381), Proverbot9001 (https://arxiv.org/abs/1907.07794), Diva (https://dl.acm.org/doi/10.1145/3510003.3510138#sec-terms), dan lainnya. Sebagian besar memiliki semacam model bahasa di dalamnya, tetapi jika mencari model bahasa besar yang belakangan menarik banyak perhatian, ada GPT-f (https://arxiv.org/abs/2009.03393), Baldur (https://arxiv.org/abs/2303.04910), dan COPRA (https://arxiv.org/abs/2310.04353). Namun untuk saat ini, model-model seperti ini tampaknya belum seefektif tool khusus non-LLM. Untuk arah yang belajar dengan reinforcement learning melampaui bukti yang ditulis manusia, ada TacticZero (https://openreview.net/forum?id=edmYVRkYZv), makalah OpenAI (https://arxiv.org/pdf/2202.01344.pdf), rlCoP (https://arxiv.org/abs/1805.07563), lini kerja HOList (https://arxiv.org/pdf/1905.10006.pdf), HyperTree Proof Search (https://arxiv.org/abs/2205.11491), serta pekerjaan yang sedang saya lakukan bersama tim University of Massachusetts
  • Sudah ada orang yang melakukan ini. Contoh dari sisi Lean ada di sini: https://morph.so/blog/the-personal-ai-proof-engineer/

• Konteks sebelumnya tentang bagaimana Tao menggunakan tool model bahasa besar, termasuk GPT-4, dalam perjalanan ini ada di sini: https://mathstodon.xyz/@tao/111233986893287137

• Perkembangannya juga dapat diikuti di GitHub: https://github.com/teorth/symmetric_project/