Towards a Certified Proof Checker for Deep Neural Network Verification

要約

ディープ ニューラル ネットワーク (DNN) の最近の開発により、セーフティ クリティカルなシステムに DNN が採用されるようになり、安全性を保証する必要性が高まっています。
DNN のこれらの安全性は、検証コミュニティによって開発されたツールを使用して証明できます。
ただし、これらのツール自体には実装上のバグや数値安定性の問題が発生しやすいため、信頼性に疑問が生じます。
これを克服するために、一部の検証者は、信頼できるチェッカーによってチェックできる結果の証明を作成します。
この研究では、DNN 検証のためのプルーフ チェッカーの新しい実装を紹介します。
数値の安定性とより優れた検証可能性を提供することで、既存の実装を改善します。
これを達成するために、工業用定理証明者である Imandra の 2 つの重要な機能、つまり無限精度の実算のサポートと形式的検証インフラストラクチャを活用します。
これまでのところ、Imandra にプルーフ チェッカーを実装し、その正確性プロパティを指定して、チェッカーがそれらに準拠しているかどうかの検証を開始しました。
私たちの継続的な作業は、チェッカーの正式な検証を完了し、そのパフォーマンスをさらに最適化することに重点を置いています。

要約(オリジナル)

Recent developments in deep neural networks (DNNs) have led to their adoption in safety-critical systems, which in turn has heightened the need for guaranteeing their safety. These safety properties of DNNs can be proven using tools developed by the verification community. However, these tools are themselves prone to implementation bugs and numerical stability problems, which make their reliability questionable. To overcome this, some verifiers produce proofs of their results which can be checked by a trusted checker. In this work, we present a novel implementation of a proof checker for DNN verification. It improves on existing implementations by offering numerical stability and greater verifiability. To achieve this, we leverage two key capabilities of Imandra, an industrial theorem prover: its support of infinite precision real arithmetic and its formal verification infrastructure. So far, we have implemented a proof checker in Imandra, specified its correctness properties and started to verify the checker’s compliance with them. Our ongoing work focuses on completing the formal verification of the checker and further optimizing its performance.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google