It is interesting to consider that the Mongol conquests in Asia, much like the Spanish conquests in America, were facilitated by a weapon they did not know they had.
Cleanly connecting NNs to contracts / rules is indeed a hard problem, which many people would like to see solved. Please see my post about that [1], and the corresponding HN comment thread [2].
Right - as far as I know most ANNs _are_ embedded in some pipeline which contains also "regular" SW, and thus by definition there _is_ some way to connect them to a rule-based system.
The only issue is that there is no easy, _natural_ way to do it. For instance, consider the various attempts at adding safety rules to an RL ANN (depicted in fig. 2 in the paper). Say that (in the context of an ANN controlling an Autonomous Vehicle) your ANN decided to do something on the freeway, but the safety rules say "no". There is no easy way to gracefully integrate the rule and ANN: One way is for the rule to disable the ANN's output at this point, take full control and decide what the AV _should_ do. But this leads to duplication and complexity.
So the four solutions I describe take various ways to avoid this problem. They all "work" in a sense, but none does real "integration" of the ANN and the rules (the shield synthesis solution perhaps comes closest). And it looks like you have to invent this kind of solution anew for every new instance of connecting-ANN-to-rules.
And this was just "inserting rules during execution". Then there is the issue of "verifying via rules", and "explaining the rules". It is tough, and I am wondering if there could be some conceptual breakthrough which would make it somewhat easier.
1. Most ML techniques are bad at connecting to rules (random trees and inductive logic programming are a small subset).
2. Most of the ML techniques that one encounters in practice while verifying intelligent autonomous systems are currently neural-network-based: Sensor fusion in the AV itself, coverage maximization attempts I am currently aware of in the verification environment, and so on.
I suspect that most ML techniques, by their nature, will not play nice with rules by default. But this is just a hunch.
That is my opinion as well. And indeed the post talks mainly about dynamic verification and achieving some "good enough" verification quality (as determined by coverage and other metrics).
And it is in that context that "soft" techniques like ML can help a lot, and thus the question of how to connect them to "hard" rules (which are also part of dynamic verification) becomes interesting.
I indeed meant it in the philosophical sense you describe. But I am very interested in the possible technical solutions. I tried to describe (in the chapter "Connecting ML and rules") the approaches I know of, none of which are very exciting.
I'd love to hear if anybody knows of good approaches.
BTW, I think information travels over "normal" networking gear (e.g. fiber optics) at about 70% of the speed of light (which is why high-frequency trading tends to move to over-the-air microwave networking to shave a few nanoseconds - see [1]). But I guess the story still works, at the resolution it is told.
I think this presentation is mainly about implementation-related coverage, and there are of course many other kinds (not sure if this is what you were asking about). For instance, in HW design, there is a bigger emphasis on "functional coverage", i.e. coverage derived from a description of what the Device Under Test should do, what the inputs look like etc..
One point already made by several people on this thread is that code coverage, while helpful, is not enough (and perhaps is not even the best bang for the buck).
In hardware verification (where I come from, and where the cost of bugs is usually higher), "functional coverage" is considered more important. This is usually achieved via constraint-based randomization (somewhat similar in spirit to QuickCheck, already mentioned in this thread).
My intuition is that (1) unemployment will indeed continue to rise due to automation, (2) the world will not become a crime-ridden dystopian place, and (3) Guaranteed basic income will probably happen, in one form or another. I posted about this here, if you care to take a look: https://blog.foretellix.com/2016/05/10/the-next-20-years-of-...
First, as etendue says, it is not easy. The problem of mixing “Boolean” verification with probabilistic, less-deterministic verification is especially hard. I discussed this a bit in [1], if you care to take a look.
Also, I think most current AVs are not driven by DNNs at the top level (comma.ai [2] is one exception). See [3] for some discussion of that, and of verifying machine-learning-based systems.
Finally, one possible way to check that AV manufacturers “do the right thing” in correctly verifying the combination of DNNs, Misra C, digital HW, sensors and so on is perhaps to create a big, extensible catalog of AV-related scenarios, which ideally should be shared between the manufacturers and the certifying bodies – see [4]. I think there is some hint of that in the DOT pdf – still working my way through it.