LTL learning on GPUs

要約

線形時相論理 (LTL) は産業検証で広く使用されています。
LTL 式はトレースから学習できます。
LTL 数式学習のスケーリングは未解決の問題です。
新しい形式の列挙的プログラム合成を使用して、最初の GPU ベースの LTL 学習器を実装します。
学習者は健全で完全です。
私たちのベンチマークは、既存の最先端の学習器よりも少なくとも 2048 倍多くのトレースを処理し、平均して少なくとも 46 倍高速に処理することを示しています。
これは、特に、$O(\log n)$ の時間計算量を持つ新しいブランチフリー LTL セマンティクスによって実現されます。ここで、$n$ はトレース長ですが、以前の実装は $O(n^2)$ 以下でした (
ビット単位のブール演算と 2 のべき乗によるシフトには単位コストがあると仮定します (最新のプロセッサでは現実的な仮定です)。

要約(オリジナル)

Linear temporal logic (LTL) is widely used in industrial verification. LTL formulae can be learned from traces. Scaling LTL formula learning is an open problem. We implement the first GPU-based LTL learner using a novel form of enumerative program synthesis. The learner is sound and complete. Our benchmarks indicate that it handles traces at least 2048 times more numerous, and on average at least 46 times faster than existing state-of-the-art learners. This is achieved with, among others, novel branch-free LTL semantics that has $O(\log n)$ time complexity, where $n$ is trace length, while previous implementations are $O(n^2)$ or worse (assuming bitwise boolean operations and shifts by powers of 2 have unit costs — a realistic assumption on modern processors).

arxiv情報

提供元, 利用サービス

arxiv.jp, Google