Revisiting Variable Ordering for Real Quantifier Elimination using Machine Learning

要約

円筒代数分解 (CAD) は、サイバーフィジカル システムの正式な検証のための主要な証明手法です。
CAD は計算コストが高く、最悪の場合、二重指数関数的な複雑さがあります。
最適な変数順序を選択することは、CAD を効率的に使用する上で最も重要です。
以前の研究では、機械学習が効率的な変数の順序付けを決定するのに役立つことが実証されています。
この作業の多くは、MetiTarski の定理証明者のアプリケーションから抽出された CAD の問題によって推進されています。
このホワイト ペーパーでは、この以前の作業を再検討し、既存のトレーニング データとテスト データのバイアスの問題を検討します。
従来の MetiTarski ベンチマークは、特定の変数の順序付けに大きく偏っていることがわかりました。
これに対処するために、対称性を適用して、偏りを取り除くように設計された 41K 以上の MetiTarski チャレンジを含む新しいデータセットを作成します。
さらに、情報漏洩の問題を評価し、新しいデータセットでモデルの一般化可能性をテストします。

要約(オリジナル)

Cylindrical Algebraic Decomposition (CAD) is a key proof technique for formal verification of cyber-physical systems. CAD is computationally expensive, with worst-case doubly-exponential complexity. Selecting an optimal variable ordering is paramount to efficient use of CAD. Prior work has demonstrated that machine learning can be useful in determining efficient variable orderings. Much of this work has been driven by CAD problems extracted from applications of the MetiTarski theorem prover. In this paper, we revisit this prior work and consider issues of bias in existing training and test data. We observe that the classical MetiTarski benchmarks are heavily biased towards particular variable orderings. To address this, we apply symmetries to create a new dataset containing more than 41K MetiTarski challenges designed to remove bias. Furthermore, we evaluate issues of information leakage, and test the generalizability of our models on the new dataset.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google