Method for proving or identifying counter-examples in neural network systems that process point cloud data

Abstract

Described is a system for proving correctness properties of a neural network for providing estimates for point cloud data. The system receives as input a description of a neural network for generating estimates from a set of point cloud data. The description of the neural network is parsed to obtain a symbolic representation. Based on a combination of the symbolic representation and a set of analysis parameters, the system generates an analysis output indicating whether the neural network satisfies a correctness property in generating the estimates from the set of point cloud data. The analysis output is a mathematical proof artifact proving that the set of analysis parameters is satisfied, a list of one or more point clouds for which the set of analysis parameters is violated, or a report that progress could not be made by the analysis.

What is claimed is: 
     
         1 . A system for proving correctness properties of a neural network for providing estimates for point cloud data, the system comprising:
 one or more processors and a non-transitory computer-readable medium having executable instructions encoded thereon such that when executed, the one or more processors perform operations of:
 receiving, as input, a description of a neural network for generating estimates from a set of point cloud data, wherein the description of the neural network is in one of a source code format or a serialized format; 
 parsing the description of the neural network to obtain a symbolic representation; 
 based on a combination of the symbolic representation and a set of analysis parameters, generating an analysis output indicating whether the neural network satisfies a correctness property in generating the estimates from the set of point cloud data, 
 wherein the analysis output is one of a mathematical proof artifact proving that the set of analysis parameters is satisfied, a list of one or more point clouds for which the set of analysis parameters is violated, and a report that progress could not be made by the analysis. 
   
     
     
         2 . The system as set forth in  claim 1 , wherein the analysis output acts as a stopping condition for preventing deployment of the neural network. 
     
     
         3 . The system as set forth in  claim 1 , wherein the estimates comprise an estimate of a slope of a patch of the set of point cloud data. 
     
     
         4 . The system as set forth in  claim 1 , wherein the estimates comprise an estimate of a surface normal of a patch of the set of point cloud data. 
     
     
         5 . The system as set forth in  claim 1 , wherein the estimates comprise an estimate regarding whether a patch of the set of point cloud data is ground or non-ground. 
     
     
         6 . The system as set forth in  claim 1 , wherein the set of analysis parameters describe geometric properties of the set of point cloud data. 
     
     
         7 . A computer implemented method for proving correctness properties of a neural network for providing estimates for point cloud data, the method comprising an act of:
 causing one or more processors to execute instructions encoded on one or more associated memories, each associated memory being a non-transitory computer-readable medium, such that upon execution, the one or more processors perform operations of:
 receiving, as input, a description of a neural network for generating estimates from a set of point cloud data, wherein the description of the neural network is in one of a source code format or a serialized format; 
 parsing the description of the neural network to obtain a symbolic representation; 
 based on a combination of the symbolic representation and a set of analysis parameters, generating an analysis output indicating whether the neural network satisfies a correctness property in generating the estimates from the set of point cloud data, 
 wherein the analysis output is one of a mathematical proof artifact proving that the set of analysis parameters is satisfied, a list of one or more point clouds for which the set of analysis parameters is violated, and a report that progress could not be made by the analysis. 
   
     
     
         8 . The method as set forth in  claim 7 , wherein the analysis output acts as a stopping condition for preventing deployment of the neural network. 
     
     
         9 . The method as set forth in  claim 7 , wherein the estimates comprise an estimate of a slope of a patch of the set of point cloud data. 
     
     
         10 . The method as set forth in  claim 7 , wherein the estimates comprise an estimate of a surface normal of a patch of the set of point cloud data. 
     
     
         11 . The method as set forth in  claim 7 , wherein the estimates comprise an estimate regarding whether a patch of the set of point cloud data is ground or non-ground. 
     
     
         12 . The method as set forth in  claim 7 , wherein the set of analysis parameters describe geometric properties of the set of point cloud data. 
     
     
         13 . A computer readable program for proving correctness properties of a neural network for providing estimates for point cloud data, the computer readable program comprising:
 computer-readable instructions stored on a non-transitory computer-readable medium that are executable by a computer having one or more processors for causing the processor to perform operations of:
 receiving, as input, a description of a neural network for generating estimates from a set of point cloud data, wherein the description of the neural network is in one of a source code format or a serialized format; 
 parsing the description of the neural network to obtain a symbolic representation; 
 based on a combination of the symbolic representation and a set of analysis parameters, generating an analysis output indicating whether the neural network satisfies a correctness property in generating the estimates from the set of point cloud data, 
 wherein the analysis output is one of a mathematical proof artifact proving that the set of analysis parameters is satisfied, a list of one or more point clouds for which the set of analysis parameters is violated, and a report that progress could not be made by the analysis. 
   
     
     
         14 . The computer readable program as set forth in  claim 13 , wherein the analysis output acts as a stopping condition for preventing deployment of the neural network. 
     
     
         15 . The computer readable program as set forth in  claim 13 , wherein the estimates comprise an estimate of a slope of a patch of the set of point cloud data. 
     
     
         16 . The computer readable program as set forth in  claim 13 , wherein the estimates comprise an estimate of a surface normal of a patch of the set of point cloud data. 
     
     
         17 . The computer readable program as set forth in  claim 13 , wherein the estimates comprise an estimate regarding whether a patch of the set of point cloud data is ground or non-ground. 
     
     
         18 . The computer readable program as set forth in  claim 13 , wherein the set of analysis parameters describe geometric properties of the set of point cloud data.