論文の概要: LTL$_f$ Learning Meets Boolean Set Cover
- arxiv url: http://arxiv.org/abs/2509.24616v1
- Date: Mon, 29 Sep 2025 11:20:20 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-09-30 22:32:19.939647
- Title: LTL$_f$ Learning Meets Boolean Set Cover
- Title(参考訳): LTL$_f$ LearningがBoolean Set Coverと出会う
- Authors: Gabriel Bathie, Nathanaël Fijalkow, Théo Matricon, Baptiste Mouillon, Pierre Vandenhove,
- Abstract要約: 我々はBoltと呼ばれる新しいCPUツールを実装し、ベンチマークの70%よりも100倍以上高速な公式を学習することで、技術の状態を改善した。
Boolean Set Coverコンポーネントのおかげで、私たちのアプローチは効率と公式サイズの間に新たなトレードオフを提供します。
- 参考スコア(独自算出の注目度): 6.812264464807767
- License: http://creativecommons.org/licenses/by-sa/4.0/
- Abstract: Learning formulas in Linear Temporal Logic (LTLf) from finite traces is a fundamental research problem which has found applications in artificial intelligence, software engineering, programming languages, formal methods, control of cyber-physical systems, and robotics. We implement a new CPU tool called Bolt improving over the state of the art by learning formulas more than 100x faster over 70% of the benchmarks, with smaller or equal formulas in 98% of the cases. Our key insight is to leverage a problem called Boolean Set Cover as a subroutine to combine existing formulas using Boolean connectives. Thanks to the Boolean Set Cover component, our approach offers a novel trade-off between efficiency and formula size.
- Abstract(参考訳): 有限トレースから線形時間論理(LTLf)で公式を学ぶことは、人工知能、ソフトウェア工学、プログラミング言語、形式的手法、サイバー物理システムの制御、ロボット工学の応用を見出した基本的な研究問題である。
ベンチマークの70%よりも100倍以上高速な公式を学習し、98%のケースでより小さいか等しい公式を学習することで、Boltと呼ばれる新しいCPUツールを実装しました。
我々の重要な洞察は、ブール集合被覆(Boolean Set Cover)と呼ばれる問題をサブルーチンとして活用し、ブール連結体を用いて既存の公式を組み合わせることである。
Boolean Set Coverコンポーネントのおかげで、私たちのアプローチは効率と公式サイズの間に新たなトレードオフを提供します。
関連論文リスト
- ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis [50.020850767257095]
本稿では,LLMに様々な粒度で自動化手法を付加するProofAugを提案する。
本手法は,オープンソースのDeep-math-7bベースモデルとIsabelle証明アシスタントを用いて,MiniF2Fベンチマークで検証した。
また、ProofAugのLean 4バージョンを実装し、Kimina-Prover-seek-Distill-1.5Bのパス@1のパフォーマンスを44.3%から50.4%に改善します。
論文 参考訳(メタデータ) (2025-01-30T12:37:06Z) - Enabling High-Sparsity Foundational Llama Models with Efficient Pretraining and Deployment [56.44025052765861]
大規模言語モデル(LLM)は自然言語処理(NLP)に革命をもたらしたが、そのサイズは計算のボトルネックを生み出している。
そこで本研究では,高性能LLMの高精度かつ疎結合な基本バージョンを作成するための新しいアプローチを提案する。
スパース量子化LLaMAの最大8.6倍のCPU上での総高速化を示す。
論文 参考訳(メタデータ) (2024-05-06T16:03:32Z) - torchmSAT: A GPU-Accelerated Approximation To The Maximum Satisfiability
Problem [1.5850859526672516]
最大満足度問題(MaxSAT)の解を近似できる単一の微分可能関数を導出する。
我々は,我々の微分可能な関数をモデル化する新しいニューラルネットワークアーキテクチャを提案し,バックプロパゲーションを用いてMaxSATを段階的に解く。
論文 参考訳(メタデータ) (2024-02-06T02:33:00Z) - Machine Learning Insides OptVerse AI Solver: Design Principles and
Applications [74.67495900436728]
本稿では,Huawei CloudのOpsVerse AIソルバに機械学習(ML)技術を統合するための総合的研究について述べる。
本稿では,実世界の多面構造を反映した生成モデルを用いて,複雑なSATインスタンスとMILPインスタンスを生成する手法を紹介する。
本稿では,解解器性能を著しく向上させる,最先端パラメータチューニングアルゴリズムの導入について詳述する。
論文 参考訳(メタデータ) (2024-01-11T15:02:15Z) - Symbolic Regression on FPGAs for Fast Machine Learning Inference [2.0920303420933273]
高エネルギー物理コミュニティは、FPGA(Field-Programmable Gate Arrays)上に機械学習ベースのソリューションをデプロイする可能性を探っている
シンボリックレグレッション(SR)と呼ばれる機械学習技術を利用した新しいエンドツーエンドプロシージャを提案する。
提案手法は,最大で5 nsまでの実行時間を最大13倍に抑えながら,90%以上の近似精度を維持した推論モデルを用いて3層ニューラルネットワークを近似できることを示す。
論文 参考訳(メタデータ) (2023-05-06T17:04:02Z) - Reinforcement Learning for Branch-and-Bound Optimisation using
Retrospective Trajectories [72.15369769265398]
機械学習は分岐のための有望なパラダイムとして登場した。
分岐のための単純かつ効果的なRLアプローチであるレトロ分岐を提案する。
我々は現在最先端のRL分岐アルゴリズムを3~5倍に上回り、500の制約と1000の変数を持つMILP上での最高のILメソッドの性能の20%以内である。
論文 参考訳(メタデータ) (2022-05-28T06:08:07Z) - Machine Learning Methods in Solving the Boolean Satisfiability Problem [72.21206588430645]
本論文は, Boolean satisfiability problem (SAT) を機械学習技術で解くことに関する最近の文献をレビューする。
ML-SATソルバを手作り特徴を持つナイーブ分類器からNeuroSATのような新たなエンド・ツー・エンドSATソルバまで,進化するML-SATソルバについて検討する。
論文 参考訳(メタデータ) (2022-03-02T05:14:12Z) - Scalable Anytime Algorithms for Learning Formulas in Linear Temporal
Logic [2.631744051718347]
トレースを分類する公式を学習する際の問題点を考察する。
既存の解には2つの制限がある: それらは小さな公式を超えてスケールせず、結果を返すことなく計算資源を消費する。
我々は,両問題に対処する新しいアルゴリズムを導入する。我々のアルゴリズムは,従来よりも桁違いに大きい式を構築でき,いつでも可能である。
論文 参考訳(メタデータ) (2021-10-13T13:57:31Z) - Transformer-based Machine Learning for Fast SAT Solvers and Logic
Synthesis [63.53283025435107]
CNFベースのSATとMaxSATは論理合成と検証システムの中心である。
そこで本研究では,Transformerアーキテクチャから派生したワンショットモデルを用いて,MaxSAT問題の解法を提案する。
論文 参考訳(メタデータ) (2021-07-15T04:47:35Z) - PAC-learning gains of Turing machines over circuits and neural networks [1.4502611532302039]
私達は最低記述の長さの原則を持って来ることができるサンプル効率の潜在的な利益を研究します。
我々はチューリングマシンを用いて普遍的なモデルと回路を表現する。
回路の複雑さと密接性における古典的オープン問題との密接な関係を浮き彫りにする。
論文 参考訳(メタデータ) (2021-03-23T17:03:10Z) - Understanding Boolean Function Learnability on Deep Neural Networks: PAC Learning Meets Neurosymbolic Models [14.29299960914962]
モデルサンプリングベンチマーク、最適化問題、および制約度の異なるランダム3CNFに関する公式を解析する。
i) ニューラルネットワークは、純粋なルールベースのシステムや純粋なシンボリックアプローチよりも一般化します。
論文 参考訳(メタデータ) (2020-09-13T03:49:20Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。