論文の概要: A Deductive System for Contract Satisfaction Proofs
- arxiv url: http://arxiv.org/abs/2604.09165v1
- Date: Fri, 10 Apr 2026 09:51:24 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-04-13 17:57:53.809345
- Title: A Deductive System for Contract Satisfaction Proofs
- Title（参考訳）: 契約満足度証明の導出システム
- Authors: Arthur Correnson, Haoyi Zeng, Jana Hofmann,
- Abstract要約: ハードウェア・ソフトウェア契約はCPUの漏洩動作の抽象的な仕様である。
契約満足度は、相対的トレース平等(英語版)と呼ばれるより一般的な問題の例である。
そこで我々は,相対的トレース等価性を示す導出的証明システムを開発した。
- 参考スコア（独自算出の注目度）: 2.1487266204344473
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Hardware-software contracts are abstract specifications of a CPU's leakage behavior. They enable verifying the security of high-level programs against side-channel attacks without having to explicitly reason about the microarchitectural details of the CPU. Using the abstraction powers of a contract requires proving that the targeted CPU satisfies the contract in the sense that the contract over-approximates the CPU's leakage. Besides pen-and-paper reasoning, proving contract satisfaction has been approached mostly from the model-checking perspective, with approaches based on a (semi-)automated search for the necessary invariants. As an alternative, this paper explores how such proofs can be conducted in interactive proof assistants. We start by observing that contract satisfaction is an instance of a more general problem we call relative trace equality, and we introduce relative bisimulation as an associated proof technique. Leveraging recent advances in the field of coinductive proofs, we develop a deductive proof system for relative trace equality. Our system is provably sound and complete, and it enables a modular and incremental proof style. It also features several reasoning principles to simplify proofs by exploiting symmetries and transitivity properties. We formalized our deductive system in the Rocq proof assistant and applied it to two challenging contract satisfaction proofs.
- Abstract（参考訳）: ハードウェア・ソフトウェア契約はCPUの漏洩動作の抽象的な仕様である。
これにより、CPUのマイクロアーキテクチャの詳細を明確に説明することなく、サイドチャネル攻撃に対するハイレベルプログラムのセキュリティを検証することができる。
コントラクトの抽象化能力を使用するには、ターゲットCPUがCPUのリークを過度に近似するという意味で、コントラクトを満たすことを証明する必要がある。
ペンとペーパーの推論の他に、契約満足度を証明することはモデルチェックの観点から主にアプローチされ、必要な不変量の(半)自動探索に基づくアプローチが採用されている。
そこで本研究では,対話型証明アシスタントにおいて,このような証明をどのように行うことができるのかを考察する。
まず、契約満足度が相対的トレース等式と呼ばれるより一般的な問題の例であることを観察し、関連する証明手法として相対的ビシミュレーションを導入する。
コインダクティブ証明の分野における最近の進歩を活用して、相対的トレース等価性を示す導出的証明システムを開発する。
我々のシステムは確実に健全で完全であり、モジュール的でインクリメンタルな証明スタイルを可能にします。
また、対称性と推移性特性を利用して証明を単純化するいくつかの推論原理も特徴である。
提案手法をRocq証明アシスタントで定式化し,2つの挑戦的契約満足度証明に適用した。
関連論文リスト
- When Agda met Vampire [3.373200015661363]
本研究の目的は,証明アシスタントと自動定理証明器(ATP)を簡単な方法で統合することである。
ほとんどのATPは古典的な一階述語論理で作用するが、これらの証明アシスタントは構成的依存型理論に基づいている。
我々は、ATPヴァンパイアに対するAgda証明義務のプロトタイプシステムを作成し、その結果得られた古典的証明をAgdaが型チェックできる構成的証明項に変換する。
論文 参考訳（メタデータ） (2026-02-21T14:19:56Z) - Witnessd: Proof-of-process via Adversarial Collapse [0.0]
我々は、暗号の完全性とプロセスの証明とのギャップに対処する。
本稿では,物理プロセスが単なる署名キーではなく,デジタルアーティファクトを生み出したことを示す,原始的なカテゴリであるProcess-of-Processを紹介した。
Wetnessdは、ジッタシールと検証遅延関数、外部タイムスタンプアンカー、デュアルソースキーストローク検証を組み合わせたアーキテクチャである。
論文 参考訳（メタデータ） (2026-02-02T05:30:21Z) - Agentic Program Verification [14.684859166069012]
本稿では,プログラム検証を行うための最初の大規模言語モデルエージェントであるAutoRocqを提案する。
LLMの広範な訓練を実証例に頼っている過去の研究とは異なり、我々のエージェントはオンザフライで学習し、反復的な改善ループを通じて証明を改善する。
このようにして、我々の証明構成は証明エージェントと定理証明器との間の自律的な協調を含む。
論文 参考訳（メタデータ） (2025-11-21T15:51:48Z) - What's in a Proof? Analyzing Expert Proof-Writing Processes in F* and Verus [2.8003002159083237]
我々は,2つの言語で作業する8人の専門家から,詳細なソースコードテレメトリの収集と解析を行うユーザスタディを実施している。
その結果、専門家が証明開発プロセスで遭遇した重要な課題や証明についてどのように考えるかについて興味深い傾向とパターンが明らかになった。
我々はこれらの知見を,AI証明アシスタントのための具体的な設計指針に翻訳する。
論文 参考訳（メタデータ） (2025-08-01T22:16:30Z) - Safe: Enhancing Mathematical Reasoning in Large Language Models via Retrospective Step-aware Formal Verification [56.218970738892764]
Chain-of-Thoughtプロンプトは、大規模言語モデル(LLM)から推論能力を引き出すデファクトメソッドとなっている。
検出が極めて難しいCoTの幻覚を緩和するために、現在の方法は不透明なボックスとして機能し、彼らの判断に対する確認可能な証拠を提供しておらず、おそらくその効果を制限する。
任意のスコアを割り当てるのではなく、各推論ステップで形式数学言語Lean 4で数学的主張を明確にし、幻覚を識別するための公式な証明を提供しようとしている。
論文 参考訳（メタデータ） (2025-06-05T03:16:08Z) - LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction [74.79306773878955]
証明の進捗を予測する手法であるLeanProgressを紹介します。
実験の結果、LeanProgressは全体の予測精度が75.1%に達することがわかった。
論文 参考訳（メタデータ） (2025-02-25T07:46:36Z) - Neuro-Symbolic Integration Brings Causal and Reliable Reasoning Proofs [95.07757789781213]
LLMの複雑な推論には2行のアプローチが採用されている。
1行の作業は様々な推論構造を持つLLMを誘導し、構造出力は自然に中間推論ステップと見なすことができる。
他方の行では、LCMのない宣言的解法を用いて推論処理を行い、推論精度は向上するが、解法のブラックボックスの性質により解釈性に欠ける。
具体的には,Prologインタプリタが生成した中間検索ログにアクセスし,人間可読推論に解釈可能であることを示す。
論文 参考訳（メタデータ） (2023-11-16T11:26:21Z) - Generating Natural Language Proofs with Verifier-Guided Search [74.9614610172561]
NLProofS (Natural Language Proof Search) を提案する。
NLProofSは仮説に基づいて関連するステップを生成することを学習する。
EntailmentBank と RuleTaker の最先端のパフォーマンスを実現している。
論文 参考訳（メタデータ） (2022-05-25T02:22:30Z) - Prove-It: A Proof Assistant for Organizing and Verifying General
Mathematical Knowledge [0.0]
Prove-ItはPythonベースの汎用的対話型定理証明アシスタントである。
Prove-ItはフレキシブルなJupyterノートブックベースのユーザーインターフェイスを使って、対話や証明の手順を文書化している。
現在の開発と今後の研究には、量子回路操作と量子アルゴリズム検証への有望な応用が含まれている。
論文 参考訳（メタデータ） (2020-12-20T18:15:12Z) - PRover: Proof Generation for Interpretable Reasoning over Rules [81.40404921232192]
本稿では,ルールベース上の二項質問に応答し,対応する証明を生成するトランスフォーマーモデルを提案する。
本モデルは,効率的な制約付き学習パラダイムを用いて,証明グラフに対応するノードやエッジを予測できることを学習する。
我々は、QAと証明生成のための有望な結果を示すために、合成、手書き、人文による規則ベースの実験を行う。
論文 参考訳（メタデータ） (2020-10-06T15:47:53Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。