Binius STARKs:バイナリ領域における革新的なアプリケーションと性能最適化

2025-08-11 10:00:16

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

1. はじめに

STARKsの効率が低下する主な理由の一つは、実際のプログラムにおいてほとんどの数値が小さいことです。例えば、forループのインデックス、真偽値、カウンターなどです。しかし、Merkleツリーに基づく証明の安全性を確保するために、Reed-Solomon符号化を使用してデータを拡張する際に、多くの追加の冗長値が全体の領域を占めることになります。元の値自体が非常に小さい場合でもです。この問題を解決するために、領域のサイズを小さくすることが重要な戦略となりました。

第1世代STARKsのエンコーディングビット幅は252ビット、第2世代STARKsのエンコーディングビット幅は64ビット、第3世代STARKsのエンコーディングビット幅は32ビットですが、32ビットのエンコーディングビット幅には依然として大量の無駄なスペースが存在します。それに比べて、バイナリフィールドはビットに直接操作を行うことを許可し、エンコーディングはコンパクトで効率的であり、無駄なスペースはありません。つまり、第4世代STARKsです。

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

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

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

バイナリーフィールドに基づいて証明システムを構築する際、2つの実際的な問題があります。STARKsのトレースを表現する際に使用するフィールドのサイズは、多項式の次数よりも大きくする必要があります。STARKsのメルクルツリーのコミットメントを行う際には、リード・ソロモン符号化を行う必要があり、使用するフィールドのサイズは符号化後の拡張サイズよりも大きくする必要があります。

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 + Brakedown PCS + 二進法領域。具体的には、Biniusにはその効率性と安全性を実現するための5つの重要な技術が含まれています。まず、タワー型の二進法領域(towers of binary fields)の算術的構成がその計算の基礎を形成し、二進法領域内での簡略化された計算を実現しています。次に、Biniusはそのインタラクティブなオラクル証明プロトコル(PIOP)において、HyperPlonkの積と置換チェックを改編し、変数とその置換の間の安全で効率的な一致チェックを保証しています。第三に、プロトコルは新しい多項線形シフト証明を導入し、小領域での多項線形関係の検証効率を最適化しています。第四に、Biniusは改良されたLasso探索証明を採用し、探索メカニズムに柔軟性と強力な安全性を提供します。最後に、プロトコルは小領域多項式コミットメントスキーム(Small-Field PCS)を使用し、二進法領域上で効率的な証明システムを実現し、大領域に関連する通常のオーバーヘッドを削減しています。

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

タワー型二項体は、高速かつ検証可能な計算を実現するための鍵であり、主に2つの側面によるものです：効率的な計算と効率的な算術化です。二項体は本質的に非常に効率的な算術操作をサポートしており、パフォーマンスに敏感な暗号アプリケーションにとって理想的な選択肢となります。さらに、二項体の構造は簡略化された算術化プロセスをサポートしており、二項体上で実行される演算はコンパクトで検証しやすい代数形式で表現できます。これらの特性に加えて、タワー構造を通じてその階層的な特性を十分に活用できる能力により、二項体は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フィールド要素として解析することもできます。この表現の柔軟性は、計算オーバーヘッドを必要とせず、ビット文字列の型変換(typecast)に過ぎず、非常に興味深く有用な特性です。また、小さなフィールド要素は、追加の計算オーバーヘッドなしでより大きなフィールド要素にパッケージ化できます。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: 2つの多変数集合が等しいかどうかをチェックします。つまり、{(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とプロトコル設計において多くの類似点があるにもかかわらず、以下の3つの点で改善を行っています:

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

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

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