Fugu-MT 論文翻訳(概要): Kairos: Generating Tick-Indexed Proof Obligations for Synchronous Temporal Contracts

論文の概要: Kairos: Generating Tick-Indexed Proof Obligations for Synchronous Temporal Contracts

arxiv url: http://arxiv.org/abs/2607.23178v1
Date: Sat, 25 Jul 2026 12:19:22 GMT
ステータス: 翻訳完了
システム内更新日: 2026-07-28 22:34:15.00796
Title: Kairos: Generating Tick-Indexed Proof Obligations for Synchronous Temporal Contracts
Title（参考訳）: Kairos氏: 同期時間契約のためのニッチインジケート証明書の作成
Abstract要約: Kairosは、同期プログラムとソースレベルの時間的安全契約から義務を生成するツールチェーンのプロトタイプである。基礎となる原則を形式化し、リアクティブなコントラクトの正しさを証明します。
参考スコア（独自算出の注目度）: 0.0
License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
Abstract: Requirements for synchronous programs relate observations across ticks, while general-purpose deductive backends use first-order conditions on local steps. Kairos is a prototype toolchain generating such obligations from synchronous programs and source-level temporal safety contracts in assume-guarantee form. Using the standard automata-theoretic reduction, it translates their linear temporal logic (LTL) formulas into bad-state automata, forms their product with the program, and derives tick-indexed Why3 obligations. We formalize the underlying principles and prove reactive contract correctness: under the stated program and automaton hypotheses, every input trace satisfying the environment assumptions induces a unique execution satisfying the temporal guarantees. The definitions, obligation construction, and proof are mechanized in Rocq. A medical infusion controller illustrates the workflow.
Abstract（参考訳）: 同期プログラムの要件は、ジャガイモ間の観測に関係し、汎用的推論バックエンドは、局所的なステップで一階条件を使用する。 Kairosは,同期プログラムやソースレベルの時間的安全契約を前提保証形式で生成するツールチェーンのプロトタイプだ。標準的なオートマトン理論の還元を用いて、それらの線形時間論理式(LTL)を悪い状態のオートマトンに変換し、プログラムで製品を作り、くすぐったWhy3の義務を導出する。プログラムと自動仮説の下で、環境仮定を満たす全ての入力トレースは、時間的保証を満たすユニークな実行を誘導する。定義、義務の構成、証明はRocqで機械化されている。医療用注入コントローラがワークフローを図示します。

関連論文リスト

