3D point cloud models are widely applied in safety-critical scenes, which delivers an urgent
need to obtain more solid proofs to verify the robustness of models. Existing verifcation
method for point cloud model is time-expensive and computationally unattainable on large
networks. Additionally, they cannot handle the complete PointNet model with joint alignment network that contains multiplication layers, which efectively boosts the performance
of 3D models. This motivates us to design a more efcient and general framework to verify
various architectures of point cloud models. The key challenges in verifying the large-scale
complete PointNet models are addressed as dealing with the cross-non-linearity operations
in the multiplication layers and the high computational complexity of high-dimensional
point cloud inputs and added layers. Thus, we propose an efcient verifcation framework,
3DVerifer, to tackle both challenges by adopting a linear relaxation function to bound the
multiplication layer and combining forward and backward propagation to compute the certifed bounds of the outputs of the point cloud models. Our comprehensive experiments
demonstrate that 3DVerifer outperforms existing verifcation algorithms for 3D models in
terms of both efciency and accuracy. Notably, our approach achieves an orders-of-magnitude improvement in verifcation efciency for the large network, and the obtained certifed
bounds are also signifcantly tighter than the state-of-the-art verifers. We release our tool
3DVerifer via https://github.com/TrustAI/3DVerifer for use by the community.