核心概念
muRelBenchは、ゾノトープ領域の操作をマイクロベンチマーキングするための拡張可能なフレームワークである。これにより、新しいアルゴリズムの効率を包括的に評価することができる。
摘要
本論文では、ゾノトープ領域とその操作のマイクロベンチマーキングを行うmuRelBenchフレームワークを紹介する。ゾノトープ領域は、プログラムや機械学習モデルの検証に広く使用されている。ゾノトープ領域の操作、例えば最小上界(LUB)、クロージャ、忘却演算子などは、検証器の計算時間を大きく支配する。そのため、これらの操作の効率化に関する研究が行われてきた。
muRelBenchは以下の3つの主要な特徴を持つ:
- パラメータ化された抽象状態の動的生成
- ユーザ定義の操作の適用
- ユーザ定義のプロパティチェック
本論文では、Octagonドメインを例に、クロージャ操作の2つのアルゴリズム(Floyd-Warshall、Chawdhary)を比較する事例研究を示す。この事例研究では、変数数や変数間の密度の異なる合成的なOctagonインスタンスを生成し、2つのクロージャアルゴリズムの性能を評価している。結果、変数数が多く、変数間の密度が高い場合にChawdharyのアルゴリズムが優れていることが示された。
統計資料
変数数が25の場合、Floyd-Warshallのクロージャ操作の平均時間は144ms、標準偏差は32.2ms。
変数数が25の場合、Chawdharyのクロージャ操作の平均時間は117ms、標準偏差は5.1ms。
変数数が50の場合、Floyd-Warshallのクロージャ操作の平均時間は46.8ms、標準偏差は3.1ms。
変数数が50の場合、Chawdharyのクロージャ操作の平均時間は49.6ms、標準偏差は10.3ms。
引述
"muRelBenchは、ゾノトープ領域の操作のプロトタイピングと既存の実装の効率性評価を支援する。"
"変数数が多く、変数間の密度が高い場合、Chawdharyのクロージャアルゴリズムが優れた性能を示す。"