Pembuatan Konjektur LLM vs Pemeriksaan Bukti: Siapa Unggul

Di antara kopi kedua dan ketiga, banyak peneliti teori kompleksitas baru-baru ini membaca kalimat yang tak pernah mereka duga: sebuah algoritma deterministik yang menghitung assignment yang memenuhi sebuah formula Boolean sembarang dalam waktu sekitar 2^(n/√(log n)) — sub-eksponensial, dalam arti teknis yang tepat yang membatalkan Exponential Time Hypothesis (ETH), salah satu asumsi penopang bidang ini. Klaim ini tidak muncul di arXiv dari grup universitas. Ia datang dari sebuah lab AI, dengan buktinya dikembangkan bersama large language model. Terlepas dari pendapat Anda soal pengumuman ini, ini menandai momen ketika pembuatan konjektur — mesin yang mengajukan matematika baru alih-alih sekadar menilainya — keluar dari tahap demo.

Lab tersebut mengemas tiga hasil: bom kompleksitas di atas, klaim bukti untuk konjektur Kakeya di semua dimensi, dan hasil fisika yang digambarkan sebagai penyelesaian terpadu Model Standar, yang ditahan sambil menunggu verifikasi formal. Reaksinya terbelah dengan pola yang sudah familiar: kekaguman tulus terhadap substansinya, dan kejengkelan tulus terhadap kemasannya. Para kritikus membandingkannya dengan produsen sepeda yang mengumumkan kemenangannya sendiri di balap sepeda. Tepat sekali. Namun substansinya layak dilihat lebih pelan, karena di balik pengumuman ini ada pelajaran nyata tentang dua cara sangat berbeda model bahasa kini menyentuh matematika, dan mana di antara keduanya yang benar-benar layak Anda percaya.

Apa Sebenarnya yang Diklaim Pengumuman Matematika AI Ini

Mulai dari hasil kompleksitasnya, karena taruhannya paling jelas. Exponential Time Hypothesis secara kasar menyatakan bahwa 3-SAT tidak bisa diselesaikan dalam waktu 2^o(n) — tidak ada algoritma yang bisa secara berarti sub-eksponensial terhadap jumlah variabel. Ratusan makalah di parameterized dan fine-grained complexity bersandar pada ETH untuk membuktikan batas bawah; ini jenis asumsi yang bisa Anda tumpuk dengan teorema “dengan syarat ETH” selama satu karier. Preprint baru ini menjelaskan algoritma penghitungan deterministik untuk formula k-CNF yang memakai ruang polinomial dan berjalan dalam waktu 2^(n/(log n)^(1/2+o(1))) dikali faktor polinomial. Eksponen itu o(n), dan justru itulah yang dilarang ETH. Algoritmanya tetap sangat lambat — tidak ada yang akan menjalankannya pada instans nyata — tapi secara asimtotik ini menentukan. Jika buktinya benar, hipotesis yang menopang dua dekade argumen batas bawah itu begitu saja berhenti berlaku.

Klaim kedua menyasar konjektur Kakeya, masalah teori ukuran geometris tentang himpunan terkecil yang memuat ruas garis satuan yang menghadap ke setiap arah. Kasus tiga dimensinya baru jatuh pada 2025, lewat bukti terkenal dari Hong Wang dan Joshua Zahl yang banyak orang anggap sebagai puncak karier. Pengumuman ini mengklaim bukti di semua dimensi, yang artinya akan mencakup terobosan itu sepenuhnya. Hasil ketiga, di teori medan kuantum, paling samar dari ketiganya: digambarkan sebagai “penyelesaian terpadu Model Standar” tapi belum dirilis, tampaknya menunggu formalisasi yang diperiksa mesin. Fisikawan yang membaca teaser ini menduga sesuatu dalam keluarga konstruksi bergaya grand unified, bukan teori segala sesuatu dalam arti harfiah, dan rumusan kalimatnya pantas diragukan.

Ada dua hal dalam peluncuran ini yang layak dipuji. Lab melibatkan matematikawan dan fisikawan yang bekerja sebelum mengumumkan ke publik, sebagai respons atas kritik yang muncul setelah pengumuman matematika yang lebih awal dan lebih canggung; setelah itu Terence Tao dan lainnya terus mendorong keterlibatan semacam ini. Dan hasil fisika ditahan sampai formalisasinya selesai, yang merupakan urutan prioritas yang benar. Tapi pertanyaan berat masih menggantung: tidak ada yang di luar tahu tagihan komputasinya, apakah dana setara yang diarahkan ke peneliti manusia akan menghasilkan teorema yang sama, atau apakah lab komersial akan terus membiayai riset yang didorong rasa ingin tahu setelah pemegang saham punya suara. Ada juga lingkaran tidak nyaman yang langsung disorot para kritikus: model ini dilatih sebagian dari pertanyaan, draf, dan postingan forum dari komunitas riset yang sekarang diminta memberi tepuk tangan untuk hasilnya.

