論文の概要: Clap: a Rust eDSL for PlonKish Proof Systems with a Semantics-preserving Optimizing Compiler
- arxiv url: http://arxiv.org/abs/2405.12115v1
- Date: Mon, 20 May 2024 15:31:32 GMT
- ステータス: 処理完了
- システム内更新日: 2024-05-21 12:25:40.593513
- Title: Clap: a Rust eDSL for PlonKish Proof Systems with a Semantics-preserving Optimizing Compiler
- Title(参考訳): Clap: セマンティックス保存最適化コンパイラを備えたPlonKish Proof Systems用のRust eDSL
- Authors: Marco Stronati, Denis Firsov, Antonio Locascio, Benjamin Livshits,
- Abstract要約: Clapは、自動最適化と正式な保証を可能にする最初のRustエグノスティック回路フォーマットである。
クラップは、お互いに健全で完全なプロンキッシュの制約システムと目撃者生成装置を生成する。
- 参考スコア(独自算出の注目度): 7.469723382577489
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Writing Plonkish constraint systems by hand is tedious and error-prone; as a result, several libraries and DSL's have emerged over the years to facilitate this task as well as techniques to directly analyze constraint systems. However, standalone languages require developers to use a foreign toolchain and leave gaps between the application and its circuits. On the other hand, Rust-embedded DSL like Halo2 or Boojum lack in modularity; furthermore, it is usually impossible to tease apart the circuit from the proof system, making it hard to reuse circuits and even to compare performance of different proof systems on the same circuits. In this paper we introduce Clap, the first Rust eDSL to propose a prover-agnostic circuit format that enables extensibility, automatic optimizations, and formal guarantees for the resulting constraint system. Clap generates Plonkish constraint systems and witness generators that are sound and complete with respect to each other, leaving no room for subtle bugs due to under- or over-constraining. A model of this equivalence is proved in the Agda proof assistant for a subset of Clap's Rust implementation that is expressive enough to capture the compositional properties of our format. In order to increase the reuse of circuits, a number of optimizations are carried out automatically, sparing the developer from over-specifying low-level constraint system details in their circuit descriptions. We test the expressivity and efficiency of Clap on an implementation of the Poseidon2 hash function that produces a constraint system that is competitive in terms of size with hand-optimized Boojum circuits.
- Abstract(参考訳): Plonkishの制約システムを手作業で書くのは面倒でエラーを起こしやすい。その結果、この作業を促進するために、長年にわたっていくつかのライブラリやDSLが登場し、また、制約システムを直接解析する技術が登場した。
しかし、スタンドアロン言語では、開発者は外部ツールチェーンを使用し、アプリケーションとその回路間のギャップを残す必要がある。
一方、Halo2やBoojumのようなラスト埋め込みDSLはモジュール性に欠けており、証明システムから回路を分離することは不可能であり、同じ回路上で異なる証明システムの性能を比較することも困難である。
本稿では、拡張性、自動最適化、および結果の制約システムに対する正式な保証を可能にする、証明不能な回路フォーマットを提案する最初のRust eDSLであるClapを紹介する。
クラップはプロンキッシュの制約システムと目撃者生成装置を生成し、互いに健全で完全なもので、過度の制約や過度の制約による微妙なバグの余地は残っていない。
この等価性のモデルが、ClapのRust実装のサブセットであるAgda証明アシスタントで証明されている。
回路の再利用性を高めるために、開発者が回路記述の低レベル制約システムの詳細を過度に指定しないように、多数の最適化が自動的に実施される。
我々は,手動最適化Boojum回路と競合する制約系を生成するPoseidon2ハッシュ関数の実装において,Clapの表現性と効率を検証した。
関連論文リスト
- A General Framework for Gradient-Based Optimization of Superconducting Quantum Circuits using Qubit Discovery as a Case Study [0.19528996680336308]
超伝導量子回路の勾配に基づく最適化のための網羅的な枠組みを提案する。
この枠組みをキュービット発見問題に適用し、優れた性能指標を持つキュービット設計の同定の有効性を実証する。
論文 参考訳(メタデータ) (2024-08-22T19:46:50Z) - Finding Transformer Circuits with Edge Pruning [71.12127707678961]
自動回路発見の効率的かつスケーラブルなソリューションとしてエッジプルーニングを提案する。
本手法は,従来の手法に比べてエッジ数の半分未満のGPT-2の回路を探索する。
その効率のおかげで、Edge PruningをCodeLlama-13Bにスケールしました。
論文 参考訳(メタデータ) (2024-06-24T16:40:54Z) - Analyzing and Enhancing the Backward-Pass Convergence of Unrolled
Optimization [50.38518771642365]
ディープネットワークにおけるコンポーネントとしての制約付き最適化モデルの統合は、多くの専門的な学習タスクに有望な進歩をもたらした。
この設定における中心的な課題は最適化問題の解によるバックプロパゲーションであり、しばしば閉形式を欠いている。
本稿では, 非線形最適化の後方通過に関する理論的知見を提供し, 特定の反復法による線形システムの解と等価であることを示す。
Folded Optimizationと呼ばれるシステムが提案され、非ローリングなソルバ実装からより効率的なバックプロパゲーションルールを構築する。
論文 参考訳(メタデータ) (2023-12-28T23:15:18Z) - Fault-tolerant quantum architectures based on erasure qubits [49.227671756557946]
我々は、支配的なノイズを既知の場所での消去に効率よく変換することで、消去量子ビットの考え方を利用する。
消去量子ビットと最近導入されたFloquet符号に基づくQECスキームの提案と最適化を行う。
以上の結果から, 消去量子ビットに基づくQECスキームは, より複雑であるにもかかわらず, 標準手法よりも著しく優れていることが示された。
論文 参考訳(メタデータ) (2023-12-21T17:40:18Z) - Design and execution of quantum circuits using tens of superconducting qubits and thousands of gates for dense Ising optimization problems [12.220619768140903]
本研究では,各層におけるコストハミルトニアンのすべての相互作用のサブセットをパラメトリズする,既存のアンサツェから派生した,変動最適化のためのハードウェア効率の良いアンサッツを開発する。
最大5000個の2量子ビットおよび5000個の1量子ビットネイティブゲートを含む回路において、ランダムな推定オラクルを使用するよりも、性能が大幅に向上したことを報告した。
論文 参考訳(メタデータ) (2023-08-18T02:36:38Z) - Faster-than-Clifford Simulations of Entanglement Purification Circuits
and Their Full-stack Optimization [0.0]
我々は,$mathcalO(1)$のゲートシミュレーション複雑性を持つ蒸留回路のシミュレーションアルゴリズムを開発した。
これにより、単純な離散最適化アルゴリズムを用いて、純化回路を$n$の生ベル対から$k$の純化ペアに設計することができる。
結果として生じる浄化回路は、有限サイズのノイズのあるハードウェアにとって最もよく知られた浄化回路である。
論文 参考訳(メタデータ) (2023-07-12T18:00:00Z) - Adaptive Planning Search Algorithm for Analog Circuit Verification [53.97809573610992]
シミュレーションの少ない機械学習(ML)アプローチを提案する。
提案手法により,OCCを全回路の仕様に近づけることができることを示す。
論文 参考訳(メタデータ) (2023-06-23T12:57:46Z) - Performance Embeddings: A Similarity-based Approach to Automatic
Performance Optimization [71.69092462147292]
パフォーマンス埋め込みは、アプリケーション間でパフォーマンスチューニングの知識伝達を可能にする。
本研究では, 深層ニューラルネットワーク, 密度およびスパース線形代数合成, および数値風速予測ステンシルのケーススタディにおいて, この伝達チューニング手法を実証する。
論文 参考訳(メタデータ) (2023-03-14T15:51:35Z) - Post-selection-free preparation of high-quality physical qubits [0.0]
提案する量子回路の族は, 選択後無条件で高品質な |0> 状態を生成する。
2量子ゲートの誤差が0.2%以下になった場合、有意義な性能向上が得られます。
論文 参考訳(メタデータ) (2022-09-12T16:42:33Z) - Finite-time System Identification and Adaptive Control in Autoregressive
Exogenous Systems [79.67879934935661]
未知のARXシステムのシステム識別と適応制御の問題について検討する。
我々は,オープンループとクローズループの両方のデータ収集の下で,ARXシステムに対する有限時間学習保証を提供する。
論文 参考訳(メタデータ) (2021-08-26T18:00:00Z) - QubiC: An open source FPGA-based control and measurement system for
superconducting quantum information processors [5.310385728746101]
超伝導量子処理ユニットを制御・測定するために,QubiCと呼ばれるモジュール型FPGAを設計する。
プロトタイプのハードウェアモジュールは、市販の市販評価ボードと、社内で開発された回路基板から組み立てられる。
システム機能と性能は、キュービットチップの特性評価、ゲート最適化、ランダム化されたベンチマークシーケンスによって実証される。
論文 参考訳(メタデータ) (2020-12-31T21:06:28Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。