Binius:バイナリドメインSTARKの革新的な最適化と原理解析

2025-07-08 18:07:24

Binius STARKsの原理とその最適化思考の解析

1 はじめに

STARKsの効率が低下する主な理由は、実際のプログラムにおけるほとんどの数値が小さいにもかかわらず、Merkleツリー証明の安全性を確保するためにReed-Solomon符号化を使用してデータを拡張すると、多くの追加の冗長値が全体の領域を占めることであり、元の値自体が非常に小さい場合でもそうです。この問題を解決するために、領域のサイズを減らすことが重要な戦略となりました。

第1世代STARKsの符号化ビット幅は252ビット、第2世代STARKsの符号化ビット幅は64ビット、第3世代STARKsの符号化ビット幅は32ビットですが、32ビットの符号化ビット幅には依然として大きな無駄なスペースが存在します。それに対して、二進数領域はビットに直接操作でき、符号化がコンパクトで効率的であり、無駄なスペースがありません。つまり、第4世代STARKsです。

Goldilocks、BabyBear、Mersenne31など、近年の新しい研究で発見された有限体と比較して、2進数体の研究は1980年代まで遡ることができます。現在、2進数体は暗号学に広く応用されており、典型的な例には次のものがあります:

F28ドメインに基づくAdvanced Encryption Standard (AES)。
Galoisメッセージ認証コード(GMAC)、F2128フィールドに基づいて；
QRコード、F28ベースのリード・ソロモン符号を使用；
元のFRIとzk-STARKプロトコル、およびSHA-3ファイナリストのGrøstlハッシュ関数は、F28体に基づいており、再帰に非常に適したハッシュアルゴリズムです。

小さな体を使用する場合、拡張体操作は安全性を確保するためにますます重要です。そして、Biniusが使用している二進法体は、その安全性と実用性を保証するために拡張体に完全に依存する必要があります。ほとんどのProver計算に関与する多項式は、拡張体に入る必要はなく、基本体の下で操作するだけで、小さな体で高い効率を実現しています。しかし、ランダムポイントチェックとFRI計算は、必要な安全性を確保するために、より大きな拡張体に深く入る必要があります。

バイナリーフィールドに基づいて証明システムを構築する際に、2つの実際的な問題があります。STARKsでトレース表現を計算する際、使用するフィールドのサイズは多項式の次数より大きくする必要があります。STARKsでMerkleツリーをコミットする際、Reed-Solomonエンコーディングを行う必要があり、使用するフィールドのサイズはエンコーディング拡張後のサイズより大きくする必要があります。

Biniusは、これら二つの問題をそれぞれ処理する革新的なソリューションを提案し、同じデータを二つの異なる方法で表現することによって実現します: まず、単変数多項式の代わりに多変数（具体的には多線形）多項式を使用し、その値を"超立方体"（hypercubes）上で表現して全体の計算軌跡を示します。次に、超立方体の各次元の長さが2であるため、STARKsのように標準的なReed-Solomon拡張を行うことはできませんが、超立方体を正方形（square）として捉え、その正方形に基づいてReed-Solomon拡張を行うことができます。この方法は、安全性を確保しながら、コーディング効率と計算性能を大幅に向上させます。

2 原理分析

現在ほとんどのSNARKsシステムの構築には通常以下の2つの部分が含まれます:

情報理論的多項式インタラクティブオラクル証明（Information-Theoretic Polynomial Interactive Oracle Proof, PIOP）:PIOPは証明システムの核心として、入力された計算関係を検証可能な多項式等式に変換します。異なるPIOPプロトコルは、検証者とのインタラクションを通じて、証明者が段階的に多項式を送信できるようにし、検証者は少数の多項式の評価結果を照会することで計算が正しいかどうかを検証できます。現在のPIOPプロトコルには、PLONK PIOP、Spartan PIOP、およびHyperPlonk PIOPなどがあり、それぞれの多項式表現の処理方法が異なるため、全体のSNARKシステムの性能と効率に影響を与えます。
多項式コミットメントスキーム（Polynomial Commitment Scheme, PCS）：多項式コミットメントスキームは、PIOPが生成した多項式等式が成立するかどうかを証明するために使用されます。PCSは暗号学的ツールであり、証明者は特定の多項式にコミットし、その後にその多項式の評価結果を検証することができますが、多項式の他の情報は隠されます。一般的な多項式コミットメントスキームにはKZG、Bulletproofs、FRI（Fast Reed-Solomon IOPP）、Brakedownなどがあります。異なるPCSは異なる性能、安全性、適用シーンを持っています。

