論文の概要: Machine Learning for Quantifier Selection in cvc5

• arxiv url: http://arxiv.org/abs/2408.14338v1
• Date: Mon, 26 Aug 2024 15:07:35 GMT
• ステータス: 処理完了
• システム内更新日: 2024-08-27 13:31:39.263219
• Title: Machine Learning for Quantifier Selection in cvc5
• Title（参考訳）: cvc5における量子化器選択のための機械学習
• Authors: Jan Jakubův, Mikoláš Janota, Jelle Piepenbrock, Josef Urban,
• Abstract要約: 我々は、どの量化器をインスタンス化すべきか、どちらがそうでないかを解決者に知らせる効率的な機械学習モデルを訓練する。 そこで本研究では,Mizar Mathematical Libraryから収集した大量の一階問題に基づいて学習を行った結果,システムのホールドアウトセット性能が大幅に向上したことを示す。
• 参考スコア（独自算出の注目度）: 1.8749305679160366
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: In this work we considerably improve the state-of-the-art SMT solving on first-order quantified problems by efficient machine learning guidance of quantifier selection. Quantifiers represent a significant challenge for SMT and are technically a source of undecidability. In our approach, we train an efficient machine learning model that informs the solver which quantifiers should be instantiated and which not. Each quantifier may be instantiated multiple times and the set of the active quantifiers changes as the solving progresses. Therefore, we invoke the ML predictor many times, during the whole run of the solver. To make this efficient, we use fast ML models based on gradient boosting decision trees. We integrate our approach into the state-of-the-art cvc5 SMT solver and show a considerable increase of the system's holdout-set performance after training it on a large set of first-order problems collected from the Mizar Mathematical Library.
• Abstract（参考訳）: 本研究では,一階量子化問題に対する最先端のSMT解法を,量子化器選択の効率的な機械学習ガイダンスにより大幅に改善する。 量子化器はSMTにとって重要な課題であり、技術的には決定不能の源である。 提案手法では,どの量化器をインスタンス化すべきか,どちらがそうでないかを,解法者に知らせる効率的な機械学習モデルを訓練する。 それぞれの量化器は複数回インスタンス化され、解法が進むにつれて活性量化器の集合が変化する。 そこで我々は,ML予測器を複数回起動する。 これを効率的にするために、勾配向上決定木に基づく高速MLモデルを用いる。 この手法を最先端のcvc5 SMTソルバに統合し,Mizar Mathematical Libraryから収集した大量の一階問題の学習後,システムのホールドアウトセット性能を大幅に向上させる。

関連論文リスト

• Unlearning as multi-task optimization: A normalized gradient difference approach with an adaptive learning rate [105.86576388991713]
  正規化勾配差(NGDiff)アルゴリズムを導入し、目的間のトレードオフをよりよく制御できるようにする。 本研究では,TOFUおよびMUSEデータセットにおける最先端の未学習手法において,NGDiffの優れた性能を実証的に実証し,理論的解析を行った。
  論文  参考訳（メタデータ） (2024-10-29T14:41:44Z)
• Enhancing Multi-Step Reasoning Abilities of Language Models through Direct Q-Function Optimization [50.485788083202124]
  強化学習(Reinforcement Learning, RL)は、大規模言語モデルを人間の好みと整合させ、複雑なタスクを遂行する能力を向上させる上で重要な役割を担っている。 反応生成過程をマルコフ決定プロセス(MDP)として定式化し,ソフトアクター・クリティック(SAC)フレームワークを用いて,言語モデルによって直接パラメータ化されたQ関数を最適化する,直接Q関数最適化(DQO)を提案する。 GSM8KとMATHという2つの数学問題解決データセットの実験結果から、DQOは従来の手法よりも優れており、言語モデルを整合させるための有望なオフライン強化学習手法として確立されている。
  論文  参考訳（メタデータ） (2024-10-11T23:29:20Z)
