I can't proof that the neutral network always behaves correctly, but with testing and statistics you can verify the network up to a chosen certainty (below 100% obviously). Or you can actively search for problems with fuzzing techniques. All without solving the halting problem.
So you'll end up with ANN's reviewing other ANN's which are reviewed by other ANN's at the end.
You can test ANN's by simply fuzzing them and seeing the output, getting much insight to why an outcome was chosen for a given data set is near impossible.
https://people.cs.umass.edu/~btaylor/publications/PSI000008....
These are also just the first steps. Not bad given what hardware and software verification used to look like a few decades ago. I think the verifiable ANN's will be more structured or constrained in their development or even use cases.
"it's simply beyond the human capability to review. So you'll end up with ANN's reviewing other ANN's which are reviewed by other ANN's at the end."
That implied it was beyond human capability to review ANN's to the point we'd need ANN's to do it. In the paper, they give a number of deterministic methods to review ANN's noting some were successful by the teams using them. Countered both of your claims in that context.
"This means that having the ANN being open sourced does not add additional security by having the code inspectable by everyone like with traditional software."
I agree that most of the problems won't be caught here. More about training set and safety monitors. However, the paper shows methods like rule extraction, visualization, and simulation that have aided in assessing and improving neural networks. These work on that internal state that's incomprehinsible at first glance. It's also usually stored in HW logic, the SW code, or some data format. Having those provably facilitates analysis of ANN's performance. Assuming it's the kind that's analyzable at all. ;)
Note: Code-level errors, either by hand-written or auto-generated engines, can also invalidate an ANN's behavior. Vast majority of software flaws occur right here. Obviously, some static analysis or safety transformations can increase assurance of correctness of overall system. Should be combined with other V&V methods.
If you get a the source code of any traditional software reviewing the code can be done by humans regardless of how complex it is, with ANN's it's not really the case simply because of the nondeterministic nature of the system. You can validate the "correctness" of an ANN but it's not done in the same manner as reviewing traditional software.
You have to do both: validate the non-deterministic aspects of the ANN logic and validate its implementation as code. Makes them a lot harder. One reason I avoid them.