Pemeriksaan Bukti vs Pembuatan Konjektur: Dua Pekerjaan Berbeda

Jika hype disingkirkan, setiap sistem AI-untuk-matematika pada dasarnya melakukan salah satu dari dua pekerjaan. Pekerjaan pertama adalah pemeriksaan bukti: diberi sebuah argumen kandidat, putuskan apakah itu valid. Pekerjaan kedua adalah pembuatan konjektur: diberi suatu area masalah, usulkan apa yang layak dicoba, seperti lemma, konstruksi, algoritma, atau contoh balik. Keduanya terdengar seperti dua separuh dari satu keterampilan. Bukan. Keduanya adalah masalah komputasi yang berbeda dengan oracle yang berbeda, mode kegagalan yang berbeda, dan profil kepercayaan yang sangat berbeda. Mencampuradukkannya adalah cara Anda berakhir terlalu percaya pada siaran pers, atau malah meremehkan kemajuan nyata.

Pemeriksaan punya oracle. Bukti yang ditulis di Lean akan lolos kompilasi terhadap kernel atau tidak, dan kernel tidak peduli seberapa yakin penulisnya terdengar. Pemeriksaan gagal dengan keras, karena blok taktik yang ditolak tidak ambigu. Pembuatan tidak punya oracle. Konjektur yang diajukan bisa benar, salah, sepele, atau benar tapi sudah diterbitkan tahun 1987 dengan notasi berbeda. Pembuatan gagal diam-diam, dan mode kegagalannya bersifat sosial: omong kosong yang terdengar masuk akal, atau hasil asli yang dibungkus sebagai kebaruan. Kualitasnya di sini diukur dari kepentingan dan orisinalitas, sifat-sifat yang ditentukan oleh selera manusia, bukan kriteria yang bisa diputuskan secara mekanis.

Mengapa pembuatan tiba-tiba cukup bagus untuk berarti? Karena model penalaran modern dilatih untuk rantai pemikiran panjang, bukan sekadar dipaksa lewat prompt. Reinforcement learning dengan reward yang bisa diverifikasi, terutama di matematika dan kode di mana jawaban bisa diperiksa secara mekanis, mengajari sistem ini untuk benar-benar mencari di ruang langkah alih-alih melengkapi satu per satu. Analogi yang saya sarankan Anda simpan: pemeriksa bukti adalah kompilator, pembuat konjektur adalah desainer. Keduanya berharga. Anda tidak akan pernah, sekali pun, membiarkan desainer mensertifikasi karyanya sendiri.

Bukti yang tidak bisa Anda periksa adalah khotbah; konjektur yang tidak bisa Anda uji adalah rumor.

Di Mana Pemeriksaan Bukti Otomatis Menang

Pemeriksa menang di mana pun ada kebenaran formal dan artefak yang ditinjau terlalu panjang atau membosankan untuk diaudit manusia baris demi baris. Lean 4 dan pustaka komunitasnya Mathlib telah menjadi arena de facto di sini: Anda menulis definisi dan bukti dalam bahasa pemrograman, dan sebuah kernel kecil yang bisa diaudit terpisah memutuskan apakah setiap langkah inferensi legal. Trusted computing base-nya kecil dibanding gunung matematika yang dibangun di atasnya, dan itulah asimetri yang Anda inginkan.

Loop praktisnya begini: model membuat draf langkah bukti tingkat taktik, kernel menerima atau menolak setiap langkah, dan pesan penolakan diumpankan kembali sebagai konteks untuk percobaan berikutnya. Ini satu-satunya setting di mana membatasi output model ke grammar yang ketat langsung terbayar. Anda hanya mengambil sampel taktik yang valid secara sintaksis, sehingga kelas halusinasi tertentu menjadi mustahil secara konstruksi. Berikut contoh minimal, jenis lemma yang kini bisa diselesaikan model dalam hitungan detik:

import Mathlib
-- The sum of two even natural numbers is even.
theorem even_add_even {a b : ℕ} (ha : Even a) (hb : Even b) : Even (a + b) := by
rcases ha with ⟨k, rfl⟩   -- a = k + k for some k
rcases hb with ⟨l, rfl⟩   -- b = l + l for some l
exact ⟨k + l, by ring⟩    -- witness k + l; ring closes the algebra

