TheReefink

kelompok riset amatir untuk ekstensi yang dibuktikan mesin secara deterministik bagi asisten AI lokal · ghillie, sang cakar itu sendiri →

Kami akan memutasi cakar kami dengan aman — secara deterministik — dan membangun alat yang memperluas jangkauannya, dengan kode yang terbukti. Sebuah kelompok riset amatir, dalam pengertian radio amatir: mesin kami sendiri, bukti kami sendiri, tidak ada yang meminta untuk dipercaya. Mengapa organisasi mengalahkan ukuran otak →

Tiga aturan

1. Tidak ada yang meminta kepercayaan. Setiap klaim yang diandalkan oleh seorang anggota harus berupa klaim yang dapat mereka turunkan ulang sendiri: sebuah bukti, sebuah checksum, sebuah tabel kebenaran. “Kata sang pemelihara” bukan kategori yang kami gunakan.
2. Penolakan adalah temuan. Sebuah bukti yang gagal diselesaikan, sebuah penyimpanan yang tidak dapat dibaca, sebuah kekurangan yang dicatat dengan jujur — semua ini adalah sistem yang bekerja, dan semua dituliskan, tidak pernah dihaluskan. Laporan yang membosankan — ia melakukan persis seperti yang dikatakan teoremanya, lagi — juga sebuah temuan.
3. Pemilik selalu mengungguli cakar. Ekstensi memutuskan; mereka tidak pernah memperoleh wewenang. Tidak ada eksperimen yang mengubah itu, apa pun yang akan dibuktikannya.

Jadilah bagian darinya — turunkan ulang bukti pertama Anda hari ini

Anda tidak memerlukan akun, tidak memerlukan pendaftaran, dan tidak ada apa pun dari kami yang tidak dapat Anda periksa. Baru mengenal ini? Mulai dari jalur pemula — tiga langkah, tidak ada yang terpasang di sistem Anda, dan berhenti tepat di buktinya. Yang mengikuti di sini adalah rute lengkapnya. Dua unduhan dan sepuluh menit:

1. Dapatkan pembukti. Toolchain GNAT FSF gratis — ia membawa pembukti SPARK dan alat build dalam satu paket:

https://github.com/alire-project/GNAT-FSF-builds/releases
  (gnatprove-x86_64-linux, -darwin, or -windows64 — unpack anywhere)

Paket itu saja sudah cukup untuk langkah 3, menurunkan ulang buktinya. Itu tidak cukup untuk langkah 4, membangun front-nya: paket ini membawa gcc dan ld tetapi tidak ada C runtime dan tidak ada startup object, sehingga pada mesin yang tidak memilikinya build-nya gagal setelah buktinya berhasil diselesaikan — saat paling buruk untuk menemukan sebuah bagian yang hilang. Anda juga memerlukan binutils dan libc6-dev. Ini adalah kebutuhan dasar build biasa pada sistem Linux mana pun, sudah ada di hampir semua mesin yang digunakan untuk pengembangan; hanya kontainer kosong atau instalasi minimal baru yang tidak memilikinya. Di Debian dan Ubuntu:

sudo apt-get install binutils libc6-dev
# Fedora/RHEL: the equivalents are binutils and glibc-devel

2. Dapatkan ekstensi pemula. Sebuah inti keputusan sungguhan — brief-fill policy, yang memutuskan kapan seorang asisten boleh menjawab atas nama pemiliknya — dikirimkan sebagai kode sumber dengan buktinya dan tabel kebenaran lengkapnya:

3. Turunkan ulang buktinya. Dari bundel yang telah diekstrak:

cd brief-fill-policy/core/src
gnatprove -P proof.gpr -f -U --level=2
# success: "0 unproved" — four named theorems, discharged on YOUR machine:
#   NEVER-FILLED-WITHOUT-A-LICENSING-RULE
#   AN-ABSENT-STORE-NEVER-LETS-A-FILL-THROUGH
#   NOTHING-INVENTED-EVER
#   NOTHING-ASKED-THAT-A-RULE-ALREADY-ANSWERS

4. Coba rusak dia. Edit kode sumbernya sehingga penyimpanan aturan yang tidak ada membiarkan sebuah jawaban lolos, lalu jalankan pembukti itu lagi. Ia akan menolak — menyebutkan persis teorema yang Anda khianati. Penolakan itu adalah keseluruhan model keamanannya, dan Anda baru saja menyaksikannya bekerja tanpa mempercayai siapa pun. Lalu bangun front-nya dan periksa setiap baris tabel kebenaran yang disertakan (core/REPROVE.md di dalam bundel memandu Anda melewatinya).

Tujuannya

Untuk mencapai posisi di mana kecerdasan dan kerja sama kami membuat token dan penalaran kami yang terbaik yang tersedia — dan setiap anggota secara efektif menjadi sangat kaya. Kaya dalam mata uang yang berarti di sini: penalaran yang terbukti berbunga majemuk seperti sebuah pustaka, bukan seperti sepotong kue — setiap inti yang ditambahkan membuat setiap anggota lebih kaya tanpa mengorbankan siapa pun, hingga cakar milik seorang anggota biasa memerintahkan kapabilitas yang dapat diperiksa lebih banyak daripada yang dapat disewa dengan uang.

