論文の概要: Complete the Cycle: Reachability Types with Expressive Cyclic References (Extended Version)

• arxiv url: http://arxiv.org/abs/2503.07328v3
• Date: Fri, 29 Aug 2025 16:11:35 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-09-01 13:41:09.889473
• Title: Complete the Cycle: Reachability Types with Expressive Cyclic References (Extended Version)
• Title（参考訳）: Complete the Cycle: Expressive Cyclic References (Extended Version) を備えたReachability Types
• Authors: Haotian Deng, Siyuan He, Songlin Jia, Yuyan Bao, Tiark Rompf,
• Abstract要約: Reachability Typesは、高次のプログラムのエイリアスと分離を追跡する。 RTを表現性を高める3つのメカニズムで拡張する。 これらの拡張は$mathsfF_:circ$-calculusで定式化され、型音の機械的な証明である。
• 参考スコア（独自算出の注目度）: 2.9406674433083686
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Local reasoning about programs that combine aliasing and mutable state is a longstanding challenge. Existing approaches -- ownership systems, linear and affine types, uniqueness types, and lexical effect tracking -- impose global restrictions such as uniqueness or linearity, or rely on shallow syntactic analyses. These designs fall short with higher-order functions and shared mutable state. Reachability Types (RT) track aliasing and separation in higher-order programs, ensuring runtime safety and non-interference. However, RT systems face three key limitations: (1) they prohibit cyclic references, ruling out non-terminating computations and fixed-point combinators; (2) they require deep tracking, where a qualifier must include all transitively reachable locations, reducing precision and hindering optimizations like fine-grained parallelism; and (3) referent qualifier invariance prevents referents from escaping their allocation contexts, making reference factories inexpressible. In this work, we address these limitations by extending RT with three mechanisms that enhance expressiveness. First, we introduce cyclic references, enabling recursive patterns to be encoded directly through the store. Second, we adopt shallow qualifier tracking, decoupling references from their transitively reachable values. Finally, we introduce an escaping rule with reference subtyping, allowing referent qualifiers to outlive their allocation context. These extensions are formalized in the $\mathsf{F}_{<:}^{\circ}$-calculus with a mechanized proof of type soundness, and case studies illustrate expressiveness through fixpoint combinators, non-interfering parallelism, and escaping read-only references.
• Abstract（参考訳）: エイリアスとミュータブルな状態を組み合わせたプログラムに関するローカル推論は、長年にわたる課題である。 既存のアプローチ -- オーナシップシステム、線形およびアフィンタイプ、一意性タイプ、語彙効果トラッキング -- は、一意性や線形性といった世界的な制限を課すか、あるいは浅い構文解析に依存する。 これらの設計は高次関数と共有可変状態に欠ける。 Reachability Types (RT)は、高次のプログラムのエイリアスと分離を追跡し、ランタイムの安全性と非干渉を保証する。 しかし、RTシステムは、循環参照を禁止し、非終端計算と固定点コンビネータを除外し、(2)全ての通過可能な場所を含む必要があるディープトラッキングを必要とし、細粒度並列化のような精度と最適化を阻害し、(3)参照修飾器の分散は、参照者が割り当てコンテキストを逃れ、参照ファクトリを表現不能にするのを防ぐ。 本研究では,表現性を高める3つのメカニズムでRTを拡張することで,これらの制約に対処する。 まず、循環参照を導入し、再帰的パターンをストアから直接エンコードできるようにします。 第2に、過渡的に到達可能な値から参照を分離する、浅い等化器追跡を採用する。 最後に、参照サブタイプによるエスケープルールを導入し、参照修飾器がアロケーションコンテキストを超過できるようにする。 これらの拡張は、タイプ音の機械的証明を持つ $\mathsf{F}_{<:}^{\circ}$-calculus で形式化され、ケーススタディでは、固定点コンビネータ、非干渉並列性、読み取り専用参照をエスケープする。

関連論文リスト

