論文の概要: Quantified Linear and Polynomial Arithmetic Satisfiability via Template-based Skolemization
- arxiv url: http://arxiv.org/abs/2412.16226v1
- Date: Wed, 18 Dec 2024 14:37:15 GMT
- ステータス: 翻訳完了
- システム内更新日: 2024-12-24 15:56:58.860219
- Title: Quantified Linear and Polynomial Arithmetic Satisfiability via Template-based Skolemization
- Title（参考訳）: テンプレートベースのスコレマイゼーションによる線形・多項算術的満足度の定量化
- Authors: Krishnendu Chatterjee, Ehsan Kafshdar Goharshady, Mehrdad Karrabi, Harshit J Motwani, Maximilian Seeliger, Đorđe Žikelić,
- Abstract要約: 既存の手法の主なボトルネックは計算コストのかかる定量化器の除去ステップである。
テンプレートに基づく Skolemization 手法を提案し,線形/ポリノミカルな Skolem 関数を自動的に合成し,式中の量化子を除去する。
提案手法は, 高性能な実用性能と相まって, 魅力的な理論特性を提供する。
- 参考スコア（独自算出の注目度）: 4.2518927441106
- License:
- Abstract: The problem of checking satisfiability of linear real arithmetic (LRA) and non-linear real arithmetic (NRA) formulas has broad applications, in particular, they are at the heart of logic-related applications such as logic for artificial intelligence, program analysis, etc. While there has been much work on checking satisfiability of unquantified LRA and NRA formulas, the problem of checking satisfiability of quantified LRA and NRA formulas remains a significant challenge. The main bottleneck in the existing methods is a computationally expensive quantifier elimination step. In this work, we propose a novel method for efficient quantifier elimination in quantified LRA and NRA formulas. We propose a template-based Skolemization approach, where we automatically synthesize linear/polynomial Skolem functions in order to eliminate quantifiers in the formula. The key technical ingredients in our approach are Positivstellens\"atze theorems from algebraic geometry, which allow for an efficient manipulation of polynomial inequalities. Our method offers a range of appealing theoretical properties combined with a strong practical performance. On the theory side, our method is sound, semi-complete, and runs in subexponential time and polynomial space, as opposed to existing sound and complete quantifier elimination methods that run in doubly-exponential time and at least exponential space. On the practical side, our experiments show superior performance compared to state-of-the-art SMT solvers in terms of the number of solved instances and runtime, both on LRA and on NRA benchmarks.
- Abstract（参考訳）: 線形実数算術(LRA)と非線形実数算術(NRA)の整合性をチェックする問題は広く応用されており、特に人工知能の論理やプログラム解析などの論理関連応用の中心にある。
定量化 LRA と NRA の公式の満足度チェックには多くの研究がなされているが、定量化 LRA と NRA の公式の満足度チェックの問題は依然として大きな課題である。
既存の手法の主なボトルネックは計算コストのかかる定量化器の除去ステップである。
本研究では,LRAおよびNRAの量子化式における効率的な定量化器の除去法を提案する。
我々はテンプレートベースのSkolemizationアプローチを提案し、線形/多項式のSkolem関数を自動で合成し、式中の量化子を除去する。
このアプローチにおける重要な技術的要素は、多項式の不等式を効率的に操作できる代数幾何学からのPositivstellens\"atze定理である。
提案手法は, 高性能な実用性能と相まって, 魅力的な理論特性を提供する。
理論面では,本手法は半完全であり,2倍の時間と少なくとも指数空間で動作する既存の音響および完全量化器除去法とは対照的に,部分指数時間と多項式空間で動作する。
実用面では、LRAおよびNRAベンチマークの両方において、解決されたインスタンス数とランタイム数の観点から、最先端のSMTソルバと比較して優れた性能を示す。
関連論文リスト
- Synthesizing Efficiently Monitorable Formulas in Metric Temporal Logic [4.60607942851373]
システム実行から形式仕様を自動合成する問題を考察する。
時間論理式を合成するための古典的なアプローチの多くは、公式のサイズを最小化することを目的としている。
我々は,この概念を定式化し,有界な外見を持つ簡潔な公式を合成する学習アルゴリズムを考案する。
論文 参考訳（メタデータ） (2023-10-26T14:13:15Z) - Learning to Optimize with Stochastic Dominance Constraints [103.26714928625582]
本稿では,不確実量を比較する問題に対して,単純かつ効率的なアプローチを開発する。
我々はラグランジアンの内部最適化をサロゲート近似の学習問題として再考した。
提案したライト-SDは、ファイナンスからサプライチェーン管理に至るまで、いくつかの代表的な問題において優れた性能を示す。
論文 参考訳（メタデータ） (2022-11-14T21:54:31Z) - Asymptotically Unbiased Instance-wise Regularized Partial AUC
Optimization: Theory and Algorithm [101.44676036551537]
One-way partial AUC (OPAUC) と Two-way partial AUC (TPAUC) はバイナリ分類器の平均性能を測定する。
既存の手法のほとんどはPAUCをほぼ最適化するしかなく、制御不能なバイアスにつながる。
本稿では,分散ロバスト最適化AUCによるPAUC問題の簡易化について述べる。
論文 参考訳（メタデータ） (2022-10-08T08:26:22Z) - Exploring Viable Algorithmic Options for Learning from Demonstration
(LfD): A Parameterized Complexity Approach [0.0]
本稿では,パラメータ化複雑性解析を用いて,アルゴリズムの選択肢を体系的に探索する方法を示す。
環境、実演、ポリシーに対する多くの(しばしば同時に)制限に対して、我々の問題は、一般的にも、あるいは相対的に、効率的に解決できないことを示す。
論文 参考訳（メタデータ） (2022-05-10T15:54:06Z) - Linear Temporal Logic Modulo Theories over Finite Traces (Extended
Version) [72.38188258853155]
有限トレース(LTLf)上の線形時間論理について検討する。
命題の文字は任意の理論で解釈された一階述語式に置き換えられる。
Satisfiability Modulo Theories (LTLfMT) と呼ばれる結果の論理は半決定可能である。
論文 参考訳（メタデータ） (2022-04-28T17:57:33Z) - Scalable Anytime Algorithms for Learning Formulas in Linear Temporal
Logic [2.631744051718347]
トレースを分類する公式を学習する際の問題点を考察する。
既存の解には2つの制限がある: それらは小さな公式を超えてスケールせず、結果を返すことなく計算資源を消費する。
我々は,両問題に対処する新しいアルゴリズムを導入する。我々のアルゴリズムは,従来よりも桁違いに大きい式を構築でき,いつでも可能である。
論文 参考訳（メタデータ） (2021-10-13T13:57:31Z) - Learning Implicitly with Noisy Data in Linear Arithmetic [94.66549436482306]
PAC-セマンティックスにおける暗黙学習を拡張し、線形算術の言語における間隔としきい値の不確実性を扱う。
最適線形プログラミング対象制約の学習に対する我々の暗黙的アプローチは、実際的な明示的アプローチよりも著しく優れていることを示す。
論文 参考訳（メタデータ） (2020-10-23T19:08:46Z) - Explaining Multi-stage Tasks by Learning Temporal Logic Formulas from
Suboptimal Demonstrations [6.950510860295866]
本稿では,一貫した線形時間論理式(LTL)の論理構造と原子命題を学習し,実演から多段階タスクを学習する手法を提案する。
学習者は、その式を満足しながらコスト関数を最適化し、学習者にはコスト関数が不確実な場合において、成功しているが潜在的に最適でないデモンストレーションが与えられる。
提案アルゴリズムでは,デモのKKT(Karush-Kuhn-Tucker)最適条件と反例誘導ファルシフィケーション戦略を用いて,原子命題パラメータを学習する。
論文 参考訳（メタデータ） (2020-06-03T17:40:14Z) - Formal Synthesis of Lyapunov Neural Networks [61.79595926825511]
本稿では,リアプノフ関数の自動合成法を提案する。
我々は,数値学習者と記号検証器が相互作用して,確実に正しいリアプノフニューラルネットワークを構築する,反例誘導方式を採用する。
提案手法は,Lyapunov関数を他の手法よりも高速かつ広い空間領域で合成する。
論文 参考訳（メタデータ） (2020-03-19T17:21:02Z) - Learning Interpretable Models in the Property Specification Language [6.875312133832079]
IEEE標準時相論理PSLにおける公式の学習アルゴリズムを開発した。
私たちの研究は、n番目の点ごとに起こる事象のような多くの自然の性質が、言葉で表現できないという事実に動機づけられている。
論文 参考訳（メタデータ） (2020-02-10T11:42:50Z) - Certified Reinforcement Learning with Logic Guidance [78.2286146954051]
線形時間論理(LTL)を用いて未知の連続状態/動作マルコフ決定過程(MDP)のゴールを定式化できるモデルフリーなRLアルゴリズムを提案する。
このアルゴリズムは、トレースが仕様を最大確率で満たす制御ポリシーを合成することが保証される。
論文 参考訳（メタデータ） (2019-02-02T20:09:32Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。