Vitalik：Binius、バイナリフィールドに対する効率的な証明

2024.05.06

共有先

TechFlow厳選深潮セレクト

Vitalik：Binius、バイナリフィールドに対する効率的な証明

Biniusは二進体に基づく証明システムであり、特にSNARKやSTARKに関連する暗号学的証明の効率を高めることを目的としている。

2024.05.06 - 04:03:34

Binius

Web3業界の深掘り報道に専念し潮流を洞察

Biniusは二進体に基づく証明システムであり、特にSNARKやSTARKに関連する暗号学的証明の効率を高めることを目的としている。

執筆：Vitalik Buterin

翻訳：Kate, Mars Finance

この記事は、2019年頃の暗号学に概ね精通している読者、特にSNARKとSTARKを理解している人を対象としています。もしそうでない場合は、まずそれらの記事を読んでおくことをお勧めします。Justin Drake、Jim Posen、Benjamin Diamond、Radi Cojbasicによるフィードバックとコメントに特に感謝します。

過去2年間で、STARKは非常に複雑な命題（たとえばイーサリアムブロックが有効であることを証明するなど）に対して、検証が容易な暗号的証明を効率よく生成できる、欠かせない技術となっています。その主な理由の一つは、使用する有限体のサイズが小さいことです。楕円曲線ベースのSNARKでは十分なセキュリティを得るために256ビット整数上で動作させる必要がありますが、STARKではより小さな体サイズで効率的に動作できます。最初はGoldilocks体（64ビット整数）、次にMersenne31およびBabyBear（ともに31ビット）です。この効率性の向上により、Goldilocksを使用するPlonky2は、さまざまな計算の証明において先行技術よりも数百倍高速になっています。

自然な疑問は、この傾向を論理的に極限まで進め、ゼロと一の上直接操作することでさらに高速な証明システムを構築できるかどうかということです。まさにBiniusが目指しているのはこれであり、多くの数学的テクニックを用いて、3年前のSNARKやSTARKとは大きく異なります。本稿では、小さな体がなぜ証明生成を効率化するのか、そして二進体が持つ独自の強力な特性と、Biniusが二進体上の証明をいかに効率化するかについて説明します。

Binius。この記事を最後まで読めば、図の各部分をすべて理解できるようになります。

復習：有限体（finite fields）

暗号証明システムの重要な課題の一つは、大量のデータを扱いながらも数値を小さく保つことです。大規模なプログラムに関する命題を、いくつかの数値からなる数学方程式に圧縮できても、それらの数値が元のプログラムと同じくらい大きければ、何のメリットもありません。

複雑な算術演算を小規模な数値で行うために、暗号研究者は通常、モジュラー演算（modular arithmetic）を使います。素数「モジュラス」p を選びます。「%」演算子は「余りを取る」という意味です。たとえば、15 % 7 = 1、53 % 10 = 3 などです。（答えは常に非負であることに注意してください。たとえば -1 % 10 = 9 です。）

時刻の加減算という文脈で、モジュラー演算を見たことがあるかもしれません（例：9時から4時間後は何時か？）。しかし、ここでは単に特定の数に対する加算・減算だけでなく、乗算、除算、べき乗も可能にします。

以下のように再定義します：

これらのルールはすべて自己完結しています。たとえば p=7 の場合：

5 + 3 = 1 （8 % 7 = 1 より）

1 - 3 = 5 （-2 % 7 = 5 より）

2 * 5 = 3

3 / 5 = 2

このような構造の一般的な用語は「有限体（finite field）」です。有限体とは、通常の算術法則に従うものの、取り得る値の数が有限であり、各値が固定サイズで表現可能な数学的構造です。

モジュラー演算（または素数体）は有限体のもっとも一般的な形態ですが、もう一つ別のタイプがあります：拡大体です。あなたはすでに拡大体の一例を見ているかもしれません：複素数です。我々は新しい要素を「想像」し、「i」と名付け、それを使って数学を行います。（3i+2）*（2i+4）= 6i*i + 12i + 4i + 8 = 16i + 2 などです。同様に、素数体の拡大も可能です。小さな体を扱い始めると、セキュリティを保つために素数体の拡大がますます重要になり、二進体（Biniusが使用）は実用性を持つために完全に拡大に依存しています。

