論文の概要: Stellis: A Strategy Language for Purifying Separation Logic Entailments

• arxiv url: http://arxiv.org/abs/2512.05159v1
• Date: Thu, 04 Dec 2025 09:58:03 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-12-13 22:40:56.766102
• Title: Stellis: A Strategy Language for Purifying Separation Logic Entailments
• Title（参考訳）: Stellis: 分離ロジックの細分化のための戦略言語
• Authors: Zhiyi Wang, Xiwei Wu, Yi Fang, Chengtao Li, Hongyi Zhong, Lihan Xie, Qinxiang Cao, Zhenjiang Hu,
• Abstract要約: Stellisは分離ロジックをパーブリケートするためのストラテジー言語である。 提案手法では,各戦略に対して音質条件を生成するアルゴリズムを導入し,各戦略の音質条件の正しさを低減させる。 我々は,標準リンクデータ構造の検証から収集した229項目のベンチマークを用いて,本システムの評価を行った。
• 参考スコア（独自算出の注目度）: 11.604146209618728
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Automatically proving separation logic entailments is a fundamental challenge in verification. While rule-based methods rely on separation logic rules (lemmas) for automation, these rule statements are insufficient for describing automation strategies, which usually involve the alignment and elimination of corresponding memory layouts in specific scenarios. To overcome this limitation, we propose Stellis, a strategy language for purifying separation logic entailments, i.e., removing all spatial formulas to reduce the entailment to a simpler pure entailment. Stellis features a powerful matching mechanism and a flexible action description, enabling the straightforward encoding of a wide range of strategies. To ensure strategy soundness, we introduce an algorithm that generates a soundness condition for each strategy, thereby reducing the soundness of each strategy to the correctness of its soundness condition. Furthermore, based on a mechanized reduction soundness theorem, our prototype implementation generates correctness proofs for the overall automation. We evaluate our system on a benchmark of 229 entailments collected from verification of standard linked data structures and the memory module of a microkernel, and the evaluation results demonstrate that, with such flexibility and convenience provided, our system is also highly effective, which automatically purifies 95.6% (219 out of 229) of the entailments using 5 libraries with 98 strategies.
• Abstract（参考訳）: 分離論理を自動証明することは、検証の根本的な課題である。 ルールベースのメソッドは自動化のための分離ロジックルール(レムマ)に依存しているが、これらのルールステートメントは自動化戦略を記述するには不十分であり、通常は特定のシナリオにおける対応するメモリレイアウトのアライメントと排除を含む。 この制限を克服するために、分離論理の包含を浄化する戦略言語であるStellisを提案する。 Stellisは強力なマッチング機構とフレキシブルなアクション記述を備えており、幅広い戦略の素直なエンコーディングを可能にしている。 戦略の健全性を確保するため,各戦略の音質条件を生成するアルゴリズムを導入し,各戦略の音質条件の正しさを低減した。 さらに, メカニズドリダクションの音響性定理に基づいて, 試作機は, 全体自動化のための正当性証明を生成する。 我々は,標準リンクデータ構造とマイクロカーネルのメモリモジュールの検証から収集した229個のエンタテインメントをベンチマークで評価し,その柔軟性と利便性を両立させて,98の戦略を持つ5つのライブラリを用いて,そのエンタテインメントの95.6%(229点中219点)を自動的に浄化する。

関連論文リスト

• The Active and Noise-Tolerant Strategic Perceptron [18.37713639105532]
  我々は,Active Perceptronアルゴリズムの修正版[DKM05,YZ17]が,$tildeO(d ln frac1)$ラベルクエリのみを使用して過剰なエラーを$$とすることを示す。 このアルゴリズムは計算的に効率的であり、これらの分布的な仮定の下では、戦略パーセプトロンの以前の研究よりもラベルクエリがかなり少ない。
  論文  参考訳（メタデータ） (2025-12-01T15:23:03Z)
