論文の概要: Exploiting the Potential of Linearity in Automatic Differentiation and Computational Cryptography
- arxiv url: http://arxiv.org/abs/2510.17220v1
- Date: Mon, 20 Oct 2025 07:02:48 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-10-25 00:56:39.343663
- Title: Exploiting the Potential of Linearity in Automatic Differentiation and Computational Cryptography
- Title(参考訳): 自動微分・計算暗号における線形性の可能性の爆発
- Authors: Giulia Giusti,
- Abstract要約: 線形性の概念は数学と計算機科学の両方において中心的な役割を果たす。
この論文では線形性に基づいたプログラミングパラダイムのモデル化にLinear Logic (LL) を用いることについて論じている。
ADLLとCryptoBLLの2つの部分から構成される。
- 参考スコア(独自算出の注目度): 0.0
- License: http://creativecommons.org/licenses/by-nc-sa/4.0/
- Abstract: The concept of linearity plays a central role in both mathematics and computer science, with distinct yet complementary meanings. In mathematics, linearity underpins functions and vector spaces, forming the foundation of linear algebra and functional analysis. In computer science, it relates to resource-sensitive computation. Linear Logic (LL), for instance, models assumptions that must be used exactly once, providing a natural framework for tracking computational resources such as time, memory, or data access. This dual perspective makes linearity essential to programming languages, type systems, and formal models that express both computational complexity and composability. Bridging these interpretations enables rigorous yet practical methodologies for analyzing and verifying complex systems. This thesis explores the use of LL to model programming paradigms based on linearity. It comprises two parts: ADLL and CryptoBLL. The former applies LL to Automatic Differentiation (AD), modeling linear functions over the reals and the transposition operation. The latter uses LL to express complexity constraints on adversaries in computational cryptography. In AD, two main approaches use linear type systems: a theoretical one grounded in proof theory, and a practical one implemented in JAX, a Python library developed by Google for machine learning research. In contrast, frameworks like PyTorch and TensorFlow support AD without linear types. ADLL aims to bridge theory and practice by connecting JAX's type system to LL. In modern cryptography, several calculi aim to model cryptographic proofs within the computational paradigm. These efforts face a trade-off between expressiveness, to capture reductions, and simplicity, to abstract probability and complexity. CryptoBLL addresses this tension by proposing a framework for the automatic analysis of protocols in computational cryptography.
- Abstract(参考訳): 線形性の概念は数学と計算機科学の両方において中心的な役割を担い、異なるが相補的な意味を持つ。
数学において、線型性は函数とベクトル空間を根ざし、線型代数と汎函数解析の基礎を形成する。
計算機科学では、リソースに敏感な計算に関係している。
例えば、線形論理(LL)は、正確に1回使用する必要がある仮定をモデル化し、時間、メモリ、データアクセスなどの計算資源を追跡する自然なフレームワークを提供する。
この双対的な視点は、計算複雑性と構成可能性の両方を表現するプログラミング言語、型システム、形式モデルに線形性を不可欠にしている。
これらの解釈をブリッジすることで、複雑なシステムを分析し検証するための厳密で実用的な方法論が可能になる。
この論文は、線形性に基づいたプログラミングパラダイムのモデル化にLLを使うことを探求している。
ADLLとCryptoBLLの2つの部分から構成される。
前者はLLを自動微分(AD)に適用し、実数上の線形関数と転置演算をモデル化する。
後者はLLを用いて計算暗号における敵の複雑さの制約を表現している。
ADでは2つの主要なアプローチが線形型システムを使用する: 証明理論に基づく理論的手法と、Googleが機械学習研究のために開発したPythonライブラリであるJAXで実装された実践的手法である。
対照的に、PyTorchやTensorFlowといったフレームワークは、線形型なしでADをサポートする。
ADLL は JAX の型システムを LL に接続することで理論と実践を橋渡しすることを目指している。
現代の暗号学において、いくつかの計算は、計算パラダイム内で暗号証明をモデル化することを目的としている。
これらの取り組みは、表現力と還元と単純さを捉え、確率と複雑さを抽象化するトレードオフに直面します。
CryptoBLLはこの緊張に対処し、計算暗号におけるプロトコルの自動解析のためのフレームワークを提案する。
関連論文リスト
- Generative Logic: A New Computer Architecture for Deterministic Reasoning and Knowledge Generation [0.0]
Generative Logic (GL) は、ユーザの公理的定義から始まる決定論的アーキテクチャである。
GLは予想を列挙し、正規化、型、CEフィルタを適用し、機械チェック可能な証明を自動的に再構築する。
論文 参考訳(メタデータ) (2025-07-25T17:29:19Z) - Learning Linear Attention in Polynomial Time [127.14106124669645]
線形注意を持つ単層変圧器の学習性に関する最初の結果を提供する。
線形アテンションは RKHS で適切に定義された線形予測器とみなすことができる。
我々は,すべての経験的リスクが線形変換器と同等のトレーニングデータセットを効率的に識別する方法を示す。
論文 参考訳(メタデータ) (2024-10-14T02:41:01Z) - CoLA: Exploiting Compositional Structure for Automatic and Efficient
Numerical Linear Algebra [62.37017125812101]
機械学習における大規模線形代数問題に対して, CoLA という, 単純だが汎用的なフレームワークを提案する。
線形演算子抽象と合成ディスパッチルールを組み合わせることで、CoLAはメモリと実行時の効率的な数値アルゴリズムを自動的に構築する。
偏微分方程式,ガウス過程,同変モデル構築,教師なし学習など,幅広い応用で有効性を示す。
論文 参考訳(メタデータ) (2023-09-06T14:59:38Z) - Stabilizing Q-learning with Linear Architectures for Provably Efficient
Learning [53.17258888552998]
本研究では,線形関数近似を用いた基本的な$Q$-learningプロトコルの探索変種を提案する。
このアルゴリズムの性能は,新しい近似誤差というより寛容な概念の下で,非常に優雅に低下することを示す。
論文 参考訳(メタデータ) (2022-06-01T23:26:51Z) - Statistically Meaningful Approximation: a Case Study on Approximating
Turing Machines with Transformers [50.85524803885483]
本研究は,統計的学習性を示すために近似ネットワークを必要とする統計有意(SM)近似の形式的定義を提案する。
回路とチューリングマシンの2つの機能クラスに対するSM近似について検討する。
論文 参考訳(メタデータ) (2021-07-28T04:28:55Z) - Tensor Relational Algebra for Machine Learning System Design [7.764107702934616]
本稿では、リレーショナルテンソル代数(TRA)と呼ばれる別の実装抽象化を提案する。
TRA は、リレーショナル代数に基づく集合基底代数である。
我々の実証研究は、最適化されたTRAベースのバックエンドが、分散クラスタでMLを実行する際の選択肢を大幅に上回っていることを示している。
論文 参考訳(メタデータ) (2020-09-01T15:51:24Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。