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

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.

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.