Editorial ilmu komputer
AI dengan Kewenangan, dari Aplikasi hingga Silikon
Masalah inti
Selama enam puluh tahun, verifikasi mesin diperlakukan sebagai biaya overhead besar — hanya terjangkau untuk artefak istimewa, dan jarang untuk perangkat lunak serta perangkat keras biasa yang benar-benar dikirim industri. Premis karya ini adalah bahwa AI generatif membalik hubungan tersebut. Pada kecepatan AI, verifikasi mesin bukan sekadar ekonomis; verifikasi itu esensial bagi produktivitas. Verifikasi berfungsi sebagai wasit yang tak dapat disuap sehingga satu orang dapat dengan aman mengarahkan kerja mesin otonom dalam skala besar.
Kampanye yang dilaporkan sengaja bersifat ekstrem: dalam lima minggu, satu peneliti dengan langganan AI konsumen mengarahkan armada kecil agen AI dari kode aplikasi, melalui kompilator dan eksekutif terverifikasi, hingga prosesor RISC-V yang taped out pada shuttle silikon komunitas. Tidak ada pembuktian yang melewati tinjauan manusia, dan tidak ada RTL yang ditulis manusia. Disiplin pengorganisasiannya — **metode Salt** — bertumpu pada kernel pembuktian yang tidak dapat dilewati oleh pembuktian hasil halusinasi. Klaim matematis berpindah antaragen sebagai artefak yang diperiksa kernel, dan perhatian manusia disisakan untuk pernyataan, desain, dan p
Inovasi
Kampanye selesai dalam lima minggu. Satu peneliti, yang bekerja dengan langganan AI konsumen, mengarahkan armada kecil agen AI dari kode aplikasi, melalui kompilator dan eksekutif terverifikasi, hingga prosesor RISC-V yang taped out pada shuttle silikon komunitas. Dua hasil negatif sama pentingnya dengan hasil positifnya: tidak ada pembuktian yang melewati tinjauan manusia, dan tidak ada RTL yang ditulis manusia.
Pembukuannya diterbitkan secara penuh. Provenans teorema dicatat untuk setiap artefak. Meter token yang diregistrasi sebelumnya melaporkan biaya komputasi. Waktu manusia dibatasi batas bawah, sehingga kontribusi manusia diukur secara konservatif alih-alih longgar. Penomoran tangkapan ledger galat mencapai #256 — penghitung monoton atas ledger flag append-only kampanye matematika, dipelihara 2026-07-07 hingga 2026-07-20, dengan satu nomor (#79) tidak pernah diberikan dan tangkapan berikutnya dicatat tanpa nomor. Terhadap ledger tangkapan itu, jumlah pembuktian salah yang mencapai catatan adalah nol.
Rantai verifikasi bertahan dari kernel Lean 4 hingga kesetaraan yang diperiksa SAT di batas silikon. Hasilnya bukan demonstrasi bahwa verifikasi itu murah secara abstrak; ini
Mengapa penting
Makna hasil ini terletak pada pembalikan yang dijelaskannya. Selama enam puluh tahun, verifikasi mesin adalah biaya overhead yang hanya terjangkau untuk artefak istimewa. Jika AI generatif membuat verifikasi ekonomis pada kecepatan AI, maka verifikasi berhenti menjadi kemewahan dan menjadi mekanisme produktivitas itu sendiri: wasit yang tak dapat disuap sehingga satu orang dapat dengan aman mengarahkan kerja mesin otonom dalam skala besar. Metode Salt adalah satu disiplin konkret untuk beroperasi di bawah wasit tersebut, dengan kernel pembuktian yang tidak dapat dilewati oleh pembuktian hasil halusinasi.
Batas kepercayaan adalah pilihan arsitektural kuncinya. Dengan mensyaratkan bahwa klaim matematis berpindah antaragen sebagai artefak yang diperiksa kernel, metode ini menyingkirkan pernyataan bahasa alami dari jalur kritis. Perhatian manusia disisakan untuk pernyataan, desain, dan putusan — tempat-tempat di mana pertimbangan tak tergantikan — sementara kernel mengadili sisanya. Penghitung tangkapan monoton ledger galat hingga #256, dengan nol pembuktian salah yang mencapai catatan, adalah bukti bahwa batas tersebut bertahan di bawah tekanan adversarial yang berkelanjutan dari usulan agen itu sendiri.
Hasil ini juga memiliki dimensi silikon. Prosesor RISC-V yang taped out pada shuttle silikon komunitas, tanpa RTL yang ditulis manusia dan dengan kesetaraan yang diperiksa SAT di batasnya, menunjukkan bahwa jalur kompilator-dan-eksekutif terverifikasi dapat dibawa hingga ke perangkat keras fisik. Kandidat taksonomi untuk karya ini — Arsitektur, Keamanan Siber, Jaringan, Kriptografi — mencerminkan tempat di mana kesetaraan yang diperiksa kernel dan ledger provenans append-only paling mungkin menjadi penting berikutnya: di mana pun batas kepercayaan harus dinyatakan tautan demi tautan dan dipertahankan tanpa tinjauan manusia atas setiap pembuktian.
Siapa yang sebaiknya membaca
Membuka konten member…