論文の概要: ILA: Correctness via Type Checking for Fully Homomorphic Encryption

• arxiv url: http://arxiv.org/abs/2509.11559v1
• Date: Mon, 15 Sep 2025 03:45:53 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-09-16 17:26:23.142689
• Title: ILA: Correctness via Type Checking for Fully Homomorphic Encryption
• Title（参考訳）: ILA: 完全同型暗号化のための型チェックによる正確性
• Authors: Tarakaram Gollamudi, Anitha Gollamudi, Joshua Gancher,
• Abstract要約: RLWEをベースとしたFully Homomorphic Encryption (FHE) スキームは、暗号化中にメッセージに小さなエンフォネーズを加える。 ノイズが臨界値を超えると、FHE回路は誤った出力を生成する。 既存のライブラリとコンパイラは、ノイズを静的に追跡するための限定的なサポートを提供する。 準同型評価を目的とした型チェック回路に対して,直交性指向型IRである中間言語(中間言語)を提案する。
• 参考スコア（独自算出の注目度）: 0.42821598129654453
• License: http://creativecommons.org/licenses/by-nc-nd/4.0/
• Abstract: RLWE-based Fully Homomorphic Encryption (FHE) schemes add some small \emph{noise} to the message during encryption. The noise accumulates with each homomorphic operation. When the noise exceeds a critical value, the FHE circuit produces an incorrect output. This makes developing FHE applications quite subtle, as one must closely track the noise to ensure correctness. However, existing libraries and compilers offer limited support to statically track the noise. Additionally, FHE circuits are also plagued by wraparound errors that are common in finite modulus arithmetic. These two limitations of existing compilers and libraries make FHE applications too difficult to develop with confidence. In this work, we present a \emph{correctness-oriented} IR, Intermediate Language for Arithmetic circuits, for type-checking circuits intended for homomorphic evaluation. Our IR is backed by a type system that tracks low-level quantitative bounds (e.g., ciphertext noise) without using the secret key. Using our type system, we identify and prove a strong \emph{functional correctness} criterion for \ila circuits. Additionally, we have designed \ila to be maximally general: our core type system does not directly assume a particular FHE scheme, but instead axiomatizes a \emph{model} of FHE. We instantiate this model with the exact FHE schemes (BGV, BFV and TFHE), and obtain functional correctness for free.
• Abstract（参考訳）: RLWEベースのFully Homomorphic Encryption (FHE) スキームは、暗号化中にメッセージに小さな \emph{noise} を追加する。 ノイズは各ホモモルフィック操作で蓄積される。 ノイズが臨界値を超えると、FHE回路は誤った出力を生成する。 これにより、FHEアプリケーションを非常に微妙に開発することができる。 しかし、既存のライブラリやコンパイラはノイズを静的に追跡するための限定的なサポートを提供している。 さらに、FHE回路は有限モジュラー算術に共通するラップアラウンド誤差にも悩まされている。 既存のコンパイラとライブラリの2つの制限は、FHEアプリケーションを自信を持って開発することを困難にしている。 本研究では,同相性評価を目的とした型チェック回路のための中間言語である<emph{correctness-oriented} IRを提案する。 我々のIRは、秘密鍵を使わずに低レベルの量的境界(例えば、暗号文ノイズ)を追跡する型システムによって支えられている。 タイプシステムを用いて、ニラ回路に対する強い \emph{functional correctness} 基準を同定し、証明する。 コア型システムは、特定の FHE スキームを直接仮定するのではなく、代わりに FHE の \emph{model} を公理化する。 我々は、このモデルを正確なFHEスキーム(BGV、BFV、TFHE)でインスタンス化し、機能的正しさを無償で取得する。

関連論文リスト