具体的な要件に基づいて、異なるPIOPおよびPCSを選択し、適切な有限体または楕円曲線を組み合わせることで、異なる属性を持つ証明システムを構築できます。例えば:

• Halo2: PLONK PIOP と Bulletproofs PCS の組み合わせで、Pasta 曲線に基づいています。Halo2 の設計では、スケーラビリティに重点を置き、ZCash プロトコルの trusted setup を排除しています。

• Plonky2: PLONK PIOPとFRI PCSを組み合わせ、Goldilocksフィールドに基づいています。Plonky2は効率的な再帰を実現するために設計されています。これらのシステムを設計する際に選択されるPIOPとPCSは、使用される有限体または楕円曲線と一致している必要があり、システムの正確性、性能、安全性を確保します。これらの組み合わせの選択は、SNARKの証明サイズと検証効率に影響を与えるだけでなく、信頼できる設定なしに透明性を実現できるか、再帰的証明や集約証明などの拡張機能をサポートできるかどうかを決定します。

Binius:HyperPlonk PIOP +ブレーキダウンPCS +バイナリドメイン。具体的には、Biniusには、その効率性と安全性を実現するための5つの主要技術が含まれています。まず第一に、バイナリフィールドのタワーに基づく算術がその計算の基礎を形成し、バイナリフィールドでの単純化された演算を実現できます。次に、Biniusは、インタラクティブなOracle Proof Protocol(PIOP)で、HyperPlonk製品と順列チェックを適応させて、変数とその順列との間の安全で効率的な一貫性チェックを確保しました。第 3 に、このプロトコルでは、小さなドメインでのマルチリニア関係の検証効率を最適化するために、新しいマルチリニアシフト引数が導入されています。第 4 に、Binius は Lasso ルックアップ引数の改良版を採用しており、ルックアップメカニズムに柔軟性と強力なセキュリティを提供します。最後に、このプロトコルはスモールフィールド多項式コミットメントスキーム(スモールフィールドPCS)を使用しているため、バイナリドメインに効率的な証明システムを実装し、大規模なドメインに通常関連するオーバーヘッドを削減できます。

2.1 有限体:二値体の塔に基づく算術

タワー型二進数体は、高速かつ検証可能な計算を実現するための鍵であり、主に二つの側面に起因しています：効率的な計算と効率的な算術化。二進数体は本質的に非常に効率的な算術操作をサポートしており、性能に敏感な暗号アプリケーションに理想的な選択肢となっています。さらに、二進数体の構造は簡略化された算術化プロセスをサポートしており、二進数体上で実行される演算はコンパクトで検証しやすい代数形式で表現できます。これらの特性に加え、タワー構造を通じてその階層的な特性を十分に活用できる能力により、二進数体はBiniusのようなスケーラブルな証明システムに特に適しています。

その中で「canonical」とは、バイナリーフィールド内の要素の唯一かつ直接的な表現方法を指します。例えば、最も基本的なバイナリーフィールドF2では、任意のkビットの文字列が直接kビットのバイナリーフィールド要素にマッピングできます。これは素数フィールドとは異なり、素数フィールドは指定されたビット数内でこのような標準的な表現を提供することができません。32ビットの素数フィールドは32ビットを含むことができますが、すべての32ビットの文字列が一意にフィールド要素に対応できるわけではなく、バイナリーフィールドにはこの一対一のマッピングの便利さがあります。素数フィールドFpにおいて、一般的な剰余方法にはBarrett剰余、Montgomery剰余、及びMersenne-31やGoldilocks-64などの特定の有限体に対する特殊な剰余方法が含まれます。バイナリーフィールドF2kにおいて、一般的な剰余方法には特殊剰余（AESで使用されるもの）、Montgomery剰余（POLYVALで使用されるもの）、および再帰的剰余（Towerのようなもの）が含まれます。論文『Exploring the Design Space of Prime Field vs. Binary Field ECC-Hardware Implementations』は、バイナリーフィールドが加算および乗算演算において繰り上がりを導入する必要がなく、バイナリーフィールドの平方演算が非常に効率的であることを指摘しています。なぜなら、それは(X + Y )2 = X2 + Y 2という簡略化されたルールに従っているからです。

