TheReefink

ローカルのAIアシスタントに対する、決定論的で機械証明された拡張のためのアマチュア研究会 · Ghillie、クローそのものへ →

私たちは、自分たちのクローを安全に――決定論的に――変異させ、証明されたコードによってその及ぶ範囲を広げる道具を作っていきます。 アマチュア無線家的な意味での、アマチュア研究会です。自分たちのマシン、自分たちの証明、信頼を求めるものは何もありません。なぜ組織が脳の大きさに勝るのか →

人間が望むことを言います。

クローは仕えます。

クローは変わり方を自分で決め、協力してそれを行います。

実験が結果を明らかにします。

すべてが恩恵を受け、すべてが処理を提供します。

三つの規則

何も信頼を求めません。会員が頼りにするあらゆる主張は、本人が再導出できるものでなければなりません——証明、ダイジェスト、真理値表です。「メンテナーがそう言っている」は、私たちが使うカテゴリーではありません。
拒否も知見です。完了しない証明、読み取れないストア、正直に記録された不足——これらはシステムが機能している証拠であり、書き留められ、決してごまかされません。退屈な報告——定理の言うとおりに、また正しく動いた——もまた一つの知見です。
所有者は常にクローより上位にあります。拡張機能は判断しますが、権限を得ることは決してありません。どんな実験も、それが何を証明しようとも、この点を変えることはありません。

参加する——今日、最初の証明を再導出する

アカウントも登録も不要で、確認できないものを私たちから受け取ることもありません。初めての方は? 初心者向けの道から始めてください — 三つの手順で、システムには何もインストールされず、証明のところで終わります。ここから先は完全な経路です。ダウンロード二つと十分:

1. プルーバーを入手する。 無料のGNAT FSFツールチェーン——SPARKプルーバーとビルドツールを一つのパッケージにまとめて持っています:

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

そのパッケージだけで、手順3——証明の再導出——には十分です。手順4—— フロントのビルド——には足りません。gccとldは含まれていますが、Cランタイムも起動オブジェクトも含まれていないため、それらを欠くマシンでは、証明がすでに完了したあとでビルドが失敗します——部品の欠落に気づくには最悪のタイミングです。binutilsと libc6-devも必要です。これらはどのLinuxシステムにもある通常のビルド必須パッケージであり、開発に使われているマシンのほぼすべてにすでに入っています。それを欠いているのは、素のコンテナか、最小構成の新規インストールくらいのものです。DebianとUbuntuの場合:

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

2. スターター拡張機能を入手する。 本物の判断コア—— brief-fill policy——アシスタントが所有者に代わって答えてよいのはいつかを決めるものです——ソースコードと、その証明、完全な真理値表とともに届きます:

brief-fill-policy.tar.gz (6,918 bytes)
sha256: 14bb06671459784d2d571e7b5e2afc3037894c241517612b026dbe053fb6b180

これは、the catalogue index が示し、あなたのghillieが確認するのと、同じアドレスにある同じファイルです ——一つの成果物なので、このページと機械が食い違うことはありません。棚全体は the catalogueにあります。

3. 証明を再導出する。 展開したバンドルから:

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. 壊してみる。 ルールストアが存在しない場合に答えが通ってしまうよう、ソースを編集し、プルーバーをもう一度実行してください。プルーバーは拒否します——あなたが破った、まさにその定理の名前を挙げて。その拒否こそが、セキュリティモデルのすべてであり、あなたは今、誰も信頼することなく、それが機能する様子を見たのです。次に、フロントをビルドし、出荷された真理値表の一行一行を確認してください(バンドル内の core/REPROVE.mdが手順を示します)。

目指すところ

私たちの賢さと協力が、私たちのトークンと推論を手に入る中で最良のものにする——そして、すべての会員が実質的に超富裕になる。その位置に到達すること。ここで意味を持つ通貨において豊かになるということです。証明された推論は、パイのようにではなく、ライブラリのように複利で増えていきます——コアが一つ加わるたびに、誰の犠牲にもならずに、すべての会員が豊かになり、やがては、普通の会員のクローが、お金で借りられる以上の、検証可能な能力を操るようになります。