Perhatikan apa yang ditunjukkan contoh ini tentang pembagian kerja. Langkah kreatifnya adalah memilih witness k + l; langkah pemeriksaannya adalah ring yang memverifikasi aljabarnya. Manusia dan model sama-sama cukup baik di yang pertama. Hanya kernel yang terpercaya di yang kedua, dan ia tidak pernah lelah, tidak pernah melewatkan, dan tidak pernah menilai berdasarkan feeling. Elemen paling kredibel dari seluruh pengumuman ini justru gerbang ini: klaim bahwa makalah fisika ditahan sampai formalisasi Lean-nya selesai. Jika penjelasan itu akurat, ini alur kerja yang berfungsi persis seperti seharusnya. Mesin mengusulkan, mesin memutuskan, dan siaran pers menunggu gilirannya.

Di Mana Pembuatan Konjektur Menang

Pembuatan menang di mana pun ruang pencariannya kombinatorial dan evaluasinya murah. FunSearch dari DeepMind menetapkan templatenya pada 2023: model bahasa mengusulkan hipotesis berbentuk program, evaluator cepat memberi skor, dan loop evolusioner menyimpan yang terbaik. Pengaturan ini menghasilkan konstruksi baru untuk cap set dan heuristik bin-packing yang lebih baik daripada puluhan tahun penyetelan manual. AlphaEvolve mendorong ide yang sama lebih jauh dan, antara lain, memangkas satu perkalian dari algoritma perkalian matriks 4×4 yang bertahan sejak era Strassen. Tidak ada yang mengklaim sistem ini memahami geometri. Mereka tidak perlu. Mereka hanya perlu mengusulkan, dan evaluatornya harus jujur.

Algoritma ETH cocok dengan pola ini hampir mencurigakan. Ruang “ide algoritmik” sangat besar, dan peneliti manusia menjelajahinya dengan prior yang kuat, yang sebenarnya berarti titik buta. Konstruksi yang membutuhkan komposisi trik representasi tertentu dengan struktur rekursi tertentu bisa tak tersentuh selama tiga dekade hanya karena jalur pencarian siapa pun tidak pernah lewat dekatnya. Pencarian yang menyeluruh, tanpa prior, dan agak “bodoh” justru yang dibawa mesin ke meja. Logika yang sama menggerakkan loop generate-and-refute: usulkan konjektur, lalu langsung coba jatuhkan dengan pencarian komputasional untuk contoh balik pada kasus kecil. Sebagian besar konjektur mati dalam hitungan menit, dan itu tidak masalah. Setiap penyangkalan mempertajam usulan berikutnya, dan yang bertahan adalah yang layak mendapat sore seorang manusia.

Ada juga asimetri psikologis yang patut dihormati. Bukti Kakeya tiga dimensi dari Wang dan Zahl butuh bertahun-tahun usaha terfokus di puncak bidang ini. Jika pencarian yang dibantu model benar-benar menghasilkan argumen untuk semua dimensi, kemungkinan besar ia menemukan rute berbeda melalui lanskap. Belum tentu lebih dalam, tapi berbeda, dan berbeda justru untuk itulah pencarian. Bahayanya bukan mesin membuat konjektur; bahayanya adalah seseorang mempublikasikan konjektur hasil generasi tanpa perangkat yang mendukungnya. Yang membawa kita ke bagian pipeline yang benar-benar perlu Anda bangun.

Membangun Loop Verifikasi untuk Bukti Hasil AI

Jika Anda ingin manfaat matematika buatan mesin tanpa rasa malu, alurnya lebih penting daripada modelnya. Ini pipeline yang akan saya jalankan, berurutan:

1. Hasilkan secara luas dan murah. Keberagaman mengalahkan kedalaman di tahap ini; Anda ingin cakupan ruang ide, bukan satu percobaan yang sudah dipoles.
2. Hapus duplikasi terhadap literatur. Retrieval di arXiv dan MathOverflow menangkap kegagalan paling umum: konjektur “baru” yang ternyata hasil lama dengan notasi yang tidak familiar.
3. Terapkan filter empiris yang murah. Uji kasus kecil secara numerik, cari contoh balik secara komputasional, dan biarkan pernyataan yang jelas salah mati cepat.
4. Formalkan yang bertahan. Lean, Isabelle, atau Rocq. Pilih asisten bukti Anda, tapi pahami bahwa ini langkah yang mahal dan bukti bahasa alami hanyalah sketsa, bukan hasil.
5. Tinjauan manusia untuk kebaruan dan framing. Apakah ini penting? Apakah pernyataannya memang yang tepat? Model mengoptimalkan apa yang bisa dibuktikan; manusia memutuskan apa yang layak dibuktikan.

