Tightening the Evaluation of PAC Bounds Using Formal Verification Results

要約

おそらくおおよそ正しい (PAC) 境界は、機械学習モデルの一般化に対する確率的保証を導き出すために広く使用されています。
これらは、一般化能力に貢献するモデルのコンポーネントを強調しています。
ただし、現在の最先端の結果は、展開された機械学習モデルの汎化能力の近似に関しては不正確です。
したがって、PAC 境界は理論的には有用ですが、特定の運用設計ドメインにおけるモデルの一般化プロパティを評価するための適用可能性は限られています。
基礎となる古典理論は、ユーザーがモデルを評価するために利用できるテスト ポイントの数が増加すると、境界を厳しくできるという考えによって裏付けられています。
ただし、ニューラル ネットワークの場合、対象範囲を取得するために必要なテスト ポイントの数は、小さな問題であっても現実的ではないことがよくあります。
この論文では、ニューラル システムの形式的検証を使用して PAC 境界の評価を通知するという新しいアプローチを採用します。
繰り返しのテストから得られた点ごとの情報を使用するのではなく、テスト ポイントの周囲の領域の検証結果を使用します。
検証結果に対する既存の境界を条件付けすると、検証された領域の基礎となる確率質量に比例して引き締めが行われることを示します。

要約(オリジナル)

Probably Approximately Correct (PAC) bounds are widely used to derive probabilistic guarantees for the generalisation of machine learning models. They highlight the components of the model which contribute to its generalisation capacity. However, current state-of-the-art results are loose in approximating the generalisation capacity of deployed machine learning models. Consequently, while PAC bounds are theoretically useful, their applicability for evaluating a model’s generalisation property in a given operational design domain is limited. The underlying classical theory is supported by the idea that bounds can be tightened when the number of test points available to the user to evaluate the model increases. Yet, in the case of neural networks, the number of test points required to obtain bounds of interest is often impractical even for small problems. In this paper, we take the novel approach of using the formal verification of neural systems to inform the evaluation of PAC bounds. Rather than using pointwise information obtained from repeated tests, we use verification results on regions around test points. We show that conditioning existing bounds on verification results leads to a tightening proportional to the underlying probability mass of the verified region.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google