論文の概要: Dynamic IFC Theorems for Free!
- arxiv url: http://arxiv.org/abs/2005.04722v3
- Date: Thu, 22 Feb 2024 21:58:36 GMT
- ステータス: 処理完了
- システム内更新日: 2024-03-26 00:17:07.138288
- Title: Dynamic IFC Theorems for Free!
- Title(参考訳): Dynamic IFC Theorems for Free!
- Authors: Maximilian Algehed, Jean-Philippe Bernardy, Catalin Hritcu,
- Abstract要約: 我々は、動的IFCライブラリの鍵となる音性定理である非干渉と透明性を「無償」で得ることを示す。
私たちの証明は、型抽象化の観点から、ライブラリのAgda実装を完全に機械化しても、短いままです。
- 参考スコア(独自算出の注目度): 2.482198622504409
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: We show that noninterference and transparency, the key soundness theorems for dynamic IFC libraries, can be obtained "for free", as direct consequences of the more general parametricity theorem of type abstraction. This allows us to give very short soundness proofs for dynamic IFC libraries such as faceted values and LIO. Our proofs stay short even when fully mechanized for Agda implementations of the libraries in terms of type abstraction.
- Abstract(参考訳): 我々は、動的IFCライブラリーの鍵となる健全性定理である非干渉と透明性が、型抽象のより一般的なパラメトリック性定理の直接的な結果として「自由」に得られることを示した。
これにより、顔付き値やLOOのような動的IFCライブラリに対して、非常に短い音質証明を行うことができる。
私たちの証明は、型抽象化の観点から、ライブラリのAgda実装を完全に機械化しても、短いままです。
関連論文リスト
- Towards Large Language Models as Copilots for Theorem Proving in Lean [81.94024084598598]
大規模な言語モデルでリーン推論を実行するためのフレームワークであるLean Copilotを紹介します。
証明手順を提案し、中間的な証明目標を完了し、関連する前提を選択するためのツールを構築します。
実験により, 提案手法の有効性を実証し, 提案手法の有効性を検証した。
論文 参考訳(メタデータ) (2024-04-18T22:54:08Z) - AbsInstruct: Eliciting Abstraction Ability from LLMs through Explanation
Tuning with Plausibility Estimation [62.41392852653183]
抽象化能力は人間の知性において不可欠であり、NLP研究における様々なタスクにも有用である。
既存の研究によると、LLMは抽象能力に欠けており、その改善方法はまだ解明されていない。
本稿では,命令チューニングによるLLMの抽象化能力を向上するフレームワークAbsInstructを設計する。
論文 参考訳(メタデータ) (2024-02-16T12:47:11Z) - Leveraging Large Language Models for Automated Proof Synthesis in Rust [6.202137610101939]
大規模言語モデル(LLM)は、コード解析と合成に成功している。
我々は、LLMと静的解析を組み合わせることで、Verusと呼ばれるRustベースの形式検証フレームワークの不変性、アサーション、その他の証明構造を合成する。
プロトタイプでは,検証タスクを複数の小さなタスクに分割し,反復的にGPT-4をクエリし,その出力と軽量な静的解析を組み合わせる。
論文 参考訳(メタデータ) (2023-11-07T05:47:47Z) - LILO: Learning Interpretable Libraries by Compressing and Documenting Code [71.55208585024198]
LILOは、反復的に合成、圧縮、文書化を行う、ニューロシンボリックなフレームワークである。
LILOは、LLM誘導プログラム合成と、Stitchから自動化された最近のアルゴリズムの進歩を組み合わせたものである。
LILOのシンセサイザーが学習した抽象化を解釈し、デプロイするのを手助けすることで、AutoDocがパフォーマンスを向上させることが分かりました。
論文 参考訳(メタデータ) (2023-10-30T17:55:02Z) - LINC: A Neurosymbolic Approach for Logical Reasoning by Combining
Language Models with First-Order Logic Provers [60.009969929857704]
論理的推論は、科学、数学、社会に潜在的影響を与える可能性のある人工知能にとって重要なタスクである。
本研究では、LINCと呼ばれるモジュール型ニューロシンボリックプログラミングのようなタスクを再構成する。
我々は,FOLIOとProofWriterのバランスの取れたサブセットに対して,ほぼすべての実験条件下で,3つの異なるモデルに対して顕著な性能向上を観察した。
論文 参考訳(メタデータ) (2023-10-23T17:58:40Z) - An Extendable Python Implementation of Robust Optimisation Monte Carlo [0.0]
本稿では,PythonパッケージELFIにおけるロバスト最適化モンテカルロ(ROMC)の実装について述べる。
ROMCは、後方から正確な重み付けされたサンプルを提供する、新しくて効率的な(高い並列化が可能な)LFIフレームワークである。
論文 参考訳(メタデータ) (2023-09-19T13:37:47Z) - LeanDojo: Theorem Proving with Retrieval-Augmented Language Models [72.54339382005732]
大規模言語モデル(LLM)は、Leanのような証明アシスタントを使って形式的な定理を証明することを約束している。
既存のメソッドは、プライベートコード、データ、計算要求のために、複製や構築が難しい。
本稿では、ツールキット、データ、モデルからなるオープンソースのリーンツールキットであるLeanDojoを紹介します。
本研究では,LLM ベースの証明器 ReProver を開発した。
論文 参考訳(メタデータ) (2023-06-27T17:05:32Z) - FuzzyLogic.jl: a Flexible Library for Efficient and Productive Fuzzy
Inference [5.584060970507507]
本稿では,ファジィ推論を行うJuliaライブラリであるtextscFuzzyLogic.jlを紹介する。
ライブラリは完全にオープンソースで、パーミッシブライセンスでリリースされている。
論文 参考訳(メタデータ) (2023-06-17T10:43:09Z) - Learning and interpreting asymmetry-labeled DAGs: a case study on
COVID-19 fear [2.3572498744567127]
非対称性ラベル付きDAGは、独立性の対称仮定を緩和することによってベイズネットワークのクラスを拡張することが提案されている。
本稿では,このモデルに対する構造学習アルゴリズムについて紹介する。このアルゴリズムは,効率的ではあるが,基礎となる依存構造を直接解釈することができる。
イタリアで収集されたFear of COVID-19 Scaleのデータを使用した実世界のデータアプリケーションでは、実際に使用されていることが示されている。
論文 参考訳(メタデータ) (2023-01-02T12:48:17Z) - Learning to Prove Theorems by Learning to Generate Theorems [71.46963489866596]
我々は、定理証明器を訓練するために、定理と証明を自動的に合成するニューラルジェネレータを学習する。
実世界の課題に関する実験は、我々の手法による合成データが定理証明器を改善することを示した。
論文 参考訳(メタデータ) (2020-02-17T16:06:02Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。