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.

翻译：近年来，深度神经网络（DNN）的发展促使其被应用于安全关键系统，这进一步凸显了保障其安全性的需求。DNN的安全性可通过验证社区开发的工具加以证明。然而，这些工具本身存在实现漏洞与数值稳定性问题，其可靠性因而存疑。为解决此问题，部分验证器会生成结果的证明，并由可信检查器进行核查。本文提出了一种新型DNN验证证明检查器实现，其通过提供数值稳定性与更高的可验证性，改进了现有实现方案。为达成此目标，我们利用了工业定理证明器Imandra的两项核心能力：无限精度实数算术支持及其形式化验证基础设施。目前，我们已在Imandra中实现了一个证明检查器，完成了其正确性属性规约，并开始验证检查器对规约的符合性。当前工作聚焦于完成检查器的形式化验证并进一步优化其性能。