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

1 はじめに

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

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

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

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

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

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

2 原理分析

現在のほとんどのSNARKsシステムの構築は通常、以下の2つの部分を含みます：

• 情報理論多項式対話型オラクル証明(PIOP) *多項式コミットメントスキーム(PCS)

Binius:HyperPlonk PIOP +ブレーキダウンPCS +バイナリドメイン。 具体的には、Biniusには、その効率性と安全性を実現するための5つの主要なテクノロジーが含まれています。

1. タワー型二進法ドメインに基づく算術化
2. 適応HyperPlonk製品と順列チェック
3. 新しい多線形シフト証明 4.なげなわルックアップ引数の改善
4. 小域多項式コミットメントスキーム

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

タワー型バイナリーフィールドは、高速かつ検証可能な計算を実現するための鍵であり、主に2つの側面に起因しています：効率的な計算と効率的な算術化です。バイナリーフィールドは本質的に非常に効率的な算術操作をサポートしており、性能要件に敏感な暗号学アプリケーションにとって理想的な選択肢となります。さらに、バイナリーフィールドの構造は簡略化された算術化プロセスをサポートしており、すなわちバイナリーフィールド上で実行される演算は、コンパクトで検証しやすい代数形式で表現できます。

素数領域 Fp では、一般的な縮約法には、バレット縮約法、モンゴメリー還元、およびメルセンヌ-31 や Goldilocks-64 などの特定の有限体に対する特別な簡約法が含まれます。 バイナリドメイン F2k では、一般的に使用される縮約法には、特殊縮約法 (AES など)、モンゴメリー縮約法 (POLYVAL など)、再帰的縮約法 (Tower など) が含まれます。

二進制体では加算および乗算において繰り上がりを導入する必要がなく、また二進制体の平方演算は非常に効率的であり、(X + Y )2 = X2 + Y 2 の簡略化ルールに従います。

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

2.2 PIOP:適応されたHyperPlonk製品と順列チェック

BiniusプロトコルのPIOP設計はHyperPlonkを参考にしており、多項式および多変数集合の正確性を検証するための一連のコアチェックメカニズムを採用しています。これらのコアチェックには次のものが含まれます：

1. ゲートチェック 2.順列チェック
   3.ルックアップチェック
2. マルチセットチェック
3. プロダクトチェック 6.ゼロチェック 7.サムチェック
4. バッチチェック

Binius は HyperPlonk と比較して、以下の点が改善されています。

• ProductCheckの最適化
• ゼロ除算の問題の処理
• Permutation列間のチェック

2.3 PIOP: 新しいマルチリニア シフト引数

Biniusプロトコルでは、仮想多項式の構築と処理が重要な技術の一つであり、入力ハンドルや他の仮想多項式から派生した多項式を効果的に生成および操作することができます。以下は2つの重要な方法です：

• パッキング
• シフト演算子

2.4 PIOP: Lasso lookup 引数の適応版

Lassoプロトコルは、証明者がベクトルa ∈ Fmをコミットし、そのすべての要素が事前に指定されたテーブルt ∈ Fnに存在することを証明することを許可します。Lassoプロトコルは以下の3つのコンポーネントで構成されています：

*大きなテーブルの仮想多項式抽象化 *小さなテーブル検索

• 多集合チェック

Biniusプロトコルは、Lassoをバイナリ領域の操作に適応させ、Lassoプロトコルの乗法バージョンを導入しました。

2.5 PCS:ブレーキダウンPCSの適応版

BiniusPCSの核心思想はpackingです。Biniusの論文では、2つのバイナリフィールドに基づくBrakedown多項式コミットメントスキームが提供されています：

1. concatenated codeを使用してインスタンス化する 2.ブロックレベルのエンコーディング技術を採用し、リードソロモンコードのみの使用をサポートします

Biniusの多項式コミットメントは主に以下の技術を使用しています：

• 小域多項式コミットメントと拡張体評価 *スモールドメインの一般的な構造
• ブロックコーディングとリード・ソロモン符号

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

3 思考の最適化

Biniusプロトコルの性能をさらに向上させるために、本稿では4つの重要な最適化ポイントを提案します：

1. GKRベースのPIOP：バイナリ領域の乗算演算に対して
2. ZeroCheck PIOP 最適化: Prover と Verifier 間の計算コストのトレードオフ
3. Sumcheck PIOP Optimization:スモールドメインのSumcheckの最適化
4. PCSの最適化:FRI-Biniusによって最適化

3.1 GKRベースのPIOP：GKRに基づくバイナリフィールド乗算

GKRに基づく整数乗算アルゴリズムでは、"2つの32ビット整数AとBがA·B =? Cを満たすかどうかを確認する"というプロセスを"中(gA)B =? gCが成り立つかどうかを確認する"に変換し、GKRプロトコルを利用してコミットメントコストを大幅に削減します。

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

3.2 ZeroCheck PIOP 最適化: Prover と Verifier 間の計算コストのトレードオフ

論文《Some Improvements for the PIOP for ZeroCheck》では、証明者（P）と検証者（V）間の作業負荷の配分を調整し、オーバーヘッドのバランスを取るためのさまざまな最適化案を提案しています。主な最適化には次のものが含まれます：

• データ提供者のデータ転送を削減する
• 評価ポイントの数を減らす *代数補間の最適化

! Bitlayer Research: Binius STARKs Principle Analysis and Optimization Thinking

3.3 Sumcheck PIOP 最適化: 小さなドメインに基づく Sumcheck プロトコル

Ingonyamaは2024年に小域ベースのSumcheckプロトコルの改善案を提案し、実装コードをオープンソース化しました。主な最適化は以下の通りです：

• ラウンド切り替えの影響と改善因子
• 基域のサイズがパフォーマンスに与える影響
• カラツバ法の最適化利益
• メモリ効率の向上

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

3.4 PCSの最適化:FRI-BiniusはBiniusプルーフサイズを下げます

論文「Polylogarithmic Proofs for Multilinears over Binary Towers」(略称:FRI-Binius)は、バイナリ領域のFRIフォールディングメカニズムを実装し、次の4つの側面で革新をもたらしています。

• フラット多項式
• サブスペース消失多項式
• アルジェブラ基のパッケージ *リングスワップサムチェック

FRI-Biniusを利用することで、Biniusの証明サイズを1桁減少させることができます。

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

4 まとめ

Biniusは「ハードウェア、ソフトウェア、およびFPGAで加速されたSumcheckプロトコル」を使用した協調設計ソリューションで、非常に低いメモリ使用率で迅速に証明できます。Biniusでは、Proverのcommitのボトルネックがほぼ完全に取り除かれており、新たなボトルネックはSumcheckプロトコルにあります。Sumcheckプロトコル内の多数の多項式評価やフィールド乗算などの問題は、専用ハードウェアを利用して効率的に解決できます。

FRI-Biniusソリューションは、FRIバリアントであり、集約証明層のコストが急増することなく、ドメイン証明層から埋め込みオーバーヘッドを排除する非常に魅力的な選択肢を提供します。現在、Irreducibleチームはその再帰層を開発しており、Polygonチームと協力してBiniusベースのzkVMを構築することを発表しました。JoltzkVMはLassoからBiniusに移行して再帰的パフォーマンスを改善しています。IngonyamaチームはBiniusのFPGAバージョンを実装しています。

! Bitlayer Research: Binius STARKs Principle Analysis and Optimization Thinking