GenOS: Compositional Certificates for Semantic Robustness in AI Code Generation [0.0]
GenOSはプロンプト、コントラクト、ジェネレータ、プログラムを置き換える確率論的操作意味論である。等価性に適合するカーネルは商類に従属し、商化の可換性は分布拡大や逐次合成と一致することを証明する。また,音の検証,全変量非拡張性,付加的境界の下でのワークフロー・バイコミットの安全性を確立した。
論文参考訳（メタデータ） (2026-08-04T12:42:11Z)
Guarded Equivalence Predicates for Scalable Formal Hardware Information-Flow Verification [0.0]
自己構成は、情報フロー検証を2つの回路コピー上の安全性チェックに還元する。近年のPDRに基づく手法では、複写対称性と大域的クロスコピー等価式を用いて、この重複構造を利用する。我々はこれらの関係をPDRに公開するために、ガード付き等価述語を導入する。
論文参考訳（メタデータ） (2026-06-20T14:25:13Z)
VASO: Formally Verifiable Self-Evolving Skills for Physical AI Agents [57.240036084348354]
本稿では,ロボットスキルコントラクトの検証誘導自己進化のためのフレームワークであるVASOを紹介する。 VASOは論理的に一貫性のないスキル契約を検証し、グローバルおよびローカルな時間的仕様に対してスキルによって誘発される計画を検証する。 Clearpath Jackal と PX4 のクアッドコプタータスクでは、VASO は100点未満の最適化サンプルを使用して97.2% の形式的な仕様準拠に達した。
論文参考訳（メタデータ） (2026-06-03T20:02:35Z)
Dance Across Shifts: Forward-Facilitation Continual Test-Time Adaptation through Dynamic Style Bridging [65.11234199720428]
継続的テスト時間適応(Continuous Test-Time Adaptation)は、デプロイメント後に発生する動的分散シフトを処理するために、知覚システムを強化することを目的としている。動的スタイルブリッジと呼ばれる手法により,新しいフォワードファシリケーションパラダイムを導入する。テスト期間中に、固有の生成バイアスを緩和し、これらのプロキシを入力データに適用するために、マルチレベルブリッジ機構を提案する。
論文参考訳（メタデータ） (2026-05-18T16:18:17Z)
LatticeBridge: Rare-Event Sequential Inference for Faithful Structured Sequence Synthesis [0.5729426778193398]
構造的シーケンス生成は、1つの出力で複数の入力由来の制約を満たすためにモデルを必要とすることが多い。 LatticeBridgeは、コンパクトなプレフィックス言語モデル、インスタンスコンパイルされたサーフェスオートマトン、およびねじれたシーケンシャルなモンテカルロデコーダを組み合わせる。 LatticeBridgeは正確なアンカー満足度と平均アンカーカバレッジを向上させる。
論文参考訳（メタデータ） (2026-04-22T09:24:25Z)
SEVerA: Verified Synthesis of Self-Evolving Agents [12.9624447364193]
自己進化型エージェントフレームワークは、安全性や正確性の正式な保証を提供しない。エージェントコード生成を制約付き学習問題として定式化し、ハードな形式仕様とソフトな目的とを組み合わせてタスクユーティリティをキャプチャする。探索はFGGMコールを含む候補パラメトリックプログラムを合成し、検証は全てのパラメータ値に対する厳しい制約に関して正当性を証明し、制約のない学習に還元する。
論文参考訳（メタデータ） (2026-03-26T07:32:20Z)
Stochastic Clock Attention for Aligning Continuous and Ordered Sequences [1.2418532541734193]
我々はアライメントモデルとして機能する連続および順序列に対する注意機構を定式化する。 Transformerのテキスト音声テストベッドでは、この構造により、より安定したアライメントが得られ、グローバルな時間スケーリングに対する堅牢性が向上する。
論文参考訳（メタデータ） (2025-09-18T07:18:34Z)
Conformal Generative Modeling with Improved Sample Efficiency through Sequential Greedy Filtering [55.15192437680943]
生成モデルは出力に対する厳密な統計的保証を欠いている。厳密な統計的保証を満たす予測セットを生成する逐次共形予測法を提案する。このことは、高い確率で予測セットが少なくとも1つの許容可能な(または有効な)例を含むことを保証している。
論文参考訳（メタデータ） (2024-10-02T15:26:52Z)
Non-autoregressive Sequence-to-Sequence Vision-Language Models [59.445765313094434]
本稿では,デコーダ内の複数の推論経路をマージする並列デコードシーケンス・ツー・シーケンス・ビジョン言語モデルを提案する。このモデルは最先端の自己回帰モデルと同等のパフォーマンスを実現するが、推論時間では高速である。
論文参考訳（メタデータ） (2024-03-04T17:34:59Z)
Self-Infilling Code Generation [60.12883980846781]
自動回帰デコードにインフィル操作を組み込んだ汎用フレームワークであるセルフインフィルコード生成を導入する。我々は,従来の復号化において,新しい割り込みとループ機構を導入するために,この機能を利用する。提案する復号処理は,複数のコード生成ベンチマークにおける正規性と品質の向上に有効である。
論文参考訳（メタデータ） (2023-11-29T16:02:06Z)
Conditional Hybrid GAN for Sequence Generation [56.67961004064029]
本稿では,この問題を解決するための条件付きハイブリッドGAN(C-Hybrid-GAN)を提案する。我々はGumbel-Softmax法を利用して離散値列の分布を近似する。提案したC-Hybrid-GANは、文脈条件付き離散値シーケンス生成において既存の手法よりも優れていることを示す。
論文参考訳（メタデータ） (2020-09-18T03:52:55Z)

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