• Tender: Accelerating Large Language Models via Tensor Decomposition and Runtime Requantization [0.6445087473595953]
  大規模言語モデル(LLM)は、機械学習における様々なタスクにおいて優れたパフォーマンスを示す。 LLM推論のデプロイは、高い計算とメモリ要求のために問題となる。 我々は,低精度でLLM推論を効率的に展開できるアルゴリズム-ハードウェア共設計ソリューションであるテンダーを提案する。
  論文  参考訳（メタデータ） (2024-06-16T09:51:55Z)
• Taking the human out of decomposition-based optimization via artificial intelligence: Part II. Learning to initialize [0.0]
  提案手法は解時間を大幅に短縮することができる。 アクティブかつ教師付き学習は、計算性能を予測する代理モデルを学ぶために使用される。 その結果,提案手法が解時間を大幅に短縮する可能性が示唆された。
  論文  参考訳（メタデータ） (2023-10-10T23:49:26Z)
• The Devil is in the Errors: Leveraging Large Language Models for Fine-grained Machine Translation Evaluation [93.01964988474755]
  AutoMQMは,大規模な言語モデルに対して,翻訳におけるエラーの識別と分類を求めるプロンプト技術である。 テキスト内学習と微調整によるラベル付きデータの影響について検討する。 次に, PaLM-2モデルを用いてAutoMQMを評価し, スコアのプロンプトよりも性能が向上することがわかった。
  論文  参考訳（メタデータ） (2023-08-14T17:17:21Z)
• Learning to Optimize Permutation Flow Shop Scheduling via Graph-based Imitation Learning [70.65666982566655]
  置換フローショップスケジューリング(PFSS)は製造業で広く使われている。 我々は,より安定かつ正確に収束を加速する専門家主導の模倣学習を通じてモデルを訓練することを提案する。 我々のモデルのネットワークパラメータはわずか37%に減少し、エキスパートソリューションに対する我々のモデルの解のギャップは平均6.8%から1.3%に減少する。
  論文  参考訳（メタデータ） (2022-10-31T09:46:26Z)
• Large Scale Mask Optimization Via Convolutional Fourier Neural Operator and Litho-Guided Self Training [54.16367467777526]
  マスクタスクを効率的に学習できる畳み込みニューラルネットワーク(CFCF)を提案する。 機械学習ベースのフレームワークが初めて、最先端の数値マスクデータセットを上回った。
  論文  参考訳（メタデータ） (2022-07-08T16:39:31Z)
• Learning the Quality of Machine Permutations in Job Shop Scheduling [9.972171952370287]
  機械の順列の質を予測することを目的とした新しい教師付き学習タスクを提案する。 そして、我々は、正確な逐次深層学習モデルを作成することができるような、この品質を推定する独自の方法論を設計する。
  論文  参考訳（メタデータ） (2022-07-07T11:53:10Z)
• Model-Agnostic Multitask Fine-tuning for Few-shot Vision-Language Transfer Learning [59.38343286807997]
  未知タスクの視覚言語モデルのためのモデル非依存型マルチタスクファインチューニング(MAMF)を提案する。 モデルに依存しないメタラーニング(MAML)と比較して、MAMFは二段階最適化を捨て、一階勾配のみを使用する。 MAMFは5つのベンチマークデータセット上で、数ショットの転送学習において古典的な微調整法よりも一貫して優れていることを示す。
  論文  参考訳（メタデータ） (2022-03-09T17:26:53Z)
• Learning the Markov Decision Process in the Sparse Gaussian Elimination [0.0]
  スパースガウス除去のための学習に基づくアプローチを提案する。 スパースソルバの主モジュールに対するQ-Learningアルゴリズムを提案する。
  論文  参考訳（メタデータ） (2021-09-30T08:56:39Z)
• A fast learning algorithm for One-Class Slab Support Vector Machines [1.1613446814180841]
  本稿では,SMO (Sequential Minimal Optimization) を用いた一級スラブSVMの高速トレーニング手法を提案する。 その結果、このトレーニング手法は、他の準計画法(QP)の解法よりも、大規模なトレーニングデータに対してより優れたスケールが可能であることが示唆された。
  論文  参考訳（メタデータ） (2020-11-06T09:16:39Z)

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

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