• Automated Synthesis of Formally Verified Multi-Abstraction Function Summaries [19.23701821549906]
  本稿では,記号実行,大規模言語モデル(LLM),および相対的最強ポストコンディション(RSP)を生成するための形式検証を組み合わせた新しいフレームワークを提案する。 我々のアプローチは、VST-Aのシンボル的実行を利用して、プログラムの実行パスと状態遷移を正確に追跡する。 生成したRSPから,ドメイン固有言語内で表現される最強の非冗長な条件を自動で合成する。
  論文  参考訳（メタデータ） (2025-06-11T09:33:02Z)
• Respecting Temporal-Causal Consistency: Entity-Event Knowledge Graphs for Retrieval-Augmented Generation [69.45495166424642]
  我々は,物語文書における時間的,因果的,文字的整合性を理解するために,頑健で差別的なQAベンチマークを開発する。 次に、バイナリマッピングでリンクされたエンティティとイベントのサブグラフを分離したまま保持するデュアルグラフフレームワークであるEntity-Event RAG(E2RAG)を紹介します。 ChronoQA全体で、我々のアプローチは最先端の非構造化およびKGベースのRAGベースラインよりも優れており、因果一貫性クエリや文字整合性クエリが顕著である。
  論文  参考訳（メタデータ） (2025-06-06T10:07:21Z)
• Neuro-Symbolic Query Compiler [57.78201019000895]
  本稿では,このギャップを埋めるために,言語文法規則とコンパイラ設計に触発されたニューラルシンボリックなフレームワークQCompilerを提案する。 理論上は、複雑なクエリを形式化するのに最小でも十分なバックス・ナウアー形式(BNF)の文法を$G[q]$で設計する。 葉のサブクエリの原子性は、より正確な文書検索と応答生成を保証し、複雑なクエリに対処するRAGシステムの能力を大幅に改善する。
  論文  参考訳（メタデータ） (2025-05-17T09:36:03Z)
• An Expressive Trace Logic for Recursive Programs [0.36832029288386137]
  本稿では, 2進状態述語, チョップ, 最小不動点に基づく, トレース式上の表現論理について述べる。 プログラムとトレース公式の両方に、直接的なスタイル、完全な構成的、意味論的意味論が備わっている。 我々の結果は、プログラミング構造と論理連結体との対応に光を当てた。
  論文  参考訳（メタデータ） (2024-11-20T08:35:29Z)
• COrAL: Order-Agnostic Language Modeling for Efficient Iterative Refinement [80.18490952057125]
  反復改良は、複雑なタスクにおける大規模言語モデル(LLM)の能力を高める効果的なパラダイムとして登場した。 我々はこれらの課題を克服するために、コンテキストワイズ順序非依存言語モデリング(COrAL)を提案する。 当社のアプローチでは、管理可能なコンテキストウィンドウ内で複数のトークン依存関係をモデル化しています。
  論文  参考訳（メタデータ） (2024-10-12T23:56:19Z)
• Tractable Offline Learning of Regular Decision Processes [50.11277112628193]
  この研究は、正則決定過程(RDP)と呼ばれる非マルコフ環境のクラスにおけるオフライン強化学習(RL)を研究する。 インスは、未来の観測と過去の相互作用からの報酬の未知の依存を実験的に捉えることができる。 多くのアルゴリズムは、まずこの未知の依存関係を自動学習技術を用いて再構築する。
  論文  参考訳（メタデータ） (2024-09-04T14:26:58Z)
• Clap: a Semantic-Preserving Optimizing eDSL for Plonkish Proof Systems [7.469723382577489]
  Plonkishはゼロ知識証明システムを開発するための一般的な回路フォーマットである。 証明系回路フォーマットを備えた最初のRust e非依存のClapを提示する。 クラップは、意味保存のコンパイル問題として、プロンキッシュシステムとその証人生成装置を製造するという問題を提起している。
  論文  参考訳（メタデータ） (2024-05-20T15:31:32Z)
• SymBa: Symbolic Backward Chaining for Structured Natural Language Reasoning [5.893124686141782]
  シンボリック・ソルバとLLMを統合した新しい後方連鎖システムを提案する。 SymBa では、解法が証明過程を制御し、解法が証明を完成させるために新しい情報を必要とする場合にのみ LLM が呼び出される。 完全性を活用して、SymBaは、ベースラインと比較して7つの導出性、リレーショナル、および算術的推論ベンチマークにおいて大幅な改善を達成している。
  論文  参考訳（メタデータ） (2024-02-20T08:27:05Z)
