U.S. patent application number 17/078079 was filed with the patent office on 2021-09-09 for method for proving or identifying counter-examples in neural network systems that process point cloud data.
The applicant listed for this patent is HRL Laboratories, LLC. Invention is credited to Aleksey Nogin, Christopher Serrano, Michael A. Warren.
Application Number | 20210279570 17/078079 |
Document ID | / |
Family ID | 1000005219590 |
Filed Date | 2021-09-09 |
United States Patent
Application |
20210279570 |
Kind Code |
A1 |
Warren; Michael A. ; et
al. |
September 9, 2021 |
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.
Inventors: |
Warren; Michael A.;
(Northridge, CA) ; Serrano; Christopher;
(Whittier, CA) ; Nogin; Aleksey; (Fresno,
CA) |
|
Applicant: |
Name |
City |
State |
Country |
Type |
HRL Laboratories, LLC |
Malibu |
CA |
US |
|
|
Family ID: |
1000005219590 |
Appl. No.: |
17/078079 |
Filed: |
October 22, 2020 |
Related U.S. Patent Documents
|
|
|
|
|
|
Application
Number |
Filing Date |
Patent Number |
|
|
62984693 |
Mar 3, 2020 |
|
|
|
62984676 |
Mar 3, 2020 |
|
|
|
Current U.S.
Class: |
1/1 |
Current CPC
Class: |
G06F 7/544 20130101;
G06N 3/08 20130101 |
International
Class: |
G06N 3/08 20060101
G06N003/08 |
Goverment Interests
GOVERNMENT LICENSE RIGHTS
[0003] This invention was made with government support under U.S.
Government Contract Number FA8750-18-C-0092. The government may
have certain rights in the invention.
Claims
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.
Description
CROSS-REFERENCE TO RELATED APPLICATIONS
[0001] This is a Non-Provisional Application of U.S. Provisional
Patent Application No. 62/984,693, filed Mar. 3, 2020, entitled,
"An Automatic Procedure for Either Proving or Identifying
Counter-Examples to Correctness Properties for Neural Network Based
Slope Estimation and Ground Plane Segmentation Systems that Process
Point Cloud Data", the entirety of which is incorporated herein by
reference.
[0002] This is also a Non-Provisional Application of U.S.
Provisional Patent Application No. 62/984,676, filed Mar. 3, 2020,
entitled, "A Neural Network Architecture for Small Lidar Processing
Networks for Slope Estimation and Ground Plane Segmentation", the
entirety of which is incorporated herein by reference.
BACKGROUND OF INVENTION
(1) Field of Invention
[0004] The present invention relates to a system for proving
correctness properties of a neural network for providing estimates
and, more particularly, to a system for proving correctness
properties of a neural network for providing estimates based on
point cloud data.
(2) Description of Related Art
[0005] Neural network based systems for providing estimates from
point cloud data (e.g., of the kind generated by lidar or stereo
camera systems) have become more prominent in the past several
years (see, for instance, Literature References No. 7 and 9 of the
List of Incorporated Literature References). At the same time, many
questions have been raised regarding the reliability and robustness
of neural network based systems (see Literature Reference Nos. 2
and 5), which makes it more pressing to be able to provide strong
guarantees on the behavior of these kinds of systems. Recent work
in analysis and verification of neural networks has focused almost
exclusively on attempting to provide guarantees regarding what is
called adversarial robustness, which is robustness in the face of
small perturbations of inputs. In this context, the specification
(i.e., definition of what it means for the system to be correct)
considered is connected to so-called local adversarial
robustness.
[0006] Katz et al. (see Literature Reference No. 8) and Wong and
Kolter (see Literature Reference No. 11) describe work on
verification of neural networks. Their work is only concerned with
the perception domain with pixel image input and not with point
cloud data. Additionally, local adversarial robustness is a weak
correctness property for several reasons (e.g., dependence on a
finite set of fixed inputs and a fixed norm). The notion of
correctness embodied in local adversarial robustness is that the
neural network does not change its output when the input is
perturbed by a perturbation with bounded norm, which says nothing
about the general correctness of the neural network.
[0007] The prior art is concerned exclusively with image (pixel)
data and with the typical machine learning benchmark datasets for
image based classification tasks, such as the MNIST handwritten
digit dataset, where the goal is to classify images of handwritten
digits. In the context of classification, the problem of defining
correctness in a mathematically precise way is very different from
the case of geometric tasks of the kind considered when working
with point cloud data. For this reason, looking at stronger
geometric correctness properties does not make sense for the
applications being considered by the prior art in this area.
Moreover, the satisfaction modulo theories (SMT) or mixed integer
linear programing (MILP) based tools that have been employed in the
prior art are not capable of reasoning about the trigonometric
functions that occur prominently in analysis for the case of
estimating surface normals.
[0008] Thus, a continuing need exists for a system for analysis of
correctness properties of a neural network for providing estimates
of surface normals for point cloud data.
SUMMARY OF INVENTION
[0009] The present invention relates to a system for proving
correctness properties of a neural network for providing estimates
for data and, more particularly, to a system for proving
correctness properties of a neural network for providing estimates
for point cloud data. The system comprises 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 multiple operations. The system receives,
as input, a concrete description of a neural network for generating
estimates from a set of point cloud data, wherein the concrete
description of the neural network is in one of a source code format
or a serialized format. 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, an
analysis output indicating whether the neural network satisfies a
correctness property in generating the estimates from the set of
point cloud data is generated. 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.
[0010] In another aspect, the analysis output acts as a stopping
condition for preventing deployment of the neural network.
[0011] In another aspect, the estimates comprise an estimate of a
slope of a patch of the set of point cloud data.
[0012] In another aspect, the estimates comprise an estimate of a
surface normal of a patch of the set of point cloud data.
[0013] In another aspect, the estimates comprise an estimate
regarding whether a patch of the set of point cloud data is ground
or non-ground.
[0014] In another aspect, the set of analysis parameters describe
geometric properties of the set of point cloud data.
[0015] Finally, the present invention also includes a computer
readable program and a computer implemented method. The computer
readable program includes computer-readable instructions stored on
a non-transitory computer-readable medium that are executable by a
computer having one or more processors, such that upon execution of
the instructions, the one or more processors perform the operations
listed herein. Alternatively, the computer implemented method
includes an act of causing a computer to execute such instructions
and perform the resulting operations.
BRIEF DESCRIPTION OF THE DRAWINGS
[0016] The objects, features and advantages of the present
invention will be apparent from the following detailed descriptions
of the various aspects of the invention in conjunction with
reference to the following drawings, where:
[0017] FIG. 1 is a block diagram depicting the components of a
system for proving correctness properties of a neural network for
providing estimates for point cloud data according to some
embodiments of the present disclosure;
[0018] FIG. 2 is an illustration of a computer readable program
according to some embodiments of the present disclosure;
[0019] FIG. 3 is an illustration of a point cloud from an
environment with box-shaped obstacles according to some embodiments
of the present disclosure;
[0020] FIG. 4 is an illustration of neural network based lidar
processing according to some embodiments of the present
disclosure;
[0021] FIG. 5 is an illustration of modules in the system for
analysis of correctness properties of a neural network for
providing estimates for point cloud data. according to some
embodiments of the present disclosure;
[0022] FIG. 6A is an illustration of a first neural network
architecture for estimating surface normals of point cloud patches
according to some embodiments of the present disclosure;
[0023] FIG. 6B is an illustration of a second neural network
architecture for estimating surface normals of point cloud patches
according to some embodiments of the present disclosure;
[0024] FIG. 7 is an illustration of a counter-example obtained for
the case of surface normal according to some embodiments of the
present disclosure;
[0025] FIG. 8 is an illustration of test points and disjoint sets
F.sub.1 as y-balls according to some embodiments of the present
disclosure; and
[0026] FIG. 9 is a flow diagram illustrating a system for analysis
of correctness properties of a neural network for providing
estimates for point cloud data. according to some embodiments of
the present disclosure.
DETAILED DESCRIPTION
[0027] The present invention relates to a system for proving
correctness properties of a neural network for providing estimates
for data and, more particularly, to a system for proving
correctness properties of a neural network for providing estimates
from point cloud data. The following description is presented to
enable one of ordinary skill in the art to make and use the
invention and to incorporate it in the context of particular
applications. Various modifications, as well as a variety of uses
in different applications will be readily apparent to those skilled
in the art, and the general principles defined herein may be
applied to a wide range of aspects. Thus, the present invention is
not intended to be limited to the aspects presented, but is to be
accorded the widest scope consistent with the principles and novel
features disclosed herein.
[0028] In the following detailed description, numerous specific
details are set forth in order to provide a more thorough
understanding of the present invention. However, it will be
apparent to one skilled in the art that the present invention may
be practiced without necessarily being limited to these specific
details. In other instances, well-known structures and devices are
shown in block diagram form, rather than in detail, in order to
avoid obscuring the present invention.
[0029] The reader's attention is directed to all papers and
documents which are filed concurrently with this specification and
which are open to public inspection with this specification, and
the contents of all such papers and documents are incorporated
herein by reference. All the features disclosed in this
specification, (including any accompanying claims, abstract, and
drawings) may be replaced by alternative features serving the same,
equivalent or similar purpose, unless expressly stated otherwise.
Thus, unless expressly stated otherwise, each feature disclosed is
one example only of a generic series of equivalent or similar
features.
[0030] Furthermore, any element in a claim that does not explicitly
state "means for" performing a specified function, or "step for"
performing a specific function, is not to be interpreted as a
"means" or "step" clause as specified in 35 U.S.C. Section 112,
Paragraph 6. In particular, the use of "step of" or "act of" in the
claims herein is not intended to invoke the provisions of 35 U.S.C.
112, Paragraph 6.
[0031] Before describing the invention in detail, first a list of
cited references is provided. Next, a description of the various
principal aspects of the present invention is provided. Finally,
specific details of various embodiment of the present invention are
provided to give an understanding of the specific aspects.
(1) LIST OF INCORPORATED LITERATURE REFERENCES
[0032] The following references are cited and incorporated
throughout this application. For clarity and convenience, the
references are listed herein as a central resource for the reader.
The following references are hereby incorporated by reference as
though fully set forth herein. The references are cited in the
application by referring to the corresponding literature reference
number, as follows: [0033] 1. Barrett, C., Stump, A., &
Tinelli, C. (2010). The SMT-LIB Standard--Version 2.0. SMT.
Edinburgh. [0034] 2. Cao, Y., Xiao, C., Cyr, B., Zhou, Y., Park,
W., Rampazzi, S., . . . Mao, Z. M. (2019). Adversarial Sensor
Attack on LiDAR-based Perception in Autonomous Driving. ACM
Conference on Computer and Communications Security. [0035] 3.
Facebook. (2020, Feb. 19). PyTorch. Retrieved from
https://pytorch.org. [0036] 4. Gao, S., Kong, S., & Clarke, E.
M. (2013). dReal: An SMT solver for nonlinear theories over the
reals. CADE. [0037] 5. Goodfellow, I., Shlens, J., & Szegedy,
C. (2015). Explaining and harnessing adversarial examples. ICLR.
[0038] 6. Google. (2020, Feb. 19). TensorFlow. Retrieved from
https://tensorflow.org. [0039] 7. Guerrero, P., Kleiman, Y.,
Ovsjanikov, M., & Mitra, N. J. (2018). PCPNet: Learning local
shape properties from raw point clouds. Computer Graphics Forum,
75-85. [0040] 8. Katz, G., Barrett, C. W., Dill, D. L., Julian, K.,
& Kochenderfer, M. J. (2017). Reluplex: An efficient SMT solver
for verifying deep neural networks. CAV, (pp. 97-117). [0041] 9.
Qi, C. R., Su, H., Mo, K., & Guibas, L. J. (2017). PointNet:
Deep learning on point sets for 3D classification and segmentation.
The IEEE Conference on Computer Vision and Pattern Recognition
(CVPR). [0042] 10. The Linux Foundation. (2020, Feb. 19). Open
Neural Network Exchange (ONNX). Retrieved from https://onnx.ai.
[0043] 11. Wong, E., & Kolter, J. Z. (2018). Provable defenses
against adversarial examples via the convex outer adversarial
polytope. ICML.
(2) PRINCIPAL ASPECTS
[0044] Various embodiments of the invention include three
"principal" aspects. The first is a system for proving correctness
properties of a neural network for providing estimates for point
cloud data. The system is typically in the form of a computer
system operating software or in the form of a "hard-coded"
instruction set. This system may be incorporated into a wide
variety of devices that provide different functionalities. The
second principal aspect is a method, typically in the form of
software, operated using a data processing system (computer). The
third principal aspect is a computer readable program. The computer
readable program generally represents computer-readable
instructions stored on a non-transitory computer-readable medium
such as an optical storage device, e.g., a compact disc (CD) or
digital versatile disc (DVD), or a magnetic storage device such as
a floppy disk or magnetic tape. Other, non-limiting examples of
computer-readable media include hard disks, read-only memory (ROM),
and flash-type memories. These aspects will be described in more
detail below.
[0045] A block diagram depicting an example of a system (i.e.,
computer system 100) of the present invention is provided in FIG.
1. The computer system 100 is configured to perform calculations,
processes, operations, and/or functions associated with a program
or algorithm. In one aspect, certain processes and steps discussed
herein are realized as a series of instructions (e.g., software
program) that reside within one or more computer readable memory
units and are executed by one or more processors of the computer
system 100. When executed, the instructions cause the computer
system 100 to perform specific actions and exhibit specific
behavior, such as described herein.
[0046] The computer system 100 may include an address/data bus 102
that is configured to communicate information. Additionally, one or
more data processing units, such as a processor 104 (or
processors), are coupled with the address/data bus 102. The
processor 104 is configured to process information and
instructions. In an aspect, the processor 104 is a microprocessor.
Alternatively, the processor 104 may be a different type of
processor such as a parallel processor, application-specific
integrated circuit (ASIC), programmable logic array (PLA), complex
programmable logic device (CPLD), or a field programmable gate
array (FPGA).
[0047] The computer system 100 is configured to utilize one or more
data storage units. The computer system 100 may include a volatile
memory unit 106 (e.g., random access memory ("RAM"), static RAM,
dynamic RAM, etc.) coupled with the address/data bus 102, wherein a
volatile memory unit 106 is configured to store information and
instructions for the processor 104. The computer system 100 further
may include a non-volatile memory unit 108 (e.g., read-only memory
("ROM"), programmable ROM ("PROM"), erasable programmable ROM
("EPROM"), electrically erasable programmable ROM "EEPROM"), flash
memory, etc.) coupled with the address/data bus 102, wherein the
non-volatile memory unit 108 is configured to store static
information and instructions for the processor 104. Alternatively,
the computer system 100 may execute instructions retrieved from an
online data storage unit such as in "Cloud" computing. In an
aspect, the computer system 100 also may include one or more
interfaces, such as an interface 110, coupled with the address/data
bus 102. The one or more interfaces are configured to enable the
computer system 100 to interface with other electronic devices and
computer systems. The communication interfaces implemented by the
one or more interfaces may include wireline (e.g., serial cables,
modems, network adaptors, etc.) and/or wireless (e.g., wireless
modems, wireless network adaptors, etc.) communication technology.
Further, one or more processors 104 (or devices, such as autonomous
platforms) can be associated with one or more associated memories,
where each associated memory is a non-transitory computer-readable
medium. Each associated memory can be associated with a single
processor 104 (or device), or a network of interacting processors
104 (or devices), such as a network of autonomous platforms (e.g.,
autonomous vehicles, robots).
[0048] In one aspect, the computer system 100 may include an input
device 112 coupled with the address/data bus 102, wherein the input
device 112 is configured to communicate information and command
selections to the processor 104. In accordance with one aspect, the
input device 112 is an alphanumeric input device, such as a
keyboard, that may include alphanumeric and/or function keys.
Alternatively, the input device 112 may be an input device other
than an alphanumeric input device. In an aspect, the computer
system 100 may include a cursor control device 114 coupled with the
address/data bus 102, wherein the cursor control device 114 is
configured to communicate user input information and/or command
selections to the processor 104. In an aspect, the cursor control
device 114 is implemented using a device such as a mouse, a
track-ball, a track-pad, an optical tracking device, or a touch
screen. The foregoing notwithstanding, in an aspect, the cursor
control device 114 is directed and/or activated via input from the
input device 112, such as in response to the use of special keys
and key sequence commands associated with the input device 112. In
an alternative aspect, the cursor control device 114 is configured
to be directed or guided by voice commands.
[0049] In an aspect, the computer system 100 further may include
one or more optional computer usable data storage devices, such as
a storage device 116, coupled with the address/data bus 102. The
storage device 116 is configured to store information and/or
computer executable instructions. In one aspect, the storage device
116 is a storage device such as a magnetic or optical disk drive
(e.g., hard disk drive ("HDD"), floppy diskette, compact disk read
only memory ("CD-ROM"), digital versatile disk ("DVD")). Pursuant
to one aspect, a display device 118 is coupled with the
address/data bus 102, wherein the display device 118 is configured
to display video and/or graphics. In an aspect, the display device
118 may include a cathode ray tube ("CRT"), liquid crystal display
("LCD"), field emission display ("FED"), plasma display, or any
other display device suitable for displaying video and/or graphic
images and alphanumeric characters recognizable to a user.
[0050] The computer system 100 presented herein is an example
computing environment in accordance with an aspect. However, the
non-limiting example of the computer system 100 is not strictly
limited to being a computer system. For example, an aspect provides
that the computer system 100 represents a type of data processing
analysis that may be used in accordance with various aspects
described herein. Moreover, other computing systems may also be
implemented. Indeed, the spirit and scope of the present technology
is not limited to any single data processing environment. Thus, in
an aspect, one or more operations of various aspects of the present
technology are controlled or implemented using computer-executable
instructions, such as program modules, being executed by a
computer. In one implementation, such program modules include
routines, programs, objects, components and/or data structures that
are configured to perform particular tasks or implement particular
abstract data types. In addition, an aspect provides that one or
more aspects of the present technology are implemented by utilizing
one or more distributed computing environments, such as where tasks
are performed by remote processing devices that are linked through
a communications network, or such as where various program modules
are located in both local and remote computer-storage media
including memory-storage devices.
[0051] An illustrative diagram of a computer readable program
(i.e., storage device) embodying the present invention is depicted
in FIG. 2. The computer readable program is depicted as floppy disk
200 or an optical disk 202 such as a CD or DVD. However, as
mentioned previously, the computer readable program generally
represents computer-readable instructions stored on any compatible
non-transitory computer-readable medium. The term "instructions" as
used with respect to this invention generally indicates a set of
operations to be performed on a computer, and may represent pieces
of a whole program or individual, separable, software modules.
Non-limiting examples of "instruction" include computer program
code (source or object code) and "hard-coded" electronics (i.e.
computer operations coded into a computer chip). The "instruction"
is stored on any non-transitory computer-readable medium, such as
in the memory of a computer or on a floppy disk, a CD-ROM, and a
flash drive. In either event, the instructions are encoded on a
non-transitory computer-readable medium.
(3) SPECIFIC DETAILS OF VARIOUS EMBODIMENTS
[0052] Neural network based systems for providing estimates from
point cloud data (e.g., of the kind generated by lidar or stereo
camera systems) have become more prominent in the past several
years (see Literature Reference Nos. 7 and 9). At the same time,
many questions have been raised regarding the reliability and
robustness of neural network based systems (see Literature
Reference Nos. 2 and 5), which makes it more pressing to be able to
provide strong guarantees on the behavior of these kinds of
systems. Recent work in analysis and verification of neural
networks has focused almost exclusively on the attempting to
provide guarantees regarding what is called adversarial robustness:
robustness in the face of small perturbations of inputs. FIG. 3
depicts an example of a point cloud from an environment with
box-shaped obstacles. Light grey points (e.g., 300) represent
ground plane, and dark grey points (e.g., 302) represent non-ground
plane.
[0053] One specification, or definition of what it means for the
system to be correct, considered in the literature is so-called
local adversarial robustness. Explicitly, where X is the input
space (e.g., the space of pixel images) and Y is the output space
(e.g., the space of classifications such as "cat", "dog", etc.),
the neural network estimator can itself be thought of as a map f:
X.fwdarw.Y. In this context, local adversarial robustness states
that, for a fixed finite batch of inputs BX, there is image b E B
and no perturbation .pi. with norm
.parallel..pi..parallel.<.delta. such that f(b).noteq.f(b+.pi.).
Several remarks regarding this definition are in order. First, the
"local" in this definition refers to the fact that although this
property quantifies over all possible perturbations bounded in norm
by .delta., the set of images over which the guarantee holds is
merely finite. Second, to state this property one must first fix a
norm .parallel.-.parallel., but the question of which norm is well
suited to the actual data distribution is non-trivial. Thus, local
adversarial robustness provides somewhat weaker guarantees than
might be hoped.
[0054] The invention described herein is concerned with attempting
to provide more meaningful guarantees than those of local
adversarial robustness in the case where the input space X is a
space of point cloud data (e.g., of the kind coming from lidar or
stereo camera) and where the task of the neural network f is to
make one of the following kinds of estimates: (1) to estimate the
surface normal vector in three-dimensional Euclidean space; (2) to
estimate whether or not the input points constitute a ground
(roughly flat) or non-ground plane; and (3) to estimate other
geometric properties (e.g., curvature) from point cloud data where
a ground truth on certain representative data can be determined
analytically. Task (1) itself can be used as part of the solution
to (2), but these can also be separate tasks. An example of where
these tasks are relevant is given by providing an estimate of where
an autonomous ground vehicle can safely drive. For example,
obstacles (such as pedestrians or buildings) would be tagged as
non-ground plane. An observation is that, in these cases, there is
a natural norm (the standard norm of three-dimensional Euclidean
space) on the space X that is relevant to the properties being
estimated. The present invention leverages this crucial
observation.
[0055] Given the source code, mathematical description, or
serialized format (e.g., TensorFlow or PyTorch saved model) of a
neural network f that aims to address one of the tasks (1) or (2),
the present invention is a method for automatically generating
either (a) a mathematical proof that, for any point cloud
x.di-elect cons.X of a certain kind, the neural network f will
produce a correct estimate f(x); or (b) a potential counter-example
x.di-elect cons.X such that f(x) is an incorrect estimate. A
detailed description of the input parameters to the process
described herein, the conditions/limitations on the point clouds to
which the process applies, and the output of the process, a
mathematical proof (which can be regarded as text data) or a
concrete point-cloud, is provided below. The invention described
herein provides a more thorough analysis of the correctness of a
neural network for carrying out one of the tasks (1) or (2) above.
Current state-of-the art approaches to this problem are based
purely on extensive testing or else using adversarial machine
learning. The disadvantages of these two approaches is that they
only provide a means to obtain counter-examples ((b) above). The
prior testing approach, in particular, by its very nature can only
provide guarantees over a finite range of inputs.
[0056] The invention described herein is directed to the analysis
of the source code or serialized representations of neural networks
for analyzing point cloud data. The input is a concrete description
(i.e., source code or serialized representation) of a neural
network which could be a mathematical (symbolic) description or
source code including saved values for all parameters (matrix
weights, bias vectors, convolutional kernels, etc.) of the network.
The input space of the neural network to be analyzed must be of the
form .sup.3n (i.e., inputs must be n-tuples of three floating point
values where these values correspond to x-, y-, and z-coordinates
of a point in Euclidean space). The output of the neural network to
be analyzed must be either: the estimate of a surface normal (and
therefore a three-tuple of floating point values); the estimate of
a slope; the estimate of ground or non-ground plane; or the
estimate of another geometric property for which the ground-truth
value can be calculated analytically for a mathematically
well-defined class of representative examples.
[0057] One example, where the sensor that produces the data to be
consumed by the neural network is a lidar sensor, is shown in FIG.
4. Given a non-ground plane object 400, the lidar sensor 402 (and
its firmware) generates point cloud data 404 that is then (possibly
after some pre-processing) consumed by the neural network f 406.
Pre-processing could include clustering points into batches for
multiple smaller collections of points that are closer in space
rather than a gigantic point cloud that is dispersed over the
entire field-of-view. Pre-processing can also include centering or
scaling the point cloud, and similar geometric operations. Such
pre-processing will be familiar to one skilled in the art of
machine learning. Some kind of pre-processing is often needed to
improve performance of machine learning systems and admit scalable
computation (e.g., feeding a gigantic point cloud to a neural
network might be a bottleneck to real-time operation).
[0058] It is assumed that a description artifact that completely
describes the neural network f 406 is given. Crucially, this
artifact should contain sufficient information to be able to
completely recreate the network. In particular, the description
artifact should consist either of the source code (including saved
weights) or a serialized representation of the neural network.
Non-limiting examples of description artifacts include networks
stored in ONNX (see Literature Reference No. 10), TensorFlow (see
Literature Reference No. 6), or PyTorch (see Literature Reference
No. 3) serialization formats.
[0059] It is assumed that the neural network f 406 has, as its
input, point clouds 404 of a fixed size n. Thus, f 406 can be
described mathematically as a function .sup.3n.fwdarw.Y where the
output space Y, which consists of estimates 408, is determined by
the particular task of f 406. Concretely this means that f 406 is
realized in source code by a function that takes as input n-many
triples of floating point values (which could be captured in code
as a list of such values) and returns a corresponding value of the
appropriate type (typically also a list of floating point values).
There are several additional parameters that the invention
requires. The following are parameters for the ground plane
segmentation task: the description artifact; a coordinate system
for Euclidean space fixed (e.g., cartesian x-, y-, z-coordinates,
spherical coordinates (r, .phi., .nu.) with .phi. the azimuthal
angle and .nu. the polar angle); n many (compact and convex)
subsets F.sub.1, . . . , F.sub.n of .sup.2 that are definable by
formulas in the language of first-order real arithmetic with common
non-linear function symbols (see below for examples); a tolerance
constant .epsilon.>0; and any additional implementation specific
constant values (see below for examples). Analogous parameters are
required for estimation of surface normals or slopes, and these
would be evident to one skilled in the art.
[0060] A high-level overview of the invention is depicted in FIG.
5. Here, the Parsing module 500 transforms the neural network
description artifact 502 into a symbolic representation 504 that
mathematically corresponds to an expression in first-order real
arithmetic with common non-linear function symbols. The nature of
the Parsing module 500 and symbolic representation 504 will vary in
different reductions to practice (e.g., depending on the agreed
upon description artifact 502 format). As an example, suppose the
neural network f in question is the scalar map .fwdarw. consisting
of an affine transformation x0.5 x+1.0 followed by a sigmoid
activation (i.e., f (x)=.sigma.(0.5x+1.0)). Then, the symbolic
representation 504 in SMT-LIB format (see Literature Reference No.
1) would be:
(define-funf((x Real))Real(sigmoid(+(*0.5x)1.0))
assuming the sigmoid function has already been declared/defined.
The line above (and those below) are examples of code written in a
SMT-LIB programming language corresponding to the definition of the
mathematical function described above, as known to one skilled in
the art. Once the symbolic representation 504 has been obtained by
parsing the description artifact 502, it is fed together with the
analysis parameters 506 to the Analyzer module 508. For each i=1, .
. . , n, the Analyzer module 508 creates pairs (r.sub.i,
.phi..sub.i) of symbolic variables ranging over real numbers and
corresponding to two-dimensional planar data (here represented for
expositional purposes in spherical coordinates, although other
coordinate systems can be used). As above, the concrete
representation of the symbolic variables will vary depending on the
specific features of the experimental studies (e.g., they could
correspond to SMT-LIB variable declarations of the form: [0061]
(declare-fun r1 ( ) Real) [0062] (declare-fun r2( ) Real).
[0063] The ensemble of symbolic variables (r.sub.i, .phi..sub.i)
represents a planar patch in the two-dimensional Euclidean plane in
spherical coordinates (i.e., with azimuthal angle .phi..sub.i and
polar angle 0). The Analyzer module 508 also creates variables .nu.
corresponding to rotations of the planar patch (r.sub.i,
.phi..sub.i).sub.i in three-dimensional space. Depending on the
precise task, it may be necessary to create either a single
variable or multiple variables. Thus, .nu. might represent a tuple.
Denote by p the planar patch of variables and by p*.nu. the result
of rotating this planar patch by the angle(s).nu.. The precise
details of the mathematical formula required to express this
rotation will depend on the choice of coordinate system and the
nature of the constraint (e.g., ground plane segmentation or
estimate of surface normal) being considered. The precise details
in each of these cases will be straightforward for one skilled in
the art. The Analyzer module 508 then creates the (symbolic)
formula .PHI..sub.i defined mathematically as:
(r.sub.i,.phi..sub.i).di-elect cons.F.sub.i.
Denote by .PHI. the conjunction:
(0<.nu.<.epsilon.) .sub.i.PHI..sub.i.
This symbolic formula is constructed symbolically in the Analyzer
module 508, and it represents initial conditions on the variables
employed in the analysis of the neural network. As above, such
symbolic formulae will be captured differently depending on the
details of the embodiment of the invention (in particular, the
choice of SMT solver). In SMT-LIB format, the foregoing symbolic
formula can be realized as: [0064] (and (and (<0 theta)
(<theta epsilon)) big_and_phi_i), where big_and_phi_i is the
large conjunction that has already been declared. Note that in
order for the verification to be sufficiently meaningful, it is
important to carefully select the input F.sub.i. For example, these
should be such that any collection of points satisfying condition
.PHI. must necessarily contain some non-colinear triple and, for
practical reasons, they should contain at least one non-colinear
triple that are not too close (what counts as not too close is
itself subject to the particular reduction to practice and the
additional constants required therein, but should be easily
determined by one skilled in the art).
[0065] The Analyzer module 508 then constructs the (symbolic)
formulas which state that the neural network estimator satisfies
the appropriate correctness property. Start by considering the case
of ground/non-ground classification. Where f (x) denotes the output
ground/non-ground classification of the neural network when
provided as input the patch x, the solving task is to show that
f(p*.xi.) yields the classification: [0066] Ground, when the
initial angle is .nu.=0 and d(.nu.,.xi.)<.epsilon.; or [0067]
Non-ground, when the initial angle is
[0067] = .pi. 2 .times. .times. and .times. .times. d .function. (
, .xi. ) < . ##EQU00001##
The cases of estimating surface normals and slopes are similar.
[0068] Once the Analyzer module 508 has constructed this symbolic
formula, it is passed as a query 510 (i.e., the symbolic formula),
together with any additional parameters (e.g., timeouts, precision
values, etc.), to the SMT solver 512, which carries out its
analysis and returns a response 514. The details of how this is
handled will be familiar to anyone skilled in the art of using an
SMT solver. The Analyzer module 508 then processes this response
514 (e.g., to confirm whether or not a potential counter-example is
correct) and returns analysis outputs 516 indicating whether or not
the neural network satisfies the correctness property or if a
solution could not be found. In the case where the neural network
has been shown to fail to satisfy the correctness property, a
counter-example will be returned consisting of instantiations of
the variables described above as concrete floating point
values.
[0069] There are three possible kinds of analysis outputs 516 (or
indicators): a proof artifact that captures the mathematical
reasoning required to prove that the rule is satisfied, a concrete
point cloud (i.e., a data structure) or list of such point clouds
for which the rule is violated, or a report that sufficient
progress could not be made by the analysis (in which case the user
would likely modify analysis parameters and try again). These
outputs 516 may then be used in a variety of ways. For instance,
the analysis outputs 516 can be used to determine what further data
should be collected and trained on (in cases of failure) before the
neural network is deployed. In this way, the outputs 516 (or
indicators) act as a stopping condition preventing the neural
network from being deployed. The analysis outputs 516 can also be
provided to regulators as part of a certification process. In
addition, the analysis outputs 516 can be used by security experts
to analyze potential system vulnerabilities arising due to failures
identified by this analysis (in the case of counter-examples).
Further, the outputs can be fed-back into the training process
directly to improve the training of the neural network. In summary,
the analysis outputs 516 can be utilized to inform future training,
provided as evidence to regulators for certification purposes, fed
back directly into the training system in order to augment the
original training, and/or utilized by security teams in their
inspection of the system for certification or other purposes.
[0070] In a first experimental study, the invention was applied to
the case of neural networks for estimating surface normals of point
cloud patches. In this case, the coordinate system was cartesian
and the neural networks considered had architectures of one of the
forms illustrated in FIGS. 6A and 6B. The studies were carried out
using a combination of Python and C++ code and the SMT solver 512
that used was the dReal SMT solver (see Literature Reference No.
4). The neural network description artifacts 502 were in the
TensorFlow serialized model format. A unitless example of a
counter-example analysis output 516 for the case of surface normals
obtained as part of this experimental study is shown in FIG. 7. In
this experimental study, the sets F.sub.1 were defined as regularly
spaced disjoint rectangular subsets of the unit box [-1,1].sup.2
arranged in a grid with two rows and >1 rows to ensure
non-degenerate counter-examples would be found. In this case, the
rotation was specified by two separate angles of rotation. The dots
700 in FIG. 7 represent the points in the point cloud.
[0071] In a second experimental study, neural networks were
considered for ground plane segmentation (i.e., classifying whether
or not a patch consists of ground plane). As above, the dReal SMT
solver 512 was used ibid. The neural network description artifacts
502 were in the PyTorch neural network serialization format. The
neural networks considered used an architecture that is not
described here. The coordinate system was spherical and the
rotation was specified in terms solely of the polar angle D. The
sets F.sub.1 were defined by first selecting fixed "test points"
u.sub.i (e.g., at (0,0), (-1,0), (1,0), (0,-1), (-1,-1) and (1,1))
and then adding as a parameter a value .gamma.>0 such that
F.sub.1 is defined to be the y-ball (element 800) centered at
u.sub.i, which is illustrated in FIG. 8. Specifically, FIG. 8
depicts test points and disjoint sets F.sub.i as y-balls (i.e.,
sets of the form {x|d(x,u.sub.i)<.gamma.}, where d(-,-) denotes
the standard Euclidean metric (element 800). In this case, the code
was a mixture of Python and C++ code. Not only were
counter-examples found, but also proofs of correctness of ground
plane segmentation.
[0072] FIG. 9 is a flow diagram illustrating a system for analysis
of correctness properties of a neural network for providing
estimates for point cloud data. according to some embodiments of
the present disclosure. As described in detail above, a neural
network based estimate related to a set of point cloud data is
received (element 900). A description of the neural network is
transformed into a symbolic representation (element 902). Based on
a combination of the symbolic representation and a set of
parameters, an analysis output indicating whether the neural
network satisfies a correctness property in generating the neural
network based estimate is generated (element 904).
[0073] Current state-of-the-art approaches to the problem of
defining correctness are based purely on extensive testing or else
using adversarial machine learning. The principal disadvantage of
these two approaches is that they only provide a means to obtain
counter-examples, whereas the invention described herein enables
the user to obtain a proof artifact that imparts mathematical
correctness guarantees on the point cloud processor. Such proof
artifacts can be used by regulators, certifiers, or quality
assurance departments to augment their standard testing approaches
in order to obtain better insight into the reliability and
trustworthiness of the point cloud processors being analyzed. For
example, the standard testing approach could be improved based on
the outputs of this invention by collecting further point cloud
data to test that is near the conditions identified as yielding
incorrect estimates by the invention. Additionally, when point
clouds are found that violate the rules, these point clouds can be
used to augment the training or test set of the neural network,
thereby improving network performance.
[0074] Additionally, existing methods for verification of neural
networks are concerned exclusively with image (pixel) data and with
the typical machine learning benchmark datasets for image based
classification tasks. In the context of classification, the problem
of defining correctness in a mathematically precise way is very
different from the case of geometric tasks of the kind considered
when working with point cloud (instead of image) data. For this
reason, looking at stronger geometric correctness properties does
not make sense for the applications being considered by the prior
art in this area. Moreover, the satisfaction modulo theories (SMT)
or mixed integer linear programing (MILP) based tools that have
been employed in the prior art are not capable of reasoning about
the trigonometric functions that occur prominently in the
specification of geometric correctness properties (the rules
described above) for point cloud data. Because an alternative
approach is being used in the method according to embodiments of
the present disclosure, which instead uses the dReal SMT solver of
Literature Reference No. 4 that is capable of manipulating
trigonometric functions, one can formulate and reason about the
natural correctness conditions related to point cloud data, as
described above.
[0075] The present invention can be applied to any program or
product line that utilizes neural network based systems for
processing point cloud data, such as autonomous or semi-autonomous
vehicle platforms that utilize lidar or stereo camera systems. As
described above, the present invention can be used either for
quality assurance of neural network based point cloud processors or
to generate point cloud data that can be utilized to improve
training. In particular, the invention is analogous to source code
analysis systems, such as described in U.S. Pat. No. 10,423,518
(which is hereby incorporated by reference as though fully set
forth herein), in that it takes as input the source code
description of the neural network based point cloud processor,
carries out an analysis of that source code to check against
"rules" (in this case, the rules correspond to the properties of
tasks (1)-(3) of interest described above), and then shares the
outputs of that analysis with the user.
[0076] In one non-limiting example, the invention described herein
is used to evaluate whether or not an autonomous system platform is
actually safe to operate. A goal of the present invention is to
help prevent a system that is likely to fail from being deployed.
Thus, the invention is configured to be used at design time (or to
provide data to regulators for certification purposes). Analysis
outputs inform for what kind of data failures are or are not likely
to occur. An example of a failure is an autonomous vehicle hitting
a pedestrian. In this type of situation, it is likely that the
perception system failed to correctly detect a pedestrian and
failed to brake before hitting the pedestrian.
[0077] Finally, while this invention has been described in terms of
several embodiments, one of ordinary skill in the art will readily
recognize that the invention may have other applications in other
environments. It should be noted that many embodiments and
implementations are possible. Further, the following claims are in
no way intended to limit the scope of the present invention to the
specific embodiments described above. In addition, any recitation
of "means for" is intended to evoke a means-plus-function reading
of an element and a claim, whereas, any elements that do not
specifically use the recitation "means for", are not intended to be
read as means-plus-function elements, even if the claim otherwise
includes the word "means". Further, while particular method steps
have been recited in a particular order, the method steps may occur
in any desired order and fall within the scope of the present
invention.
* * * * *
References