Fugu-MT 論文翻訳(概要): Formal verification of the S-two AIR

論文の概要: Formal verification of the S-two AIR

arxiv url: http://arxiv.org/abs/2606.04311v1
Date: Wed, 03 Jun 2026 00:36:41 GMT
ステータス: 翻訳完了
システム内更新日: 2026-06-04 20:44:18.442639
Title: Formal verification of the S-two AIR
Title（参考訳）: S-2エアーの形式的検証
Authors: Jeremy Avigad, Anat Ganor, Lior Goldberg, David Levit, Ohad Nir, Yoav Seginer, Alon Titelman,
Abstract要約: StarkWareのS-two証明は、カイロ仮想マシン言語で記述されたプログラムを完了まで実行させる効率的な手段を提供する。 Lean 4の証明アシスタントを使って、エンコーディングが健全であることを検証します。
参考スコア（独自算出の注目度）: 0.9479099294667721
License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
Abstract: StarkWare's S-two prover provides an efficient means for establishing, on blockchain, that a program written in the Cairo virtual machine language runs to completion. The latter claim is encoded by an algebraic intermediate representation (AIR) that captures the semantics of the Cairo language. The AIR asserts the existence of tables of values from a finite field satisfying certain algebraic constraints. A cryptographic interactive proof system, circle STARK, provides an efficiently-checked certificate that the AIR is satisfied. We describe our verification, using the Lean 4 proof assistant, that the AIR encoding is sound, which is to say, the satisfiability of the AIR implies the computational claim.
Abstract（参考訳）: StarkWareのS-two証明は、ブロックチェーン上で、Cairo仮想マシン言語で記述されたプログラムが完了まで実行されることを確立する効率的な手段を提供する。後者の主張は、カイロ語の意味を捉える代数的中間表現(AIR)によって符号化される。 AIRは、ある代数的制約を満たす有限体からの値のテーブルの存在を主張する。暗号対話型証明システムである円STARKは、AIRが満たされるような効率よくチェックされた証明書を提供する。私たちは、Lean 4の証明アシスタントを使って、AIRのエンコーディングが音であること、つまりAIRの満足度が計算的クレームを意味することを検証します。

関連論文リスト

Lemma Discovery in Agentic Program Verification [12.551445518827768]
帰納的検証は、検証条件(VC)を抽出し、それらの公式な証明を書くことによって、コードに対して強い正当性を保証する。 VC証明の専門知識集約的なタスクは、このプロセスの主要なボトルネックであり、最近のLarge Language Model (LLM)エージェントの進歩により部分的に自動化されている。私たちは、プログラム検証のためのVCの証明は純粋に数学的タスク以上のものであり、プログラムの理解からかなりの恩恵を受けると主張している。
論文参考訳（メタデータ） (2026-03-23T15:42:07Z)
Authenticated Contradictions from Desynchronized Provenance and Watermarking [48.47756819432157]
この研究は、$textitIntegrity Clash$を形式化し、実証的に実証している。本稿では,3500枚のテスト画像に対して100%の分類精度を達成し,証明メタデータと透かし検出ステータスを共同評価する層間監査プロトコルを提案する。
論文参考訳（メタデータ） (2026-03-02T20:42:12Z)
AlgoVeri: An Aligned Benchmark for Verified Code Generation on Classical Algorithms [54.99368693313797]
既存のベンチマークでは、個々の言語/ツールのみをテストするため、パフォーマンス番号は直接比較できない。このギャップに対処するAlgoVeriは、Dafny、Verus、Leanで77ドルの古典的アルゴリズムのベリコーディングを評価するベンチマークです。
論文参考訳（メタデータ） (2026-02-10T06:58:26Z)
A Proof-Producing Compiler for Blockchain Applications [0.0873811641236639]
CairoZeroは、分散アプリケーション(dApps)を大規模に実行するためのプログラミング言語である。暗号化プロトコルは、ブロックチェーン上での実行結果を効率的に検証するために使用される。ユーザがLean 3の証明アシスタントで、コンパイルされたコードが高レベルの機能仕様を満たすことを証明できるように、CairoZeroコンパイラをいかに拡張したかを示します。
論文参考訳（メタデータ） (2025-01-25T00:31:47Z)
AC4: Algebraic Computation Checker for Circuit Constraints in ZKPs [4.810904298160317]
過度に制約された回路や過度に制約された回路はバグを引き起こす可能性がある。提案手法の実装を表すためにAC4というツールが提案されている。解決可能な範囲内では、チェック時間も顕著に改善されている。
論文参考訳（メタデータ） (2024-03-23T01:44:57Z)
Oracle Computability and Turing Reducibility in the Calculus of Inductive Constructions [0.0]
インダクティブ・コンストラクションの計算におけるオラクル計算可能性とチューリング再現性の概念を総合的に展開する。通常、合成手法では、メタレベル関数に基づいたオラクル計算の定義を用いる。チューリングの再現性は上半格子を形成し、決定可能性を持ち、真理値の再現性よりも厳密に表現可能であることを示す。
論文参考訳（メタデータ） (2023-07-28T13:16:46Z)
BERM: Training the Balanced and Extractable Representation for Matching to Improve Generalization Ability of Dense Retrieval [54.66399120084227]
本稿では,BERMと呼ばれるマッチング信号の取得により,高密度検索の一般化を改善する手法を提案する。センス検索は、ドメイン内のラベル付きデータセットでトレーニングされた場合、第1段階の検索プロセスにおいて有望であることが示されている。
論文参考訳（メタデータ） (2023-05-18T15:43:09Z)
Precise Zero-Shot Dense Retrieval without Relevance Labels [60.457378374671656]
仮説文書埋め込み(英: hypothetical Document Embeddings, HyDE)は、ゼロショット高密度検索システムである。我々は,HyDEが最先端の非教師付き高密度検索器であるContrieverを著しく上回っていることを示す。
論文参考訳（メタデータ） (2022-12-20T18:09:52Z)
Quantum Proofs of Deletion for Learning with Errors [91.3755431537592]
完全同型暗号方式として, 完全同型暗号方式を初めて構築する。我々の主要な技術要素は、量子証明器が古典的検証器に量子状態の形でのLearning with Errors分布からのサンプルが削除されたことを納得させる対話的プロトコルである。
論文参考訳（メタデータ） (2022-03-03T10:07:32Z)
Hierarchical Variational Autoencoder for Visual Counterfactuals [79.86967775454316]
条件変量オート(VAE)は、説明可能な人工知能(XAI)ツールとして注目されている。本稿では, 後部の効果がいかに緩和され, 対物的効果が成功するかを示す。本稿では,アプリケーション内の分類器を視覚的に監査できる階層型VAEについて紹介する。
論文参考訳（メタデータ） (2021-02-01T14:07:11Z)

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