論文の概要: 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課題を含む新しいデータセットを作成します。 さらに,情報漏洩の問題を評価し,新しいデータセット上でモデルの一般化可能性をテストする。

関連論文リスト

• ReasonAgain: Using Extractable Symbolic Programs to Evaluate Mathematical Reasoning [54.70811660561151]
  既存の数学データセットは、最終回答または静的例から派生した中間推論ステップを用いて、大規模言語モデル(LLM)の推論能力を評価する。 モデルがプログラムへの様々な入力に対して常に正しい最終回答を生成できる場合、シンボルプログラムを自動評価の手段として利用したいと考えている。 提案手法は, 従来の静的な例と比較して, 精度の低下を観測し, 現状のLLMにおける数学推論の脆弱さを示唆する。
  論文  参考訳（メタデータ） (2024-10-24T18:02:37Z)
• CorDA: Context-Oriented Decomposition Adaptation of Large Language Models for Task-Aware Parameter-Efficient Fine-tuning [101.81127587760831]
  現在の微調整手法は、学習すべき下流タスクのコンテキストや、維持すべき重要な知識のコンテキストに広く適用できるアダプタを構築している。 学習可能なタスク対応アダプタを構築するコンテキスト指向の分解適応手法であるCorDAを提案する。 本手法は,知識保存型適応と指導レビュー型適応の2つの選択肢を実現する。
  論文  参考訳（メタデータ） (2024-06-07T19:10:35Z)
• Robust Capped lp-Norm Support Vector Ordinal Regression [85.84718111830752]
  正規回帰は、ラベルが固有の順序を示す特殊な教師付き問題である。 卓越した順序回帰モデルとしてのベクトル順序回帰は、多くの順序回帰タスクで広く使われている。 我々は,新たなモデルであるCapped $ell_p$-Norm Support Vector Ordinal Regression (CSVOR)を導入する。
  論文  参考訳（メタデータ） (2024-04-25T13:56:05Z)
• Boarding for ISS: Imbalanced Self-Supervised: Discovery of a Scaled Autoencoder for Mixed Tabular Datasets [1.2289361708127877]
  不均衡な自己教師付き学習の分野は、広く研究されていない。 既存の研究は主に画像データセットに焦点を当てている。 バランス学習のための新しい指標として,マルチスーパーバイザードバランスMSEを提案する。
  論文  参考訳（メタデータ） (2024-03-23T10:37:22Z)
• 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)
• 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)
• 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)
• Supervised Quantile Normalization for Low-rank Matrix Approximation [50.445371939523305]
  我々は、$X$ の値と $UV$ の値を行ワイズで操作できる量子正規化演算子のパラメータを学習し、$X$ の低ランク表現の質を改善する。 本稿では,これらの手法が合成およびゲノムデータセットに適用可能であることを実証する。
  論文  参考訳（メタデータ） (2020-02-08T21:06:02Z)

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

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