Kolaborasi yang diumumkan kira-kira mengikuti bentuk ini: peneliti dilibatkan sebelum rilis, secara efektif mengisi langkah kelima. Itu peningkatan nyata dibanding cara lama, yaitu menjatuhkan preprint dan membiarkan media sosial menjadi wasit. Tapi perhatikan asimetri pipeline ini: langkah satu sampai tiga murah dan skalanya mengikuti komputasi, langkah empat adalah bottleneck, dan langkah lima sama sekali tidak skalabel. Jika Anda membangun tooling di bidang ini, belanjakan uang Anda di bottleneck, seperti autoformalisasi yang lebih baik dan umpan balik error yang lebih baik ke generator, bukan pada generator yang lebih besar dan lebih percaya diri.

Mengapa Matematikawan Manusia Masih Menjaga Gerbang Kebenaran

Tidak ada verifier yang bisa memberi tahu Anda bahwa sebuah teorema penting. Pemilihan masalah adalah selera, dan selera adalah teknologi sosial yang dibangun selama puluhan tahun: seminar, laporan referee, dan konsensus lambat tentang pertanyaan mana yang membuka pintu dan mana yang jalan buntu. Skeptisisme komunitas riset terhadap pengumuman vendor bukan sekadar penjagaan gerbang demi gerbang. Itu sistem imun, dan sistem imun kadang bereaksi berlebihan justru karena kurang bereaksi itu fatal.

Lalu ada soal provenance. Model ini dilatih dari pertanyaan, draf, dan postingan forum komunitas itu sendiri, yang memunculkan kemungkinan tidak nyaman bahwa sebuah “penemuan” yang dirayakan ternyata rekombinasi dari hal-hal yang ditulis oleh referee masa depannya. Ketakutan akan “berlomba” melawan alat Anda sendiri bukan paranoia. Ini masalah lineage data, dan sampai lab bisa menunjukkan lineage, referee manusia tetap satu-satunya pendeteksi plagiarisme yang berfungsi. Tambahkan politik kredit, seperti siapa yang diundang untuk memverifikasi, nama siapa yang muncul di pengumuman, dan tuduhan favoritisme, dan Anda paham mengapa gerbang manusia tidak bisa dihapus. Memilih lima ilmuwan terkemuka untuk memberkati sebuah hasil sama politisnya dengan epistemiknya.

Satu peringatan lagi bagi siapa pun yang tergoda membaca papan peringkat sebagai kemampuan riset: medali emas kompetisi mengukur performa pada soal yang dirancang agar bisa diselesaikan dalam hitungan jam. Riset adalah kebalikannya, yakni soal yang dipilih justru karena tidak ada yang tahu apakah ia bisa diselesaikan. Ini alasan yang sama mengapa benchmark melewatkan sebagian besar pekerjaan nyata dalam rekayasa perangkat lunak: metriknya menghargai soal yang sudah dibentuk, bukan yang berantakan. Model yang unggul di soal olimpiade memang telah menunjukkan sesuatu yang nyata. Ia belum menunjukkan penilaian.

Rekomendasi: Percaya pada Loop, Bukan pada Model

Ini posisi saya, saya nyatakan terus terang. Generasi konjektur itu nyata, berguna, dan hanya akan membaik. Generasi konjektur tanpa verifikasi tidak berharga, dan bukti bahasa alami tanpa dukungan formal sebaiknya diperlakukan sebagai pemasaran sampai terbukti sebaliknya. Pemeriksaan bukti menang setiap kali artefaknya harus dipercaya. Pembuatan menang setiap kali bottleneck-nya imajinasi, bukan ketelitian. Pengumuman yang penting adalah yang menyatukan keduanya.

Jadi perlakukan model sebagai rekan junior yang produktif dengan energi tak terbatas dan tanpa penilaian: apa pun yang diberikannya harus lewat asisten bukti sebelum masuk ke makalah, dan lewat manusia yang punya selera sebelum masuk ke pendahuluan. Jika Anda seorang peneliti, pelajari satu asisten bukti dengan benar. Formalisasi adalah bottleneck, dan orang yang bisa mengendalikannya akan sangat sibuk. Jika Anda membangun tool, bangun loop-nya, bukan demo-nya. Dan saat pengumuman besar berikutnya datang, lewati siaran pers, buka preprint-nya, dan periksa apakah repositori Lean-nya ada. Klaim yang bertahan adalah yang datang dalam keadaan sudah diperiksa mesin.