• Experience-Guided Adaptation of Inference-Time Reasoning Strategies [49.954515048847874]
  Experience-Guided Reasoner (EGuR) は蓄積された経験に基づいて推論時に調整された戦略を生成する。 EGuRは最強のベースラインに対して最大14%の精度向上を実現し、計算コストを最大111倍に削減する。
  論文  参考訳（メタデータ） (2025-11-14T17:45:28Z)
• Winning the Pruning Gamble: A Unified Approach to Joint Sample and Token Pruning for Efficient Supervised Fine-Tuning [71.30276778807068]
  サンプルプルーニングとトークンプルーニングを戦略的に協調する統合フレームワークを提案する。 Q-Tuningは、トレーニングデータの12.5%しか使用せず、全データSFTベースラインに対する平均38%の改善を実現している。
  論文  参考訳（メタデータ） (2025-09-28T13:27:38Z)
• HAFLQ: Heterogeneous Adaptive Federated LoRA Fine-tuned LLM with Quantization [55.972018549438964]
  LLM(Federated Fine-tuning of Pre-trained Large Language Models)は、さまざまなデータセットにまたがるタスク固有の適応を可能にすると同時に、プライバシの保護を可能にする。 本研究では, HAFLQ (Heterogeneous Adaptive Federated Low-Rank Adaptation Fine-tuned LLM with Quantization) を提案する。 テキスト分類タスクの実験結果から,HAFLQはメモリ使用量を31%削減し,通信コストを49%削減し,精度を50%向上し,ベースライン法よりも高速な収束を実現している。
  論文  参考訳（メタデータ） (2024-11-10T19:59:54Z)
• Bisimulation Learning [55.859538562698496]
  我々は、大きな、潜在的に無限の状態空間を持つ状態遷移系の有限バイシミュレートを計算する。 提案手法は,実際に行われている他の最先端ツールよりも高速な検証結果が得られる。
  論文  参考訳（メタデータ） (2024-05-24T17:11:27Z)
• Large-scale Fully-Unsupervised Re-Identification [78.47108158030213]
  大規模未ラベルデータから学ぶための2つの戦略を提案する。 第1の戦略は、近傍関係に違反することなく、それぞれのデータセットサイズを減らすために、局所的な近傍サンプリングを行う。 第2の戦略は、低時間上限の複雑さを持ち、メモリの複雑さを O(n2) から O(kn) に k n で還元する新しい再帰的手法を利用する。
  論文  参考訳（メタデータ） (2023-07-26T16:19:19Z)
• Symbolic Regression by Exhaustive Search: Reducing the Search Space Using Syntactical Constraints and Efficient Semantic Structure Deduplication [2.055204980188575]
  シンボリック回帰は、モデル構造に関する事前の知識が得られない産業シナリオにおいて、強力なシステム識別技術である。 この章では、これらの問題に対処するために特別に設計された決定論的シンボリック回帰アルゴリズムを紹介します。 全ての可能なモデルの有限列挙は、構造的制約と意味論的に等価な解を検出するキャッシング機構によって保証される。
  論文  参考訳（メタデータ） (2021-09-28T17:47:51Z)
• Refining Labelled Systems for Modal and Constructive Logics with Applications [0.0]
  この論文は、モーダル論理や構成論理のセマンティクスを「経済的な」証明システムに変換する手段として機能する。 精製法は、ラベル付きおよびネストされたシーケント計算の2つの証明理論パラダイムを結合する。 導入された洗練されたラベル付き電卓は、デオン性STIT論理に対する最初の証明探索アルゴリズムを提供するために使用される。
  論文  参考訳（メタデータ） (2021-07-30T08:27:15Z)
• Learning explanations that are hard to vary [75.30552491694066]
  例を越えた平均化は、異なる戦略を縫合する記憶とパッチワークのソリューションに有利であることを示す。 そこで我々は論理ANDに基づく単純な代替アルゴリズムを提案し,実験的に検証する。
  論文  参考訳（メタデータ） (2020-09-01T10:17:48Z)

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

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