論文の概要: 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実装を完全に機械化しても、短いままです。

関連論文リスト

• Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
  この研究は、記号的突然変異を通じて形式的な定理を構成するデータ合成のフレームワークであるAlchemyを提案する。 マドリブにおける各候補定理について、書き直しや適用に使用できるすべてのイベーシブルな定理を同定する。 その結果、マドリブの定理の数は110kから6Mへと桁違いに増加する。
  論文  参考訳（メタデータ） (2024-10-21T08:04:21Z)
• Efficient and Universal Merkle Tree Inclusion Proofs via OR Aggregation [27.541105686358378]
  本稿では,メルクル木包摂証明のためのOR論理に基づく新しい証明集約手法を提案する。 木内の葉の数に依存しない証明サイズを実現し、有効な葉のハッシュ1つを用いて検証を行う。 提案手法は,ゼロ知識証明システムのスケーラビリティ,効率,柔軟性を著しく向上させる可能性がある。
  論文  参考訳（メタデータ） (2024-05-13T17:15:38Z)
• ATG: Benchmarking Automated Theorem Generation for Generative Language Models [83.93978859348313]
  人間はより広範に複雑な数学的結果を探求するために新しい定理を開発することができる。 現在の生成言語モデル(LM)は、定理の自動証明において著しく改善されている。 本稿では,エージェントが価値ある(あるいは新しい)定理を自動生成できるかどうかを評価する自動定理生成ベンチマークを提案する。
  論文  参考訳（メタデータ） (2024-05-05T02:06:37Z)
• Towards Large Language Models as Copilots for Theorem Proving in Lean [81.94024084598598]
  大規模な言語モデルでリーン推論を実行するためのフレームワークであるLean Copilotを紹介します。 証明手順を提案し、中間的な証明目標を完了し、関連する前提を選択するためのツールを構築します。 実験により, 提案手法の有効性を実証し, 提案手法の有効性を検証した。
  論文  参考訳（メタデータ） (2024-04-18T22:54:08Z)
• 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)
• 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)

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

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