Recent advances in the verification of deep neural networks (DNNs) have
opened the way for broader usage of DNN verification technology in many
application areas, including safety-critical ones. DNN verifiers are themselves
complex programs that have been shown to be susceptible to errors and
imprecisions; this in turn has raised the question of trust in DNN verifiers.
One prominent attempt to address this issue is enhancing DNN verifiers with the
capability of producing proofs of their results that are subject to independent
algorithmic certification (proof checking). Formulations of proof production
and proof checking already exist on top of the state-of-the-art Marabou DNN
verifier. The native implementation of the proof checking algorithm for Marabou
was done in C++ and itself raised the question of trust in the code (e.g., in
the precision of floating point calculations or guarantees for implementation
soundness). Here, we present an alternative implementation of the Marabou proof
checking algorithm in Imandra -- an industrial functional programming language
and prover -- that allows us to obtain an implementation with formal
guarantees, including proofs of mathematical results underlying the algorithm,
such as the use of the Farkas lemma.

深度神经网络验证技术的验证进展为 DNN 验证器的广泛应用开辟了道路，提出了在 Marabou DNN 验证器的基础上以 Imandra 为实现语言进行形式保证的 Marabou 证明检查算法的替代实现。