OpenAI mengklaim model AI generasi berikutnya mereka telah memecahkan 10 masalah kelas dunia, termasuk membantah Connes Rigidity Conjecture.
Keesokan harinya, muncul respons dari sebuah makalah manusia: Contra-example yang diajukan AI tidak valid.
Penulisnya adalah J. L. Nielsen dari Kansas University's Center for Topological Physics. Dia menelusuri 37.000 baris kode Lean 4 yang dipublikasikan OpenAI dari awal hingga akhir, memetakan setiap objek kembali ke prototipe matematikanya, dan akhirnya memberikan dua jalur kegagalan yang independen.
Proses pembuktiannya sendiri kurang bisa dipahami orang awam, serahkan saja perdebatan ini kepada AI dan matematikawan.
Tapi melalui kejadian ini, terlihat bahwa pengawasan manusia terhadap hasil penelitian AI masih sangat krusial.
Apa itu Connes Rigidity Conjecture?
Connes Rigidity Conjecture berbicara tentang hal ini.
Dalam matematika, sebuah grup dapat dilengkapi dengan struktur aljabar. Terkadang dua grup yang tampak berbeda, menghasilkan struktur yang persis sama.
Connes mengajukan dugaan sekitar tahun 1980: Asalkan grup ini memenuhi dua kondisi tambahan, situasi seperti itu tidak akan terjadi. Jika strukturnya sama, maka grupnya harus sama.
Dua kondisi tambahan itu, satu disebut ICC, dan satunya lagi disebut properti Kazhdan (T).
Dengan kata lain, untuk membantah dugaan ini, perlu memberikan contoh grup yang memenuhi kedua kondisi tersebut, tetapi konstruksinya berbeda.
Cara model baru OpenAI adalah dengan mengonstruksi dua grup yang tidak isomorfik, yang menghasilkan aljabar yang sama, dan memberikan bukti bahwa kedua grup tersebut memenuhi ICC dan properti (T).
Seluruh argumen ditulis menjadi 37.000 baris kode Lean 4, diverifikasi baris demi baris oleh kernel Lean, serta dilengkapi dengan dokumen penjelasan tentang bagaimana kedua grup itu dibangun.
Nielsen menunjukkan: Salah satu grup yang dikonstruksi AI, sebenarnya tidak memenuhi kondisi tambahan, bukan ICC, juga tidak memiliki properti (T).
Ada tiga kemungkinan di sini:
Properti (T) dalam kode tidak sesuai setia dengan definisi asli Kazhdan; atau bukti hanya berlaku untuk sebagian, tetapi dianggap berlaku untuk seluruh grup; atau grup dalam kode sama sekali bukan seperti yang digambarkan dalam dokumen penjelasan.
37.000 Baris, Dicocokkan Satu per Satu
Untuk memverifikasi kesimpulan ini, Nielsen melakukan hal yang lebih melelahkan.
Kode yang dipublikasikan adalah versi yang digabungkan menjadi satu file, nama-nama dari kode sumber awal yang terpisah menjadi modul sudah tidak ada.
Dia kemudian membuat tabel pencocokan, menandai nama dan nomor baris setiap objek matematika dalam kode baru:
Cohomologi nol di atas siklus tertutup ada di baris 13700, grup terdistorsi di baris 14069, bukti isomorfisme dua aljabar di baris 36712, teorema utama di baris 36954.
Dia juga menelusuri seluruh rantai penalaran yang membuktikan ICC dalam kode. Rantai ini dimulai dari baris 31430, disalurkan ke atas lapis demi lapis, dan akhirnya mensintesis kesimpulan di baris 31610.
Masalah yang ditunjukkan Nielsen adalah, lemma-lemma ini menangani objek setelah transformasi dual, bukan grup asli dengan elemen pusat, sehingga tidak secara langsung mencakup elemen-elemen kunci tersebut.
Apakah lemma-lemma ini berlaku untuk setiap elemen dalam grup spesifik yang masuk ke dalam teorema akhir, tergantung pada bagaimana antarmuka antara dua blok konstruksi tersebut terhubung.
Ini menunjukkan bahwa masalahnya ada pada "apa yang ingin dibuktikan", bukan pada "apakah pembuktiannya benar". Lean hanya bertanggung jawab memverifikasi yang terakhir.
Untuk grup terdistorsi lainnya, Nielsen bersikap konservatif. Dia mengatakan tidak memverifikasi secara independen dari kode apakah grup itu benar-benar memenuhi ICC atau tidak, dan mengakui bahwa lemma dalam kode mungkin memang membuktikannya terpenuhi, tetapi itu tidak mengubah kesimpulan, karena satu syarat sudah tidak terpenuhi.
Dia juga menuliskan dua sanggahannya dalam kode Lean, yang dikompilasi di bawah Lean 4.32.2.
Mesin Memeriksa Bentuk, Bukan Makna
Bagian terakhir makalah menempatkan peristiwa ini dalam konteks yang lebih besar.
Apa yang dapat dijamin oleh kernel Lean hanyalah bahwa suatu bukti secara formal sempurna, tetapi tidak bertanggung jawab apakah bukti itu benar-benar membuktikan kesimpulan asli.
Di sini kita bisa mengutip langsung pernyataan Terence Tao: Yang diverifikasi adalah pernyataan formal itu sendiri, bukan apakah pernyataan itu sesuai dengan niat, sehingga pengawasan manusia tidak dapat langsung digantikan.
Insiden seperti ini sudah ada catatannya di masa lalu.
Sebuah audit terhadap lima benchmark Lean yang umum digunakan menghasilkan 4833 temuan, termasuk counterexample, teorema kosong, dan aksioma yang tidak dapat diandalkan, yang semuanya lolos verifikasi mesin. Pada akhirnya, manusia yang mengonstruksi counterexample baru menyadari bahwa pernyataan yang dibuktikan itu sendiri salah.
Dalam pekerjaan formalisasi teori pembelajaran statistik, skenario paling berbahaya digambarkan sebagai "bukan bukti yang gagal, tetapi bukti yang sukses terhadap pernyataan yang salah".
Penelitian tentang jaringan tensor juga mencatat fenomena serupa: Bukti yang diberikan sistem benar secara formal sepenuhnya, hanya saja proposisi yang dibuktikannya lebih lemah dari yang diharapkan.
Nielsen menulis, formalisasi OpenAI itu mungkin membangun setiap klaim yang disebutkannya dengan benar. Tetapi yang tidak dibangun, dan tidak dapat diperiksa oleh kernel Lean, adalah apakah kesimpulan-kesimpulan itu berkaitan dengan kata-kata asli dari dugaan tersebut.
Manusia membaca dugaan akan melihat premisnya, asisten pembuktian yang menerima kesimpulan yang tidak memenuhi premis, akan tetap memverifikasi setiap pernyataan tentangnya.
Connes Rigidity Conjecture masih terbuka.
Alamat makalah:
https://philarchive.org/archive/NIEWTCv17
Tautan referensi:
[1]https://openai.com/index/ten-advances-in-mathematics/
[2]https://github.com/openai/ten-proofs/blob/main/ConnesRigidity.lean
Artikel ini berasal dari akun WeChat publik "量子位", penulis: Meng Chen