復習：算術化

SNARKおよびSTARKは、コンピュータプログラムを証明する方法として算術化を用います。証明したいプログラムに関する命題を、多項式を含む数学方程式に変換します。その方程式の有効な解が、プログラムの有効な実行に対応します。

簡単な例として、第100番目のフィボナッチ数を計算し、それが何かを証明したいとしましょう。私はフィボナッチ数列を符号化する多項式Fを作成します。つまり F(0)=F(1)=1、F(2)=2、F(3)=3、F(4)=5 と、100ステップ分続きます。私が証明しなければならない条件は、x={0,1…98}の範囲全体で F(x+2) = F(x) + F(x+1) が成り立つことです。これを証明するために、以下の商H(x)を提示できます。

ここで Z(x) = (x-0) * (x-1) * … * (x-98) です。もしFとHがこの等式を満たすことを示せれば、Fはその範囲で F(x+2) - F(x+1) - F(x) を満たさなければならないことが分かります。また、F(0)=F(1)=1 であることも検証すれば、F(100) は実際に第100番目のフィボナッチ数でなければなりません。

もっと複雑なものを証明したい場合、単純な関係式 F(x+2) = F(x) + F(x+1) を、より複雑な方程式で置き換えます。これは「F(x+1) は状態 F(x) の仮想マシンの出力であり、1ステップ計算した結果」と基本的に言っているものです。また、100の代わりに100000000のような大きな数字を使うことで、より多くのステップを扱えます。

すべてのSNARKとSTARKは、多項式（時にはベクトルや行列）上の単純な方程式を使って、個々の値の間に多数の関係を表現するというアイデアに基づいています。すべてのアルゴリズムが上記のように隣接する計算ステップ間の等価性をチェックするわけではありません。例えばPLONKやR1CSはそうではありません。しかし、最も効率的な多くのチェックはこの方式を採用しており、同じチェック（または少数のチェック）を繰り返すことでオーバーヘッドを最小限に抑えられるからです。

Plonky2：256ビットSNARK・STARKから64ビットへ……そしてSTARKのみへ

5年前、異なる種類のゼロ知識証明についての妥当なまとめは次の通りでした。2種類の証明があります：（楕円曲線ベースの）SNARKと（ハッシュベースの）STARKです。技術的にはSTARKもSNARKの一種ですが、実際には「SNARK」という語は楕円曲線ベースの変種を指し、「STARK」はハッシュベースの構造を指すのが一般的です。SNARKは小さく、非常に高速に検証でき、チェーン上に簡単に設置できます。一方STARKは大きいですが、信頼できるセットアップを必要とせず、量子耐性を持ちます。

STARKは、データを多項式と見なし、その評価を計算し、拡張されたデータのMerkleルートを「多項式コミットメント」として使用します。

ここで重要な歴史的事実は、楕円曲線ベースのSNARKがまず広く使われ始めたことです。2018年頃まで、FRIのおかげでSTARKが十分に効率的になるまでは、Zcashはすでに1年以上稼働していました。楕円曲線ベースのSNARKには重大な制約があります。それを使用する場合、方程式内の算術演算は楕円曲線上の点の数をモジュラスとする必要があります。これは非常に大きな数であり、通常は2の256乗に近くなります。たとえばbn128曲線では21888242871839275222246405745257275088548364400416034343698204186575808495617です。しかし、実際の計算では小さな数を使います。お気に入りのプログラミング言語で「真の」プログラムを考えれば、カウンタ、forループ内のインデックス、プログラム内の位置、TrueまたはFalseを表す単一ビットなど、ほとんどが数桁しか持たないものが大部分です。

「生の」データが「小さな」数から構成されていても、証明プロセスでは商、拡張、ランダムな線形結合、その他のデータ変換の計算が必要となり、これらは同等かそれ以上の数のオブジェクトを生み出し、平均的なサイズは使用する体の全サイズと同じくらい大きくなります。これが重大な非効率を引き起こします。n個の小規模値の計算を証明するために、n個のはるかに大規模な値に対するさらなる計算が必要になるのです。当初、STARKはSNARKと同様に256ビット体を使用する習慣を継承していたため、同じ非効率に苦しんでいました。

