論文の概要: Formally Verifying Noir Zero Knowledge Programs with NAVe

• arxiv url: http://arxiv.org/abs/2601.09372v1
• Date: Wed, 14 Jan 2026 10:56:17 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-01-15 18:59:20.37348
• Title: Formally Verifying Noir Zero Knowledge Programs with NAVe
• Title（参考訳）: NAVeを用いた雑音ゼロ知識プログラムの形式的検証
• Authors: Pedro Antonino, Namrata Jain,
• Abstract要約: 我々は、Noirプログラミング言語のためのオープンソースの形式検証器を作成する。 Noirプログラムが適切に制約されているかどうかを確認するために使用できる。 我々は,4種類のNoirプログラムに対して検証を行い,評価を行った。
• 参考スコア（独自算出の注目度）: 0.7366405857677226
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Zero-Knowledge (ZK) proof systems are cryptographic protocols that can (with overwhelming probability) demonstrate that the pair $(X, W)$ is in a relation $R$ without revealing information about the private input $W$. This membership checking is captured by a complex arithmetic circuit: a set of polynomial equations over a finite field. ZK programming languages, like Noir, have been proposed to simplify the description of these circuits. A developer can write a Noir program using traditional high-level constructs that can be compiled into a lower-level ACIR (Abstract Circuit Intermediate Representation), which is essentially a high-level description of an arithmetic circuit. In this paper, we formalise some of the ACIR language using SMT-LIB and its extended theory of finite fields. We use this formalisation to create an open-source formal verifier for the Noir language using the SMT solver cvc5. Our verifier can be used to check whether Noir programs behave appropriately. For instance, it can be used to check whether a Noir program has been properly constrained, that is, the finite-field polynomial equations generated truly capture the intended relation. We evaluate our verifier over 4 distinct sets of Noir programs, demonstrating its practical applicability and identifying a hard-to-check constraint type that charts an improvement path for our verification framework.
• Abstract（参考訳）: Zero-Knowledge (ZK) 証明システムは暗号プロトコルであり、(圧倒的な確率で)ペア$(X, W)$がプライベート入力の$W$に関する情報を公開せずに関係$R$にあることを示す。 このメンバシップチェックは複素演算回路(有限体上の多項式方程式の集合)によって捕捉される。 ノワールのようなZKプログラミング言語は、これらの回路の記述を単純化するために提案されている。 開発者は、算術回路の高レベル記述である低レベルACIR(Abstract Circuit Intermediate Representation)にコンパイルできる従来の高レベル構造を使って、Noirプログラムを書くことができる。 本稿では、SMT-LIBと拡張有限体理論を用いてACIR言語の一部を定式化する。 我々はこの形式化を用いて、SMTソルバcvc5を用いて、Noir言語のためのオープンソースの形式検証を作成する。 我々の検証器は、Noirプログラムが適切に振る舞うかどうかを確認するのに利用できる。 例えば、Noirプログラムが適切に制約されているかどうか、すなわち、生成した有限体多項式方程式が意図した関係を真に捉えているかどうかを確認するのに使うことができる。 我々は,4つの異なるNoirプログラムに対して検証を行い,その実用性を実証し,検証フレームワークの改善経路を図示する厳密な検証制約タイプを特定した。

関連論文リスト

• ILA: Correctness via Type Checking for Fully Homomorphic Encryption [0.42821598129654453]
  RLWEをベースとしたFully Homomorphic Encryption (FHE) スキームは、暗号化中にメッセージに小さなエンフォネーズを加える。 ノイズが臨界値を超えると、FHE回路は誤った出力を生成する。 既存のライブラリとコンパイラは、ノイズを静的に追跡するための限定的なサポートを提供する。 準同型評価を目的とした型チェック回路に対して,直交性指向型IRである中間言語(中間言語)を提案する。
  論文  参考訳（メタデータ） (2025-09-15T03:45:53Z)
• Generative Logic: A New Computer Architecture for Deterministic Reasoning and Knowledge Generation [0.0]
  Generative Logic (GL) は、ユーザの公理的定義から始まる決定論的アーキテクチャである。 GLは予想を列挙し、正規化、型、CEフィルタを適用し、機械チェック可能な証明を自動的に再構築する。
  論文  参考訳（メタデータ） (2025-07-25T17:29:19Z)
• Safe: Enhancing Mathematical Reasoning in Large Language Models via Retrospective Step-aware Formal Verification [56.218970738892764]
  Chain-of-Thoughtプロンプトは、大規模言語モデル(LLM)から推論能力を引き出すデファクトメソッドとなっている。 検出が極めて難しいCoTの幻覚を緩和するために、現在の方法は不透明なボックスとして機能し、彼らの判断に対する確認可能な証拠を提供しておらず、おそらくその効果を制限する。 任意のスコアを割り当てるのではなく、各推論ステップで形式数学言語Lean 4で数学的主張を明確にし、幻覚を識別するための公式な証明を提供しようとしている。
  論文  参考訳（メタデータ） (2025-06-05T03:16:08Z)
• Categorical Schrödinger Bridge Matching [58.760054965084656]
  Schr"odinger Bridge (SB)は、未ペアドメイン翻訳のような生成モデリングタスクを解決するための強力なフレームワークである。 我々は、最近導入されたイテレーティブマルコフフィッティング(IMF)法を用いて、離散空間におけるSBを解くための理論的かつアルゴリズム的な基礎を提供する。 これにより、我々はCSBM(Categorical Schr"odinger Bridge Matching)と呼ばれるSBの実用的な計算アルゴリズムを開発することができる。
  論文  参考訳（メタデータ） (2025-02-03T14:55:28Z)
• Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming [8.34623776815378]
  我々は600K行のオープンソースF*プログラムと証明のデータセットをキュレートする。 このデータセットには、Windows、Linux、Python、Firefoxなど、プロダクションシステムで使用されるソフトウェアが含まれている。 我々は,AIを用いてプログラムとその証明をF*で合成し,有望な結果を得る。
  論文  参考訳（メタデータ） (2024-05-03T00:14:33Z)
• Guess & Sketch: Language Model Guided Transpilation [59.02147255276078]
  学習されたトランスパイレーションは、手作業による書き直しやエンジニアリングの取り組みに代わるものだ。 確率的ニューラルネットワークモデル(LM)は、入力毎に可塑性出力を生成するが、正確性を保証するコストがかかる。 Guess & Sketch は LM の特徴からアライメントと信頼性情報を抽出し、意味的等価性を解決するためにシンボリック・ソルバに渡す。
  論文  参考訳（メタデータ） (2023-09-25T15:42:18Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。