論文の概要: SEAL: Symbolic Execution with Separation Logic (Competition Contribution)
- arxiv url: http://arxiv.org/abs/2602.05703v1
- Date: Thu, 05 Feb 2026 14:29:10 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-02-06 18:49:08.971511
- Title: SEAL: Symbolic Execution with Separation Logic (Competition Contribution)
- Title(参考訳): SEAL:分離論理による記号的実行(競合貢献)
- Authors: Tomáš Brablec, Tomáš Dacík, Tomáš Vojnar,
- Abstract要約: SEALは、リンクされたデータ構造を操作するプログラムの検証のための静的アナライザである。
汎用的な分離論理解法であるAstralを用いて、満足度と細かなチェックを行う。
SEALはLinkedListsベースカテゴリの競争結果を達成した。
- 参考スコア(独自算出の注目度): 0.0
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: SEAL is a static analyser for the verification of programs that manipulate unbounded linked data structures. It is based on separation logic to represent abstract memory states and, unlike other separation-logic-based approaches, it employs a general-purpose separation logic solver Astral for satisfiability and entailment checking, which itself is based on translation to SMT. This design results in a modular architecture intended to be easier to extend and to combine with reasoning in other theories. Although still a prototype, SEAL achieved competitive results in the LinkedLists base category and was one of only four analysers capable of verifying programs with unbounded lists. We believe that the tool's extensibility, combined with further development, can lead to significant improvements in future competitions.
- Abstract(参考訳): SEALは、非有界リンクデータ構造を操作するプログラムの検証のための静的解析器である。
これは抽象記憶状態を表す分離論理に基づいており、他の分離論理に基づくアプローチとは異なり、汎用的な分離論理ソルバであるAstralを用いて、SMTへの変換をベースとしている。
この設計はモジュラーアーキテクチャを拡張しやすくし、他の理論の推論と組み合わせることを目的としている。
いまだプロトタイプだが、SEALはLinkedListsのベースカテゴリで競争力を発揮しており、未有のリストを持つプログラムを検証できる唯一の4つのアナライザの1つであった。
我々は,ツールの拡張性とさらなる開発が組み合わさって,将来の競争において大幅な改善をもたらすと考えている。
関連論文リスト
- OrLog: Resolving Complex Queries with LLMs and Probabilistic Reasoning [51.58235452818926]
そこで我々は,論理的推論から述語レベルの妥当性推定を分離するニューロシンボリック検索フレームワークOrLogを紹介する。
大規模言語モデル (LLM) は1つの復号のない前方通過において原子述語に対する可視性スコアを提供し、確率論的推論エンジンはクエリ満足度の後方確率を導出する。
論文 参考訳(メタデータ) (2026-01-30T15:31:58Z) - LSRIF: Logic-Structured Reinforcement Learning for Instruction Following [56.517329105764475]
命令論理を明示的にモデル化するロジック構造化学習フレームワーク LSRIF を提案する。
実験の結果、LSRIFは命令追従と一般的な推論に大きな改善をもたらすことが示された。
論文 参考訳(メタデータ) (2026-01-10T05:11:38Z) - SEAL: Self-Evolving Agentic Learning for Conversational Question Answering over Knowledge Graphs [28.59157823781425]
SEALは、自己進化型エージェント学習に基づく、2段階のセマンティックパーシングフレームワークである。
SEALは、特にマルチホップ推論、比較、集約タスクにおいて、最先端のパフォーマンスを達成する。
その結果, 構造精度と計算効率の両面で有意な向上が認められた。
論文 参考訳(メタデータ) (2025-12-04T14:52:30Z) - Do LLMs Dream of Discrete Algorithms? [0.7646713951724011]
大規模言語モデル(LLM)は、人工知能の風景を急速に変化させてきた。
確率的推論への依存は、厳密な論理的推論を必要とする領域における有効性を制限する。
本稿では,論理ベースの推論モジュールでLLMを増強するニューロシンボリックアプローチを提案する。
論文 参考訳(メタデータ) (2025-06-29T22:03:01Z) - Proof of Thought : Neurosymbolic Program Synthesis allows Robust and Interpretable Reasoning [1.3003982724617653]
大規模言語モデル(LLM)は自然言語処理に革命をもたらしたが、一貫性のない推論に苦戦している。
本研究では,LLM出力の信頼性と透明性を高めるフレームワークであるProof of Thoughtを紹介する。
主な貢献は、論理的整合性を高めるためのソート管理を備えた堅牢な型システム、事実的知識と推論的知識を明確に区別するための規則の明示である。
論文 参考訳(メタデータ) (2024-09-25T18:35:45Z) - Improving Complex Reasoning over Knowledge Graph with Logic-Aware Curriculum Tuning [89.89857766491475]
カリキュラムベースの論理認識型チューニングフレームワークであるLACTを提案する。
具体的には、任意の一階論理クエリをバイナリツリー分解によって拡張する。
広く使われているデータセットに対する実験では、LATは高度な手法よりも大幅に改善(平均+5.5% MRRスコア)し、新しい最先端技術を実現している。
論文 参考訳(メタデータ) (2024-05-02T18:12:08Z) - Modeling Hierarchical Reasoning Chains by Linking Discourse Units and
Key Phrases for Reading Comprehension [80.99865844249106]
本稿では,論理的推論の基盤として,対話レベルと単語レベルの両方の文脈を扱う総合グラフネットワーク(HGN)を提案する。
具体的には、ノードレベルの関係とタイプレベルの関係は、推論過程におけるブリッジと解釈できるが、階層的な相互作用機構によってモデル化される。
論文 参考訳(メタデータ) (2023-06-21T07:34:27Z) - Linear Temporal Logic Modulo Theories over Finite Traces (Extended
Version) [72.38188258853155]
有限トレース(LTLf)上の線形時間論理について検討する。
命題の文字は任意の理論で解釈された一階述語式に置き換えられる。
Satisfiability Modulo Theories (LTLfMT) と呼ばれる結果の論理は半決定可能である。
論文 参考訳(メタデータ) (2022-04-28T17:57:33Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。