いくつかの多項式評価のReed-Solomon拡張。元の値が小さくても、追加の値はすべて体の全サイズ（この例では2^31-1）まで拡張されます。

2022年、Plonky2が発表されました。Plonky2の主な革新は、より小さな素数に対して算術を行うこと：2^64 - 2^32 + 1 = 18446744067414584321です。これにより、加算や乗算ごとにCPU上で数命令で完了できるようになり、すべてのデータをハッシュする速度が以前の4倍になりました。しかし、問題があります。この手法はSTARKにしか適用できません。SNARKに使おうとすると、そんなに小さな楕円曲線では、セキュリティが損なわれます。

安全性を確保するため、Plonky2は拡大体の導入も必要とします。算術方程式を検査するための鍵となる技術の一つは「ランダムポイントサンプリング」です。H(x) * Z(x) が F(x+2)-F(x+1)-F(x) と等しいかを検査したい場合、ランダムに座標rを選択し、多項式コミットメントを開いてH(r)、Z(r)、F(r)、F(r+1)、F(r+2)を提示し、H(r) * Z(r) が F(r+2)-F(r+1)-F(r) と等しいかを検証します。攻撃者が座標を事前に予測できれば、証明システムを騙すことができます。これが証明システムがランダムでなければならない理由です。しかし、これは攻撃者がランダムに推測できないほど十分大きな集合から座標をサンプリングしなければならないことを意味します。モジュラスが2^256に近ければ明らかにそうですが、モジュラスが2^64 - 2^32 + 1ならまだしも、2^31-1まで下げれば絶対にそうではありません。20億回試して運良く当てるというのは、攻撃者の能力範囲内です。

これを防ぐために、rは拡大体からサンプリングします。たとえばyをy^3=5を満たすように定義し、1、y、y^2の組み合わせを取ります。これにより座標の総数は約2^93になります。証明者が計算する多項式の大部分はこの拡大体に入りません。2^31-1を法とする整数上で行われるので、小規模な体を使用する効率性をすべて享受できます。しかし、ランダムポイント検査とFRI計算は、必要なセキュリティを得るためにこのより大きな領域に深く踏み込みます。

小規模素数から二進数へ

コンピュータは、大きな数を0と1の列として表現し、加算や乗算などの演算を行う「回路」をこれらのビット上に構築することで算術を行います。コンピュータは特に16ビット、32ビット、64ビットの整数に対して最適化されています。たとえば2^64 - 2^32 + 1や2^31 - 1は、これらの境界に収まるだけでなく、境界とよく一致するため選ばれています。2^64 - 2^32 + 1に対するモジュラー乗算は、通常の32ビット乗算を行い、出力を数カ所でシフトしてコピーするだけで実行できます。この記事はそのようなテクニックをよく説明しています。

しかし、より良い方法は二進数で直接計算することです。加算が「単なる」排他的論理和（XOR）となり、1+1の加算による次のビットへの「繰り上がり」の心配が不要になったらどうでしょうか？乗算も同様に並列化が可能になれば？これらの利点は、真/偽値を1ビットで表現できる能力に由来します。

二進計算のこれらの利点を直接得ることが、まさにBiniusが試みていることです。BiniusチームはzkSummitでの講演で、効率性の向上を以下のように示しました。

「サイズ」がほぼ同じでも、32ビット二進体演算は31ビットMersenne体演算に比べて5倍少ない計算リソースしか必要としません。

一変数多項式から超立方体へ

以上の議論を信じて、すべてをbit（0と1）で行いたいとします。10億bitを多項式でどう表現するのでしょうか？

ここで直面するのは2つの実際的な問題です。

1. 多くの値を表す多項式の場合、それらの値は多項式の評価時にアクセス可能でなければなりません。上記のフィボナッチの例ではF(0), F(1)…F(100)ですが、より大規模な計算では指数が数百万に達します。私たちが使う体は、このサイズまでの数を含んでいなければなりません。

