論文の概要: Revisiting Variable Ordering for Real Quantifier Elimination using
Machine Learning
- arxiv url: http://arxiv.org/abs/2302.14038v1
- Date: Mon, 27 Feb 2023 18:48:33 GMT
- ステータス: 処理完了
- システム内更新日: 2023-02-28 14:25:48.597907
- Title: Revisiting Variable Ordering for Real Quantifier Elimination using
Machine Learning
- Title(参考訳): 機械学習を用いた実数量化器除去のための変数順序の再検討
- Authors: John Hester, Briland Hitaj, Grant Passmore, Sam Owre, Natarajan
Shankar, Eric Yeh
- Abstract要約: 我々は、バイアスを取り除くように設計された41K以上のMetiTarski課題を含む新しいデータセットを作成するために対称性を適用した。
情報漏洩の問題を評価し、新しいデータセット上でモデルの一般化可能性をテストする。
- 参考スコア(独自算出の注目度): 0.7388859384645262
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Cylindrical Algebraic Decomposition (CAD) is a key proof technique for formal
verification of cyber-physical systems. CAD is computationally expensive, with
worst-case doubly-exponential complexity. Selecting an optimal variable
ordering is paramount to efficient use of CAD. Prior work has demonstrated that
machine learning can be useful in determining efficient variable orderings.
Much of this work has been driven by CAD problems extracted from applications
of the MetiTarski theorem prover. In this paper, we revisit this prior work and
consider issues of bias in existing training and test data. We observe that the
classical MetiTarski benchmarks are heavily biased towards particular variable
orderings. To address this, we apply symmetries to create a new dataset
containing more than 41K MetiTarski challenges designed to remove bias.
Furthermore, we evaluate issues of information leakage, and test the
generalizability of our models on the new dataset.
- Abstract(参考訳): Cylindrical Algebraic Decomposition (CAD)は、サイバー物理システムの正式な検証のための重要な証明手法である。
cadは計算コストが高く、最悪の場合2倍の複雑さがある。
最適な変数順序付けを選択することはCADの効率的な利用にとって最重要である。
先行研究は、機械学習が効率的な変数順序を決定するのに役立つことを証明した。
この研究の多くは、MetiTarski定理証明の応用から抽出されたCAD問題によって進められている。
本稿では,この先行研究を再検討し,既存のトレーニングおよびテストデータにおけるバイアスの問題について考察する。
古典的なMetiTarskiベンチマークは、特定の変数順序に大きく偏っている。
これを解決するために、対称性を適用して、バイアスを取り除くように設計された41K以上のMetiTarski課題を含む新しいデータセットを作成します。
さらに,情報漏洩の問題を評価し,新しいデータセット上でモデルの一般化可能性をテストする。
関連論文リスト
- Lessons on Datasets and Paradigms in Machine Learning for Symbolic
Computation: A Case Study on CAD [0.0]
本研究では,機械学習に先立ってデータセットを分析することの重要性について報告する。
本稿では, 筒状代数分解に対する変数順序付けの選択について, 特定のケーススタディに対する結果を示す。
我々は、データセットのバランスとさらなる拡張を可能にするシステムのための拡張技術を導入する。
論文 参考訳(メタデータ) (2024-01-24T10:12:43Z) - Data Augmentation for Mathematical Objects [0.0]
非線形問題のデータセットと, 筒状分解のための変数順序付けを選択する問題を考える。
すでにラベル付けされた問題に変数名を入れ替えることで、さらにラベル付けを必要としない新しい問題インスタンスを生成します。
その結果,MLの精度は平均63%向上した。
論文 参考訳(メタデータ) (2023-07-13T16:02:45Z) - Evaluating and Improving Tool-Augmented Computation-Intensive Math
Reasoning [75.74103236299477]
CoT(Chain-of- Thought prompting)とツール拡張は、大きな言語モデルを改善するための効果的なプラクティスとして検証されている。
ツールインターフェース,すなわち textbfDELI を用いた推論ステップを考慮に入れた新しい手法を提案する。
CARPと他の6つのデータセットの実験結果から、提案されたDELIは、主に競合ベースラインを上回っていることが示された。
論文 参考訳(メタデータ) (2023-06-04T17:02:59Z) - Machine Learning Capability: A standardized metric using case difficulty
with applications to individualized deployment of supervised machine learning [2.2060666847121864]
モデル評価は教師付き機械学習分類解析において重要な要素である。
アイテム応答理論(IRT)と機械学習を用いたコンピュータ適応テスト(CAT)は、最終分類結果とは無関係にデータセットをベンチマークすることができる。
論文 参考訳(メタデータ) (2023-02-09T00:38:42Z) - Toward Theoretical Guidance for Two Common Questions in Practical
Cross-Validation based Hyperparameter Selection [72.76113104079678]
クロスバリデーションに基づくハイパーパラメータ選択における2つの一般的な質問に対する最初の理論的治療について述べる。
これらの一般化は、少なくとも、常に再トレーニングを行うか、再トレーニングを行わないかを常に実行可能であることを示す。
論文 参考訳(メタデータ) (2023-01-12T16:37:12Z) - Automatic Data Augmentation via Invariance-Constrained Learning [94.27081585149836]
下位のデータ構造は、しばしば学習タスクのソリューションを改善するために利用される。
データ拡張は、入力データに複数の変換を適用することで、トレーニング中にこれらの対称性を誘導する。
この作業は、学習タスクを解決しながらデータ拡張を自動的に適応することで、これらの問題に対処する。
論文 参考訳(メタデータ) (2022-09-29T18:11:01Z) - Toward Learning Robust and Invariant Representations with Alignment
Regularization and Data Augmentation [76.85274970052762]
本論文はアライメント正則化の選択肢の増大を動機としている。
我々は、ロバスト性および不変性の次元に沿って、いくつかの人気のある設計選択のパフォーマンスを評価する。
我々はまた、現実的と考える仮定の下で経験的な研究を補完するために、アライメント正則化の挙動を正式に分析する。
論文 参考訳(メタデータ) (2022-06-04T04:29:19Z) - Provable Continual Learning via Sketched Jacobian Approximations [17.381658875470638]
忘れを克服するための一般的なアプローチは、以前のタスクで不十分なモデルをペナルティ化することで損失関数を正規化することである。
理想的条件下であっても、対角行列が以前のタスクのヘッセン行列の近似が貧弱であれば、破滅的な忘れを被る可能性があることを示す。
過去のデータのヤコビ行列をスケッチした新しいタスクの正規化トレーニング。
論文 参考訳(メタデータ) (2021-12-09T18:36:20Z) - Sparse PCA via $l_{2,p}$-Norm Regularization for Unsupervised Feature
Selection [138.97647716793333]
再構成誤差を$l_2,p$ノルム正規化と組み合わせることで,単純かつ効率的な特徴選択手法を提案する。
提案する非教師付きモデルを解くための効率的な最適化アルゴリズムを提案し,アルゴリズムの収束と計算の複雑さを理論的に解析する。
論文 参考訳(メタデータ) (2020-12-29T04:08:38Z) - An Advance on Variable Elimination with Applications to Tensor-Based
Computation [11.358487655918676]
本稿では,確率的推論を含む多くのアルゴリズムの基盤となる可変除去の古典的アルゴリズムについて述べる。
結果は機能的依存関係の活用に関連しており、非常に大きなツリー幅を持つモデルで推論と学習を効率的に行うことができる。
論文 参考訳(メタデータ) (2020-02-21T14:17:44Z) - Supervised Quantile Normalization for Low-rank Matrix Approximation [50.445371939523305]
我々は、$X$ の値と $UV$ の値を行ワイズで操作できる量子正規化演算子のパラメータを学習し、$X$ の低ランク表現の質を改善する。
本稿では,これらの手法が合成およびゲノムデータセットに適用可能であることを実証する。
論文 参考訳(メタデータ) (2020-02-08T21:06:02Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。