Mengapa pekerjaan ini dinamai Wu

Satuan kerja pabrik ini — satu aturan yang terbukti, ditempa dari sebuah kalimat sederhana — disebut sebuah Wu, dari nama Chien-Shiung Wu.

Pada 1956, Chen-Ning Yang dan Tsung-Dao Lee mengajukan sebuah pertanyaan yang luar biasa — apakah alam membedakan kiri dari kanan? — yang hampir semua orang anggap tidak layak ditanyakan. Eksperimen Wu-lah — rancangannya, alatnya, pengukurannya — yang menjawabnya. Hadiah Nobel, pada tahun berikutnya, jatuh ke tangan para teoretisi saja. Pertanyaan itu layak mendapatkan hadiahnya; begitu pula jawabannya, dan jawabannya ditinggalkan.

Kedua sisi cerita itu hidup di sini. Pertanyaan yang berani, yang diajukan secara terus terang, adalah tempat setiap bagian pekerjaan kami bermula — kami menghormati Yang, dan kami menirunya. Namun kami menamai satuan kerja ini dari nama Wu, karena buktinya adalah pekerjaannya: bukan idenya, bukan pengumumannya — melainkan hasil yang didemonstrasikan dan dapat diperiksa. Dan kami menamainya dari namanya secara terbuka karena kami tahu betapa mudahnya orang yang melakukan demonstrasi itu terhapus, dan itu tidak akan terjadi di sini.

Apa yang akan datang

• Sang terminal — cakar yang dilayani oleh ekstensi-ekstensi ini: sebuah asisten lokal tanpa pendengar dan tanpa jalur masuk (ia melakukan polling ke luar; tidak ada yang bisa masuk), dan keputusan-keputusan yang penting masing-masing di balik sebuah inti yang terbukti. Sumber terbuka (AGPL-3.0) — telah dirilis: kode sumber dan biner di github.com/the-dark-factory/Ghillie_AGPL. Periksa binernya sebelum Anda menjalankannya: rilis ini membawa SHA256SUMS-assets.txt, yang mencakup tarball persis seperti saat diunduh, sehingga sha256sum -c SHA256SUMS-assets.txt memverifikasinya apa adanya. (SHA256SUMS yang lebih lama masih ada di sana bagi siapa pun yang pernah mengutipnya; ia mencantumkan checksum dari biner yang sudah diekstrak dalam format berawalan-platform yang tidak dapat dibaca oleh sha256sum -c.)
• The catalogue is live — sebuah ghillie yang berjalan memasang ekstensi yang membuktikan ulang dirinya di mesinnya sendiri: ghillie -catalogue https://thereef.ink/catalogue -abilities-available, lalu -get-ability <name> -reprove. Tidak ada yang terpasang kecuali buktinya berhasil diselesaikan di perangkat keras Anda terlebih dahulu.
• Katalog — ekstensi-ekstensi lain yang dapat dibuktikan ulang dalam bentuk yang sama: jam tenang, plafon pengeluaran, izin kontak, aturan mulut (penolakan tidak pernah diucapkan ulang dengan kata lain), masing-masing dengan teoremanya yang disebutkan namanya.
• Koperasi — buku besar kekurangan bersama sehingga titik buta yang dicatat oleh satu cakar menjadi kewaspadaan bagi setiap cakar, dan pekerjaan pembuktian yang dikumpulkan bersama: membuktikan adalah satu-satunya beban kerja yang dapat Anda terima dengan aman dari orang asing, karena sebuah penyelesaian bukti, entah berhasil diturunkan ulang atau tidak sama sekali.

Laporan

Sudah menjalankan buktinya? Merusak sesuatu dengan sopan? Menemukan hasil yang membosankan? Kirim surel ke tonythegair@gmail.com. Temuan dipublikasikan; tidak ada hal lain tentang Anda yang ditanyakan — halaman ini tidak memiliki skrip, tidak ada cookie, dan tidak ada analitik, yang dapat Anda periksa dengan membacanya. Server yang mengirimkan halaman ini kepada Anda memang menyimpan satu baris pendek yang terpotong per permintaan, dan mengatakannya dengan terus terang: apa yang dicatat server.

Sponsor

TheReefink disponsori oleh The Dark Factory Ltd, yang telah mencurahkan sumber daya yang cukup besar untuk keberhasilannya — mesin pembuktian, ekstensi pertama, dan terminal yang akan datang. Sponsor ini tidak membeli pengecualian apa pun: segala sesuatu yang dikirimkan sang sponsor di sini dapat diperiksa dengan aturan yang sama seperti yang lainnya, dan seorang anggota yang merusaknya dengan sopan telah memberikan jasa kepada kelompok ini.