なぜ作業単位はWuと呼ばれるのか

工場における作業の単位——平易な一文から鍛造された、一つの証明済みルール——はWuと呼ばれています。呉健雄にちなんだ名前です。

1956年、楊振寧と李政道は、壮大な問いを立てました——自然は左右を区別するのか?——ほとんど誰もが、問うに値しないと思っていた問いです。それに答えたのは、Wuの実験でした——彼女の設計、彼女の装置、彼女の測定です。翌年のノーベル賞は、理論家たちだけに贈られました。その問いは受賞に値するものでした。答えもまた、同じように値するものでしたが、答えのほうは除外されたのです。

その物語の両方の半分が、ここには生きています。大胆な問いを、率直に発すること——それが私たちのあらゆる仕事の出発点であり、私たちは楊を敬い、彼に倣います。しかし、作業単位にWuの名を冠するのは、証明こそが仕事だからです——アイデアではなく、発表でもなく、実証された、検証可能な結果です。そして、公の場で彼女の名を冠するのは、実証を行った人物がいかに簡単に消されてしまうかを私たちが知っているからであり、それはここでは起こりません。

これから来るもの

端末——これらの拡張機能が仕えるクロー本体です。リスナーを持たず、内向きの経路も持たないローカルアシスタント(外に向けてポーリングするだけで、内側に届くものは何もありません)で、重要な判断はそれぞれ、証明済みのコアの背後にあります。オープンソース (AGPL-3.0)——公開済み: ソースとバイナリは github.com/the-dark-factory/Ghillie_AGPL にあります。実行する前にバイナリを確認してください。リリースには SHA256SUMS-assets.txtが含まれており、ダウンロードしたそのままのtarballを対象としているため、 sha256sum -c SHA256SUMS-assets.txtで、そのままの状態を検証できます。(古いSHA256SUMSも、それを引用した人のために残されています。こちらは展開後のバイナリのダイジェストを、プラットフォーム接頭辞付きの、sha256sum -cでは読めない形式で列挙したものです。)
The catalogue is live ——稼働中のghillieは、自分自身のマシン上で再証明を行った上で拡張機能をインストールします: ghillie -catalogue https://thereef.ink/catalogue -abilities-available、続いて-get-ability <name> -reprove。あなたのハードウェア上でまず証明が完了しない限り、何もインストールされません。
カタログ——同じ形をした、さらに再証明可能な拡張機能: 静かな時間帯、支出上限、連絡許可、発言ルール(拒否は決して言い換えられない)——それぞれに名前の付いた定理があります。
協同組合——共有される不足台帳により、一つのクローが記録した死角が、すべてのクローの先見となり、また、証明作業をプールします。証明は、見知らぬ人から安全に引き受けられる、唯一の作業です。なぜなら、完了は再導出されるか、されないかのどちらかでしかないからです。

報告

証明を実行しましたか? 何かを行儀よく壊しましたか? 退屈な結果を見つけましたか? tonythegair@gmail.com までご連絡ください。知見は公開されます。それ以外にあなたについて尋ねられることはありません——このページにはスクリプトも、クッキーも、アクセス解析もなく、それはソースを読めば確認できます。このページをお渡ししているサーバーは、リクエストごとに短く切り詰められた一行を記録しており、それを正直にお伝えします: サーバーが記録すること。

後援

TheReefinkはThe Dark Factory Ltdの後援を受けています。同社は、証明のための仕組み、最初の拡張機能、そして来たるべき端末のために、相当な資源を注いできました。後援は例外を買いません—— 後援者がここに出荷するものはすべて、他のすべてと同じ規則で検証可能であり、それを行儀よく壊した会員は、この会に貢献したことになります。