• Measuring Uncertainty in Transformer Circuits with Effective Information Consistency [0.0]
  本研究では,トランスフォーマー回路のシャーフ/コホモロジーと因果出現の視点を開発する。 EICSは(i)局所ジャコビアンとアクティベーションから計算された正規化棚の不整合と(ii)回路レベルの因果発生のためのガウスEIプロキシを組み合わせる。 本稿では,スコアの解釈,計算オーバーヘッド(高速かつ高精度なモード),およびおもちゃの健全性チェック分析に関する実践的ガイダンスを提供する。
  論文  参考訳（メタデータ） (2025-09-08T18:54:56Z)
• Compile-Time Fully Homomorphic Encryption of Vectors: Eliminating Online Encryption via Algebraic Basis Synthesis [1.3824176915623292]
  暗号文は、事前計算された暗号化ベースベクターとランタイムスケールの0の暗号化を組み合わせた構成である。 ランダム化された$mathbbZ_t$-加群として定式化し、標準仮定の下でIND-CPAセキュリティを満たすことを証明した。 ゼロのランダムな暗号のプールを必要とする以前の設計とは異なり、我々の構成は実行時に新しいスカラーによって乗算された1つのゼロ暗号文を用いて等価なセキュリティを実現する。
  論文  参考訳（メタデータ） (2025-05-19T00:05:18Z)
• Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming [8.34623776815378]
  我々は600K行のオープンソースF*プログラムと証明のデータセットをキュレートする。 このデータセットには、Windows、Linux、Python、Firefoxなど、プロダクションシステムで使用されるソフトウェアが含まれている。 我々は,AIを用いてプログラムとその証明をF*で合成し,有望な結果を得る。
  論文  参考訳（メタデータ） (2024-05-03T00:14:33Z)
• LM-Combiner: A Contextual Rewriting Model for Chinese Grammatical Error Correction [49.0746090186582]
  過剰補正は中国の文法的誤り訂正(CGEC)タスクにおいて重要な問題である。 モデルアンサンブル法による最近の研究は、過剰補正を効果的に軽減し、ECCシステムの精度を向上させることができる。 本稿では,GECシステム出力の過度補正をモデルアンサンブルなしで直接修正できる書き換えモデルLM-Combinerを提案する。
  論文  参考訳（メタデータ） (2024-03-26T06:12:21Z)
• GEC-DePenD: Non-Autoregressive Grammatical Error Correction with Decoupled Permutation and Decoding [52.14832976759585]
  文法的誤り訂正(GEC)は、通常自己回帰的なシーケンス・ツー・シーケンスモデルで解決される重要なNLPタスクである。 本稿では, アーキテクチャを置換ネットワークに分離する, GEC に対する非自己回帰的アプローチを提案する。 GECの既知の非自己回帰手法よりもネットワークが向上することを示す。
  論文  参考訳（メタデータ） (2023-11-14T14:24:36Z)
• GRACE: Discriminator-Guided Chain-of-Thought Reasoning [75.35436025709049]
  本稿では, 正しい推論手順を導出するために, GRACE (CorrectnEss Discriminator) を用いたチェーン・オブ・シークレット・リAsoningを提案する。 GRACEは、正しいステップと間違ったステップに対して対照的な損失で訓練された判別器を採用しており、復号時に次のステップ候補を採点するために使用される。
  論文  参考訳（メタデータ） (2023-05-24T09:16:51Z)
• LM-Critic: Language Models for Unsupervised Grammatical Error Correction [128.9174409251852]
  文を文法的に判断する LM-Critic の定義において,事前訓練された言語モデル (LM) の活用法を示す。 このLM-Critic と BIFI と、ラベルなし文の集合を併用して、現実的な非文法的/文法的ペアをブートストラップし、修正子を訓練する。
  論文  参考訳（メタデータ） (2021-09-14T17:06:43Z)
• Hardness of Random Optimization Problems for Boolean Circuits, Low-Degree Polynomials, and Langevin Dynamics [78.46689176407936]
  アルゴリズムの族は高い確率でほぼ最適な解を生成できないことを示す。 ブール回路の場合、回路複雑性理論で知られている最先端境界を改善する。
  論文  参考訳（メタデータ） (2020-04-25T05:45:59Z)

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

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