PSI Melaporkan Bukti Konjektur Aaronson-Ambainis yang Diperiksa Mesin

Physical Superintelligence mengumumkan pada 6 November 2026 bahwa sebuah sistem riset internal yang menjalankan beberapa instans model Anthropic nonpublik telah menemukan bukti untuk konjektur Aaronson-Ambainis, masalah komputasi kuantum yang belum terpecahkan sejak 2008.

Sistem tersebut menghasilkan bukti lengkap pada hari ketiga pengoperasian di infrastruktur PSI sendiri, dan asisten pembuktian Lean menerimanya. PSI kemudian memberikan sejumlah masalah terbuka terkait kepada sistem itu, yang dua kali menyempurnakan hasilnya sebelum Lean menerima versi final. Naskah dan formalisasi Lean 4 tersedia untuk umum.

Apa yang Dinyatakan Konjektur Ini tentang Percepatan Kuantum

Pertanyaannya adalah kapan komputer kuantum dapat bekerja secara eksponensial lebih cepat daripada komputer klasik. Algoritma pemfaktoran Shor pada 1994 bergantung pada struktur: masukannya memiliki pola berulang yang dapat dimanfaatkan algoritma tersebut. Hasil PSI membahas kasus yang berlawanan, yakni masukan acak atau tidak terstruktur, yang umumnya tidak memiliki pola seperti itu.

Dalam model kueri, algoritma klasik membaca satu bit untuk setiap kueri, sedangkan kueri kuantum dapat disebarkan dalam superposisi ke banyak posisi masukan. Penjelasan PSI menghubungkan model ini dengan polinomial: setelah T kueri kuantum, probabilitas algoritma menjawab “ya” merupakan polinomial terbatas dari bit-bit masukan dengan derajat paling tinggi 2T. Karena itu, menyimulasikan algoritma kuantum berarti memperkirakan polinomial tersebut tanpa membaca bit masukan dalam jumlah eksponensial.

Dalam makalah asli mereka, Scott Aaronson dan Andris Ambainis mengajukan konjektur bahwa setiap polinomial berderajat rendah yang terbatas memiliki variabel yang sangat berpengaruh. Mereka membuktikan bahwa, jika konjektur itu berlaku, setiap algoritma kuantum dengan T kueri dapat disimulasikan pada sebagian besar masukan oleh algoritma klasik yang melakukan kueri sebanyak jumlah polinomial dalam T. Artinya, jumlah kueri klasik bertambah secara polinomial, bukan eksponensial, untuk setiap galat pendekatan dan fraksi masukan yang dikecualikan yang ditetapkan; hasil ini tidak meniadakan keunggulan kuantum eksponensial untuk masalah dengan struktur yang sesuai.

Secara formal, repositori tersebut membahas polinomial riil p berderajat paling tinggi d, yang nilainya pada kubus diskret berada di antara 0 dan 1. Jika variansnya atas masukan acak yang dipilih secara seragam setidaknya ε, ada suatu koordinat yang memiliki pengaruh setidaknya (8√15 / (125π⁴)) · ε^(5/2) / d⁶, dan akibatnya setidaknya (ε/d)⁷. Pengaruh adalah nilai harapan kuadrat perubahan pada p ketika bit koordinat tersebut dibalik.

Bagaimana Bukti Ini Disusun dan Diperiksa

Pembuktian ini mengikuti rencana Shachar Lovett dan Jiapeng Zhang yang bertumpu pada sertifikat fraksional dan himpunan level, tetapi mengganti sebuah pertidaksamaan yang dalam rencana mereka masih berupa konjektur dengan pertidaksamaan baru yang berlaku untuk semua pasangan. Sebuah determinan menghasilkan pemasangan satu-ke-satu atas konfigurasi masukan. Menurut PSI, pemasangan ini lebih kuat daripada pemasangan dalam Butterfly Lemma David Reimer yang lebih lemah karena juga membatasi seberapa sering konfigurasi yang dipasangkan memiliki nilai sama pada setiap koordinat—batas yang diperlukan untuk pertidaksamaan baru tersebut.

Repositori itu membagi pembuktian elementer menjadi empat bagian: menurunkan pertidaksamaan untuk semua pasangan dari determinan dan bijeksi, mengintegrasikannya atas himpunan level, merata-ratakannya atas koordinat, serta membuktikan batas baris dengan batas sensitivitas titik demi titik. Keempat langkah tersebut menghasilkan batas pengaruh eksplisit.

Menurut audit yang tercatat dalam repositori, pengembangan formal tersebut tidak memuat penanda bukti yang belum diisi ataupun aksioma tambahan. Deklarasinya diputar ulang melalui kernel Lean dan lean4lean, implementasi independen dari pemeriksa tipe Lean. Dalam pengujian terisolasi, pembanding yang menggunakan kernel nanoda dan Lean menerima keempat teorema final; pada mesin kedua, pembanding itu menerima satu solusi kecil yang benar dan menolak empat solusi yang sengaja dibuat keliru.

Pemeriksaan tersebut memiliki batasan yang jelas. Pembaca tetap harus memastikan bahwa pernyataan formalnya sesuai dengan konjektur yang dicetak. Makalah yang ditulis agar dapat dibaca manusia itu sendiri tidak diperiksa oleh mesin, sementara kernel dan kompiler Lean, definisi Mathlib, serta mesin yang digunakan untuk pemeriksaan tetap menjadi bagian dari basis tepercaya.

Peran Manusia dan Tinjauan Pakar

David Turturean, anggota staf teknis PSI, mengembangkan dan menjalankan sistem riset tersebut, menentukan cakupan masalah, meminta model menyusun draf pertama, meninjau draf itu, dan bertanggung jawab atas kebenaran makalah. Repositori tersebut mengungkapkan bahwa model AI menghasilkan pernyataan matematika, draf pertama, dan formalisasi Lean. Jim Halverson mengaudit bukti tersebut, sementara Phiala Shanahan memberikan komentar tentang formalisasinya.

Pengumuman ini menyusul makalah yang diajukan pada 19 Agustus 2026 oleh Guy Blanc, Jordan Docter, Carmen Strassle, dan Li-Yang Tan. Para penulis tersebut telah membuktikan konsekuensi simulasi klasik untuk algoritma kuantum paralel, dengan menunjukkan bahwa algoritma dengan t kueri dan d ronde dapat disimulasikan pada sebagian besar masukan menggunakan t^(O(d²)) kueri klasik. Menurut PSI, keempatnya telah membaca keseluruhan bukti, memberikan komentar, dan sedang menyiapkan pemaparan yang lebih ringkas untuk para pakar.

Dalam penilaian mereka yang diterbitkan oleh PSI, para peneliti menulis: “Ini adalah hasil yang sangat besar. Hasil ini menuntaskan konjektur yang telah berusia puluhan tahun, dengan implikasi penting terhadap hakikat masalah-masalah yang memungkinkan percepatan kuantum. Pembuktian ini bertumpu pada dan mengembangkan beberapa jalur penelitian dalam analisis fungsi Boolean dan kombinatorika probabilistik. Semuanya dirangkai dengan cara yang sungguh ajaib.”

Pengujian langsungnya sangat konkret: kernel independen dapat memutar ulang argumen yang dikodekan, sementara para pakar tetap harus memastikan bahwa pernyataan yang dikodekan sesuai dengan konjektur Aaronson dan Ambainis serta menilai bagian-bagian makalah yang berada di luar Lean. Pembagian ini menentukan apa yang dapat dipastikan melalui pemeriksaan mesin dan apa yang masih memerlukan penelaahan matematis oleh manusia.