論文の概要: Whiel: A Neurosymbolic Platform for Certified Relational Program Verification
- arxiv url: http://arxiv.org/abs/2611.05612v2
- Date: Thu, 05 Nov 2026 17:45:04 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-11-07 04:55:13.514679
- Title: Whiel: A Neurosymbolic Platform for Certified Relational Program Verification
- Title（参考訳）: Whiel: 認定リレーショナルプログラム検証のためのニューロシンボリックプラットフォーム
- Abstract要約: 命令型リレーショナルプログラムに関するリーン認証推論のためのWhielシステムを提案する。
このシステムは、Datalogの格納と等価性の問題、否定付き拡張、およびグラフクエリ言語のコアフラグメントをエンコードすることができる。
The Whiel system, we evaluate its performance on a curated benchmark suite。
- 参考スコア（独自算出の注目度）: 13.648225103172274
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: We present the Whiel (a contraction of Whi(le-R)el) system for Lean-certified reasoning about imperative relational programs. The system can encode containment and equivalence problems for Datalog, its extensions with negation, and the core fragment of graph query languages. It can also represent optimized or incremental evaluation algorithms that are not expressible in the original query language, as well as first-order specifications of integrity constraints, schema mappings, and views arising in data integration, exchange, and sharing. Whiel's program states are database instances, and its imperative structure enables compositional Hoare-style reasoning with first-order relational specifications, using prophecy variables and leveled invariants to support inductive arguments. Whiel supports neurosymbolic discovery of loop invariants whose verification conditions can be checked using the Vampire first-order theorem prover. Counterexamples are fed back into the neurosymbolic pipeline, while proposed solutions are translated into Lean proof certificates. To validate the Whiel system, we evaluate its performance on a curated benchmark suite. In summary, we envision the Whiel system as a tool for tackling mathematically demanding, typically undecidable problems involving complex query and constraint languages, with a high degree of trust in its output.
- Abstract（参考訳）: 命令型リレーショナルプログラムに関するリーン認証推論のためのWhiel(Whi(le-R)elの収縮)システムを提案する。
このシステムは、Datalogの格納と等価性の問題、否定付き拡張、およびグラフクエリ言語のコアフラグメントをエンコードすることができる。
また、元のクエリ言語では表現できない最適化またはインクリメンタルな評価アルゴリズムや、データ統合、交換、共有に起因する整合性制約、スキーママッピング、ビューのファーストオーダー仕様を表現できる。
Whielのプログラムステートはデータベースインスタンスであり、その命令構造は一階関係仕様による構成的ホアスタイルの推論を可能にし、予言変数と帰納的引数をサポートするレベル付き不変量を使用する。
ウィエルは、ヴァンパイア一階定理証明器を用いて検証条件を確認することができるループ不変量のニューロシンボリック発見をサポートする。
反例はニューロシンボリックパイプラインに送られ、提案されたソリューションはリーン証明証明書に変換される。
The Whiel system, we evaluate its performance on a curated benchmark suite。
要約すると、Whielシステムは、複雑なクエリや制約言語を含む決定不能な問題に数学的に要求される問題に対処するためのツールであり、その出力を高い信頼度で処理する。
関連論文リスト
- VeriGraph: Towards Verifiable Data-Analytic Agents [71.17693022916896]
LLMをベースとしたエージェントは、データ集約分析タスクにおいて強力な能力を示してきたが、その出力は滅多に検証されていない。
We propose VeriGraph, a traceable neuro-symbolic reasoning framework that agent can construct an explicit heterogeneous evidence directed acyclic graph。
以上の結果から,明示的なエビデンスグラフ構築がデータ分析エージェントの検証に期待できる道のりであることが示唆された。
論文 参考訳（メタデータ） (2026-06-15T11:50:56Z) - Neural Information Causality [0.0]
我々はニューラル情報因果性(Neural-IC)と呼ばれる枠組みを開発する。
本稿では,Neural-ICがクエリリーク,精度リーク,エピソード固有メモリの操作診断であることを示す。
また、1ビットの古典的RACベンチマークも提供し、関連する量子エンハンスメントがボトルネックを超える完全な情報ではないことを示す。
論文 参考訳（メタデータ） (2026-05-10T04:25:11Z) - Multi-Step Semantic Reasoning in Generative Retrieval [50.65947993017158]
生成検索(GR)モデルは、モデルパラメータ内のコーパスを符号化し、所定のクエリに対して関連するドキュメント識別子を生成する。
既存のGRモデルは、財務報告に対するセマンティック推論など、数値的な文脈で複雑なクエリに苦しむ。
GR内の数値文脈における多段階意味推論を強化するためのフレームワークであるReasonGRを提案する。
論文 参考訳（メタデータ） (2026-03-12T18:38:50Z) - Neuro-Symbolic Generation and Validation of Memory-Aware Formal Function Specifications [12.783777562919383]
メモリ操作プログラムの形式的検証は、専門家によって書かれたメモリ状態をキャプチャする正確な機能仕様に依存している。
本稿では,Cプログラムのメモリ対応形式関数仕様を自動生成するニューロシンボリックフレームワークを提案する。
我々は,メモリ対応の形式関数仕様を生成するための200Cプログラミング問題のベンチマークであるLeetCode-C-Specを紹介する。
論文 参考訳（メタデータ） (2026-03-12T15:02:26Z) - OrLog: Resolving Complex Queries with LLMs and Probabilistic Reasoning [51.58235452818926]
そこで我々は,論理的推論から述語レベルの妥当性推定を分離するニューロシンボリック検索フレームワークOrLogを紹介する。
大規模言語モデル (LLM) は1つの復号のない前方通過において原子述語に対する可視性スコアを提供し、確率論的推論エンジンはクエリ満足度の後方確率を導出する。
論文 参考訳（メタデータ） (2026-01-30T15:31:58Z) - CoT-Seg: Rethinking Segmentation with Chain-of-Thought Reasoning and Self-Correction [50.67483317563736]
本稿では,段階的に考察し,必要な情報を検索し,結果を生成し,自己評価を行い,結果を洗練するシステムを提案する。
CoT-Segは、思考の連鎖推論と自己補正を組み合わせることで、推論セグメンテーションを再考する、トレーニング不要のフレームワークである。
論文 参考訳（メタデータ） (2026-01-24T11:41:54Z) - Large Language Models Meet Symbolic Provers for Logical Reasoning Evaluation [24.081573908824353]
一階述語論理(FOL)推論はインテリジェントシステムにおいて重要である。
既存のベンチマークは、広範囲の人間のアノテーションや手作りテンプレートに依存していることが多い。
本稿では,大言語モデルの生成強度を記号型プローサの厳密性と精度で相乗化するProverGenという新しいフレームワークを提案する。
論文 参考訳（メタデータ） (2025-02-10T15:31:54Z) - H-STAR: LLM-driven Hybrid SQL-Text Adaptive Reasoning on Tables [56.73919743039263]
本稿では,2段階のプロセスにシンボル的アプローチと意味的アプローチ(テキスト的アプローチ)を統合し,制約に対処する新しいアルゴリズムを提案する。
実験の結果,H-STARは3つの質問応答(QA)と事実検証データセットにおいて,最先端の手法を大幅に上回っていることがわかった。
論文 参考訳（メタデータ） (2024-06-29T21:24:19Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。