• Transformer-Based Models Are Not Yet Perfect At Learning to Emulate Structural Recursion [14.739369424331478]
  本稿では,プログラミング言語領域における構造的再帰という抽象概念を,シーケンスモデリング問題や学習モデルの振る舞いにうまく結合する汎用フレームワークを提案する。 フレームワークを強力な概念ツールとして、さまざまな設定の下で異なる問題を特定します。
  論文  参考訳（メタデータ） (2024-01-23T18:07:38Z)
• Tractable Bounding of Counterfactual Queries by Knowledge Compilation [51.47174989680976]
  本稿では, パール構造因果モデルにおいて, 因果関係などの部分的特定可能なクエリのバウンダリングの問題について議論する。 最近提案された反復EMスキームは初期化パラメータをサンプリングしてそれらの境界を内部近似する。 シンボルパラメータを実際の値に置き換えた回路構造を,単一のシンボル知識コンパイルによって得られることを示す。
  論文  参考訳（メタデータ） (2023-10-05T07:10:40Z)
• Gated Recurrent Neural Networks with Weighted Time-Delay Feedback [59.125047512495456]
  重み付き時間遅延フィードバック機構を備えた新しいゲートリカレントユニット(GRU)を導入する。 我々は、$tau$-GRUが、最先端のリカレントユニットやゲート型リカレントアーキテクチャよりも早く収束し、より一般化できることを示します。
  論文  参考訳（メタデータ） (2022-12-01T02:26:34Z)
• Differentiable Inference of Temporal Logic Formulas [1.370633147306388]
  信号時相論理式を学習するための最初のリカレントニューラルネットワークアーキテクチャを実演する。 本稿では,式推論法の最初の体系的比較について述べる。
  論文  参考訳（メタデータ） (2022-08-10T16:52:23Z)
• Temporally-Consistent Surface Reconstruction using Metrically-Consistent Atlases [131.50372468579067]
  そこで本稿では,時間変化点雲列から時間一貫性のある面列を復元する手法を提案する。 我々は、再構成された表面をニューラルネットワークによって計算されたアトラスとして表現し、フレーム間の対応性を確立することができる。 当社のアプローチは、いくつかの挑戦的なデータセットにおいて、最先端のものよりも優れています。
  論文  参考訳（メタデータ） (2021-11-12T17:48:25Z)
• Self-Supervised Learning to Prove Equivalence Between Straight-Line Programs via Rewrite Rules [9.1570563482476]
  2つのプログラムは、1つのプログラムをもう1つのプログラムに書き換える、書き換え規則の一連の適用が存在する場合と同値である。 本稿では,プログラムペア間の等価性の証明を生成するために,トランスフォーマーモデルに基づくニューラルネットワークアーキテクチャを提案する。 我々のシステムであるS4Eqは、1万対の等価プログラムをキュレートしたデータセット上で97%の証明成功を達成した。
  論文  参考訳（メタデータ） (2021-09-22T01:37:08Z)
• High-performance symbolic-numerics via multiple dispatch [52.77024349608834]
  Symbolics.jlは拡張可能なシンボルシステムで、動的多重ディスパッチを使用してドメインのニーズに応じて振る舞いを変更する。 実装に依存しないアクションでジェネリックapiを形式化することで、システムに最適化されたデータ構造を遡及的に追加できることを示します。 従来の用語書き換えシンプリファイアと電子グラフベースの用語書き換えシンプリファイアをスワップする機能を実証する。
  論文  参考訳（メタデータ） (2021-05-09T14:22:43Z)
• Pattern-aware Data Augmentation for Query Rewriting in Voice Assistant Systems [10.332550622090718]
  既存のトレーニングペアからパターンを学習し、ラベルの書き換えから書き換え候補を逆に生成し、不十分なQRトレーニングデータを補う拡張フレームワークを提案する。 実験の結果,QRベースラインを十分に訓練し,低リソース領域やローカライズ領域でのQR性能向上に有効である可能性が示された。
  論文  参考訳（メタデータ） (2020-12-21T16:36:32Z)

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

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