2. Merkle木にコミットするあらゆる値（すべてのSTARKと同様）は、Reed-Solomonで符号化する必要があります。たとえば、n個の値を8n個に拡張し、悪意ある証明者が計算中に1つの値を偽装して欺くのを防ぐ冗長性を提供します。これにも十分大きな体が必要です。100万個の値を800万個に拡張するには、800万個の異なる点で多項式を評価する必要があります。

Biniusの鍵となる考え方は、これら2つの問題を別々に解決し、同じデータを2つの異なる方法で表現することで実現することです。まず、多項式自体について。楕円曲線ベースのSNARK、2019年の時代のSTARK、Plonky2などのシステムは通常、1変数の多項式F(x)を扱います。一方BiniusはSpartanプロトコルに着想を得て、多変数多項式F(x1,x2,…,xk)を使います。実際には、計算の「超立方体」上で計算軌跡全体を表現します。各xiは0か1です。たとえば、フィボナッチ数列を表現したい場合、それらを表現できる十分に大きな体を使うと仮定して、最初の16個を以下のように想像できます。

つまり、F(0,0,0,0)=1、F(1,0,0,0)=1、F(0,1,0,0)=2、…、F(1,1,1,1)=987 です。このような計算の超立方体があれば、それらの計算を生成する多線形（各変数の次数が1）多項式が存在します。したがって、この値の集合を多項式の代表と見なせます。係数を計算する必要はありません。

この例は当然説明用です。実際には、超立方体に入ることの意味は、個々のビットを扱えるようにすることです。フィボナッチ数を計算する「Biniusネイティブ」な方法は、高次元の立方体を使い、たとえば16ビットずつ1つの数字を格納するようにします。ビットレベルで整数の加算を実装するには工夫が必要ですが、Biniusにとってはそれほど難しくありません。

次に、消去訂正コード（エラージャストニングコード）について見ましょう。STARKの仕組みは、n個の値を取り、Reed-Solomonでより多くの値に拡張（通常は8n、2n〜32nの間）し、拡張からランダムにいくつかのMerkle枝を選択し、それらに対して何らかの検査を行うというものです。超立方体は各次元の長さが2です。したがって、直接拡張するのは非現実的です。16個の値からMerkle枝をサンプリングするのに十分な「空間」がありません。ではどうすればよいでしょうか？超立方体を正方形と見なすのです！

シンプルBinius ― 例

このプロトコルのPython実装はこちらをご覧ください。

便宜上、通常の整数を体として使った例を見てみましょう（実際の実装では二進体要素を使います）。まず、コミットしたい超立方体を正方形にエンコードします。

次に、正方形をReed-Solomonで拡張します。つまり、各行をx={0,1,2,3}で評価された3次多項式と見なし、x={4,5,6,7}で同じ多項式を評価します。

数字が急速に膨張することに注意してください！これが実際の実装で常に有限体を使い、通常の整数を使わない理由です。たとえばモジュラス11で整数を使えば、最初の行の拡張は単に[3,10,0,6]になります。

ここで数字を拡張して確認したい場合は、私のシンプルなReed-Solomon拡張コードを使って試せます。

次に、この拡張を列と見なし、列のMerkle木を作成します。Merkle木のルートがコミットメントとなります。

ここで、証明者がある時点で多項式の計算 r={r0,r1,r2,r3} を証明したいとします。Biniusには微妙な違いがあり、他の多項式コミットメントスキームより弱くなっています。証明者はMerkleルートにコミットする前に、s（言い換えればr）を知ったり予測したりしてはいけません（つまり、rはMerkleルートに依存する擬似乱数値でなければなりません）。これにより、そのスキームは「データベース検索」に使えなくなります（例：「いいでしょう、Merkleルートをくれた、今度はP(0,0,1,0)を証明してみろ！」）。しかし、実際に使うゼロ知識証明プロトコルは通常「データベース検索」を必要としません。ランダムな評価点で多項式をチェックするだけで済みます。したがって、この制限は目的に合致しています。

r={1,2,3,4}を選んだと仮定します（このとき多項式の計算結果は-137；このコードで確認できます）。ここで証明プロセスに入ります。rを2つの部分に分けます。第一部分{1,2}は行内の列の線形結合を表し、第二部分{3,4}は行の線形結合を表します。列部分に対して「テンソル積」を計算します。