論文の概要: SemML 2.0: Synthesizing Controllers for LTL
- arxiv url: http://arxiv.org/abs/2604.24102v1
- Date: Mon, 27 Apr 2026 06:50:14 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-04-28 17:12:07.776736
- Title: SemML 2.0: Synthesizing Controllers for LTL
- Title(参考訳): SemML 2.0: LTL用のコントローラの合成
- Authors: Jan Křetínský, Tobias Meggendorfer, Maximilian Prokop,
- Abstract要約: SemMLの2番目のバージョンは、どちらのソリューションでも、最先端のツールよりも優れています。
我々は,既存の最先端ツール(特にStrix,LtlSynt,およびSemMLの前バージョン)に対して,合成競合SyntCOMPのデータセット上で評価を行った。
- 参考スコア(独自算出の注目度): 4.1483423188102755
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Synthesizing a reactive system from specifications given in linear temporal logic (LTL) is a classical problem, finding its applications in safety-critical systems design. These systems are typically represented using either Mealy machines or AIGER circuits. We present the second version of SemML, which outperforms all state-of-the-art tools for finding either solution. Aside from implementing the classical automata-theoretic approach, our tool utilizes partial exploration and machine-learning guidance for obtaining solutions efficiently, and numerous heuristics and improvements of classic algorithms for extracting small representations of these solutions. We evaluate our tool against the existing state-of-the-art tools (in particular Strix, LtlSynt, and the previous version of SemML) on the dataset of the synthesis competition SYNTCOMP. We show that we solve significantly more instances and do so much faster than other tools, while maintaining state-of-the-art solution quality.
- Abstract(参考訳): 線形時間論理(LTL)の仕様からリアクティブシステムを合成することは古典的な問題であり、安全クリティカルなシステム設計にその応用を見出した。
これらのシステムは一般にMealyマシンまたはAIGER回路を用いて表現される。
SemMLの2番目のバージョンは、どちらのソリューションでも、最先端のツールよりも優れています。
提案手法は,古典的オートマトン理論の手法の他に,部分探索と機械学習の指導による解の効率向上,およびこれらの解の小さな表現を抽出するための古典的アルゴリズムの多くのヒューリスティックと改良を利用した。
我々は,既存の最先端ツール(特にStrix,LtlSynt,およびSemMLの以前のバージョン)を合成競合SynTCOMPのデータセット上で評価した。
私たちは、最先端のソリューションの品質を維持しながら、はるかに多くのインスタンスを解決し、他のツールよりもはるかに高速に実行しています。
関連論文リスト
- SOCRATES: Simulation Optimization with Correlated Replicas and Adaptive Trajectory Evaluations [25.18297372152296]
SOCRATESは、調整されたSOアルゴリズムの設計を自動化する新しい2段階のプロシージャである。
実システムのデジタルレプリカのアンサンブルは、ベースラインSOアルゴリズムのセットを評価するテストベッドとして使用される。
LLMはメタ最適化器として機能し、これらのアルゴリズムのパフォーマンストラジェクトリを分析して、最終的なハイブリッド最適化スケジュールを反復的に修正し構成する。
論文 参考訳(メタデータ) (2025-11-01T19:57:38Z) - Tool-Star: Empowering LLM-Brained Multi-Tool Reasoner via Reinforcement Learning [63.31585771716123]
大言語モデル(LLM)は、大規模強化学習(RL)を通じて顕著な推論能力を示した。
ステップワイズ推論中に複数の外部ツールを自律的に呼び出すLLベースのフレームワークであるTool-Starを紹介する。
Tool-Starは6種類のツールを統合し、データ合成とトレーニングの両方に体系的な設計を取り入れている。
論文 参考訳(メタデータ) (2025-05-22T09:00:19Z) - SemML: Enhancing Automata-Theoretic LTL Synthesis with Machine Learning [3.468621550644668]
SemMLは今年のSynTCOMPの実現可能性トラックで優勝した。
我々は,SynTCOMPの今年の実現可能性トラックを受賞したSemMLを紹介する。
論文 参考訳(メタデータ) (2025-01-29T09:06:19Z) - Scaffolded Language Models with Language Supervision for Mixed-Autonomy: A Survey [52.00674453604779]
本調査は,戦後のLM周辺における新規構造物の設計と最適化に関する文献を整理した。
本稿では,この階層構造を足場型LMと呼び,ツールを用いた多段階プロセスに統合されたLMに焦点を当てる。
論文 参考訳(メタデータ) (2024-10-21T18:06:25Z) - Planning, Creation, Usage: Benchmarking LLMs for Comprehensive Tool Utilization in Real-World Complex Scenarios [93.68764280953624]
UltraToolは、ツール利用におけるLarge Language Modelsの能力を改善し評価するために設計された、新しいベンチマークである。
現実の複雑さを強調し、効果的な問題解決のために正確で多段階の計画を必要とする。
UltraToolの重要な特徴は、ツールの使用前に発生する自然言語による計画の独立した評価である。
論文 参考訳(メタデータ) (2024-01-30T16:52:56Z) - Machine Learning Insides OptVerse AI Solver: Design Principles and
Applications [74.67495900436728]
本稿では,Huawei CloudのOpsVerse AIソルバに機械学習(ML)技術を統合するための総合的研究について述べる。
本稿では,実世界の多面構造を反映した生成モデルを用いて,複雑なSATインスタンスとMILPインスタンスを生成する手法を紹介する。
本稿では,解解器性能を著しく向上させる,最先端パラメータチューニングアルゴリズムの導入について詳述する。
論文 参考訳(メタデータ) (2024-01-11T15:02:15Z) - INVICTUS: Optimizing Boolean Logic Circuit Synthesis via Synergistic
Learning and Search [18.558280701880136]
最先端論理合成アルゴリズムは、多数の論理最小化を持つ。
INVICTUSは、以前に見られた設計のトレーニングデータセットに基づいて、論理最小化のシーケンスを生成する。
論文 参考訳(メタデータ) (2023-05-22T15:50:42Z) - LTLf Synthesis on Probabilistic Systems [0.0]
合成は、この行動を達成する確率を最大化するポリシーを見つけるために用いられる。
有限トレース特性を与えられた振る舞いに対するポリシー合成を解くための道具は存在しない。
本稿では,マルコフプロセスの削減による2つの問題を解決するアルゴリズムと,オートマトンフのための2番目のネイティブツールを提案する。
論文 参考訳(メタデータ) (2020-09-23T01:26:47Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。