図1に示すように、128ビットの文字列：この文字列は、バイナリフィールドの文脈でさまざまな方法で解釈できます。それは128ビットバイナリフィールドのユニークな要素として見なされるか、2つの64ビットタワーフィールド要素、4つの32ビットタワーフィールド要素、16の8ビットタワーフィールド要素、または128のF2フィールド要素として解析される可能性があります。この表現の柔軟性は、計算オーバーヘッドを必要とせず、単なるビット文字列の型キャストであり、非常に興味深く有用な特性です。同時に、小さなフィールド要素は、追加の計算オーバーヘッドなしでより大きなフィールド要素にパッケージ化できます。Biniusプロトコルは、この特性を利用して計算効率を向上させます。さらに、論文「On Efficient Inversion in Tower Fields of Characteristic Two」では、nビットタワー型バイナリフィールド（mビットサブフィールドに分解可能）での乗算、平方、逆演算の計算複雑性について探討しています。

! Bitlayer研究:Binius STARKsの原理分析と最適化思考

2.2 PIOP: バイナリドメイン用の適応 HyperPlonk プロダクトと PermutationCheck ------

BiniusプロトコルのPIOP設計はHyperPlonkを参考にし、一連のコアチェックメカニズムを採用して多項式と多変数集合の正しさを検証しています。これらのコアチェックには:

GateCheck: 検証された秘密証明ωと公開入力xが回路演算関係C(x,ω)=0を満たしていることを確認し、回路が正しく機能することを保証します。
PermutationCheck: 2つの多変数多項式fとgがブール超立方体上での評価結果が置換関係であるかどうかを検証する f(x) = f(π(x))、これは多項式の変数間の配置の一貫性を確保するためです。
LookupCheck: 多項式の評価が与えられたルックアップテーブルに存在するかどうかを検証します。つまり、f(Bµ) ⊆ T(Bµ)、特定の値が指定された範囲内にあることを確認します。
MultisetCheck: 二つの多変量集合が等しいかどうかをチェックします。つまり、{(x1,i,x2,)}i∈H={(y1,i,y2,)}i∈Hであり、複数の集合間の一貫性を保証します。
ProductCheck: 有理多項式がブール超立方体上での評価がある宣言された値∏x∈Hµ f(x) = sに等しいかどうかを検出し、多項式の積の正確性を確保します。
ZeroCheck: ブール超立方体上の任意の点において、多変数多項式がゼロであるかどうかを検証する ∏x∈Hµ f(x) = 0, ∀x ∈ Bµ, 多項式のゼロ点の分布を確保するために。
SumCheck: 多変数多項式の合計が宣言された値∑x∈Hµ f(x) = s であるかどうかを検出します。多変数多項式の評価問題を単変数多項式の評価に変換することで、検証者の計算の複雑さを低減します。また、SumCheckはランダム数を導入することで、複数の合計検証インスタンスのバッチ処理を実現する線形結合を構築することも可能です。
BatchCheck:SumCheckに基づいて、複数の多変量多項式評価の正確性を検証し、プロトコールの効率を向上させます。

BiniusはHyperPlonkとプロトコル設計において多くの類似点がありますが、Biniusは以下の3つの点で改善を行いました:

ProductCheckの最適化: HyperPlonkにおいて、ProductCheckは分母Uが超立方体上で常に非零であることを要求し、かつ積が特定の値に等しい必要があります。Biniusはこの値を1に特化することで、このチェックプロセスを簡素化し、計算の複雑さを軽減しました。
ゼロ除算の問題の処理: HyperPlonkはゼロ除算の状況を十分に処理できず、超立方体上のUが非零であるという主張ができなくなった; Biniusはこの問題を正しく処理し、分母がゼロであってもBiniusのProductCheckは処理を続け、任意の積の値に拡張を許可する。
列間のPermutationCheck: HyperPlonkにはこの機能がありません; Biniusは複数の列間でPermutationCheckをサポートしており、これによりBiniusはより複雑な多項式の排列状況を処理できるようになります。

したがって、Biniusは既存のPIOPSumCheckメカニズムを改善することによって、プロトコルの柔軟性と効率を向上させ、特により複雑な多変数多項式の検証を処理する際に、より強力な機能サポートを提供しました。これらの改善は、HyperPlonkの限界を解決するだけでなく、将来の二進法ドメインに基づく証明システムの基盤を築くものです。

! Bitlayer研究:Binius STARKsの原理分析と最適化思考