論文の概要: Homomorphic Encryption of Intuitionistic Logic Proofs and Functional Programs: A Categorical Approach Inspired by Composite-Order Bilinear Groups
- arxiv url: http://arxiv.org/abs/2503.05779v1
- Date: Wed, 26 Feb 2025 10:10:10 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-03-16 08:47:02.421172
- Title: Homomorphic Encryption of Intuitionistic Logic Proofs and Functional Programs: A Categorical Approach Inspired by Composite-Order Bilinear Groups
- Title(参考訳): 直観主義論理証明と関数プログラムの同型暗号化:複合次双線型群に着想を得たカテゴリー的アプローチ
- Authors: Ben Goertzel,
- Abstract要約: 本稿では、算術やブール演算以外の同型暗号を直観論理の領域に拡張するための概念的枠組みを提案する。
ソフトウェア最適化やハードウェアアクセラレーションなど,このアプローチを潜在的に効率的にするための戦略を概説する。
- 参考スコア(独自算出の注目度): 0.0
- License:
- Abstract: We present a conceptual framework for extending homomorphic encryption beyond arithmetic or Boolean operations into the domain of intuitionistic logic proofs and, by the Curry-Howard correspondence, into the domain of typed functional programs. We begin by reviewing well-known homomorphic encryption schemes for arithmetic operations, and then discuss the adaptation of similar concepts to support logical inference steps in intuitionistic logic. Key to our construction are polynomial functors and Bounded Natural Functors (BNFs), which serve as a categorical substrate on which logic formulas and proofs are represented and manipulated. We outline a complexity-theoretic hardness assumption -- the BNF Distinguishing Problem, constructed via a reduction from Subgraph Isomorphism, providing a foundation for cryptographic security. Finally, we describe how these methods can homomorphically encode the execution of total, dependently typed functional programs, and outline strategies for making the approach potentially efficient, including software optimizations and hardware acceleration.
- Abstract(参考訳): 本稿では、算術やブール演算以外の準同型暗号を直観論的論理証明の領域に拡張するための概念的枠組みと、カリー・ホワード対応により、型付き関数プログラムの領域に拡張する。
まず、算術演算のためのよく知られた同型暗号化スキームの見直しから始め、直観論的論理における論理推論ステップをサポートするための類似概念の適応について議論する。
我々の構築の鍵となるのは多項式関手と境界自然関手(BNF)であり、これは論理式と証明が表現され、操作されるカテゴリの基質として機能する。
本稿では,部分グラフアイソモーフィズム(Subgraph Isomorphism)の低減により構築されたBNFディスティネーション問題(BNF Distinguishing Problem)という複雑性理論的硬さの仮定を概説し,暗号セキュリティの基礎となる。
最後に、これらの手法が全型依存型関数プログラムの実行を均質に符号化し、ソフトウェア最適化やハードウェアアクセラレーションを含むアプローチを効果的にするための戦略を概説する。
関連論文リスト
- On Computational Indistinguishability and Logical Relations [1.024113475677323]
この研究は、疑似乱数関数によって誘導される暗号化スキームが、純粋に方程式的なスタイルでアクティブな敵に対して安全であることが証明されたセキュリティ証明の例で締めくくられる。
論文 参考訳(メタデータ) (2024-08-30T15:08:51Z) - Logical recognition method for solving the problem of identification in
the Internet of Things [0.0]
本研究の目的は、非交差オブジェクトの論理的特徴とクラスを持つ参照テーブルからなるオブジェクト認識のための論理的手法を開発することである。
この手法は、参照テーブルを至るところで定義されていない論理関数として考慮し、特徴空間全体への論理関数の最適継続を構築する。
論文 参考訳(メタデータ) (2024-02-06T19:20:58Z) - An Encoding of Abstract Dialectical Frameworks into Higher-Order Logic [57.24311218570012]
このアプローチは抽象弁証法フレームワークのコンピュータ支援分析を可能にする。
応用例としては、メタ理論的性質の形式的解析と検証がある。
論文 参考訳(メタデータ) (2023-12-08T09:32:26Z) - Query Structure Modeling for Inductive Logical Reasoning Over Knowledge
Graphs [67.043747188954]
KGに対する帰納的論理的推論のための構造モデル付きテキスト符号化フレームワークを提案する。
線形化されたクエリ構造とエンティティを、事前訓練された言語モデルを使ってエンコードして、回答を見つける。
2つの帰納的論理推論データセットと3つの帰納的推論データセットについて実験を行った。
論文 参考訳(メタデータ) (2023-05-23T01:25:29Z) - Object Representations as Fixed Points: Training Iterative Refinement
Algorithms with Implicit Differentiation [88.14365009076907]
反復的洗練は表現学習に有用なパラダイムである。
トレーニングの安定性とトラクタビリティを向上させる暗黙の差別化アプローチを開発する。
論文 参考訳(メタデータ) (2022-07-02T10:00:35Z) - A Formalisation of Abstract Argumentation in Higher-Order Logic [77.34726150561087]
本稿では,古典的高階論理へのエンコーディングに基づく抽象的議論フレームワークの表現手法を提案する。
対話型および自動推論ツールを用いた抽象的議論フレームワークのコンピュータ支援評価のための一様フレームワークを提供する。
論文 参考訳(メタデータ) (2021-10-18T10:45:59Z) - Refining Labelled Systems for Modal and Constructive Logics with
Applications [0.0]
この論文は、モーダル論理や構成論理のセマンティクスを「経済的な」証明システムに変換する手段として機能する。
精製法は、ラベル付きおよびネストされたシーケント計算の2つの証明理論パラダイムを結合する。
導入された洗練されたラベル付き電卓は、デオン性STIT論理に対する最初の証明探索アルゴリズムを提供するために使用される。
論文 参考訳(メタデータ) (2021-07-30T08:27:15Z) - Fractal Structure and Generalization Properties of Stochastic
Optimization Algorithms [71.62575565990502]
最適化アルゴリズムの一般化誤差は、その一般化尺度の根底にあるフラクタル構造の複雑性'にバウンドできることを示す。
さらに、特定の問題(リニア/ロジスティックレグレッション、隠れ/層ニューラルネットワークなど)とアルゴリズムに対して、結果をさらに専門化します。
論文 参考訳(メタデータ) (2021-06-09T08:05:36Z) - Differentiable Inductive Logic Programming for Structured Examples [6.8774606688738995]
雑音や構造化例から論理プログラムを学ぶための新しいフレームワークを提案する。
我々の新しいフレームワークは、シーケンスやツリーなど、ノイズや構造化された例から論理プログラムを学習できることを示します。
我々のフレームワークは、関数記号を持つ複数の節からなる複雑なプログラムを扱うためにスケールできる。
論文 参考訳(メタデータ) (2021-03-02T13:47:33Z) - Patterns of Cognition: Cognitive Algorithms as Galois Connections
Fulfilled by Chronomorphisms On Probabilistically Typed Metagraphs [0.0]
AGI関連アルゴリズムの幅広いクラスは、共通の形式的なフレームワークで表現できると論じられている。
例としては、OpenCog AGIフレームワークで使用されるコア認知アルゴリズムがある。
論文 参考訳(メタデータ) (2021-02-21T10:50:40Z) - Finite-Function-Encoding Quantum States [52.77024349608834]
任意の$d$値論理関数を符号化する有限関数符号化(FFE)を導入する。
それらの構造的特性について検討する。
論文 参考訳(メタデータ) (2020-12-01T13:53:23Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。