yoav_hollander

Exactly. I was assuming that the by now the default answer to "LLMs sort-of do this, but not very well" should be "OK, wait a few months".

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.

Here is a (longish) post I wrote about this issue (mainly from the perspective of verifying autonomous vehicles):

https://blog.foretellix.com/2017/07/06/where-machine-learnin...

This is a really good list. Thanks.

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].

[1] http://blog.foretellix.com/2017/07/06/where-machine-learning...

[2] https://news.ycombinator.com/item?id=14717692

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.

I agree to that. But:

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 do think that random forests (and Inductive Logic Programming) seem easier to connect to rule-based "human-written" logic.

It does seem though that Neural Networks are the main ML story, at least for now, by a wide margin.

Thanks a lot - will look it up.

OP here:

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.

Fun story - never heard it before.

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.

[1] https://en.wikipedia.org/wiki/High-frequency_trading

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..

Please see my post about the various kinds of coverage here: https://blog.foretellix.com/2016/12/23/verification-coverage...

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).

I tried to cover (ahem) this whole how-to-use-and-improve-coverage topic in the following post: https://blog.foretellix.com/2016/12/23/verification-coverage...

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-...

Thanks. I did a second pass through the policy paper, and put a summary of the verification implications here: https://blog.foretellix.com/2016/09/21/verification-implicat...

Finally posted my initial comments on the verification implications of all this here: https://blog.foretellix.com/2016/09/21/verification-implicat...

Just ended. And here is Obama's call for safe automated vehicles: https://www.post-gazette.com/opinion/Op-Ed/2016/09/19/Barack...

Live streaming just started here: https://www.transportation.gov/AV

A few comments on this:

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.

[1] https://blog.foretellix.com/2016/07/22/checking-probabilisti...

[2] http://www.bloomberg.com/features/2015-george-hotz-self-driv...

[3] https://blog.foretellix.com/2016/09/14/using-machine-learnin...

[4] https://blog.foretellix.com/2016/07/05/the-tesla-crash-tsuna...

Right. This paper ([0]) is actually mentioned in the DARPA BAA ([1]) as an example of a possible direction. A somewhat-similar scheme is [2]. Both seem to do some kind of sensitivity analysis, so as to show the user which parts of the input were most important for coming up with the decision: For instance, [2] "explains" an ML system (which answers questions about pictures), by telling you which pixels were most important for the decision. It does that by essentially hiding pixels and seeing how that influences the ML system's decisions.

So this produces not so much an explanation as "hints" as to why the system made the decision (still pretty useful). The BAA also mentions another possible direction ([3]), which is actually capable of making full-sentence explanations. For instance, it can explain the decisions of an image-to-wild-bird-name classifier with sentences like "This is a Laysan Albatross because this bird has a large wingspan, hooked yellow beak, and white belly”.

This sounds pretty impressive, but seems to depend on vocabulary provided by a user. As a result, in some cases the explanation provided may have nothing to do with how the classifier actually classified - see [4] for my interpretation of these issues and how they might perhaps be solved.

[0] https://arxiv.org/pdf/1602.04938v3.pdf

[1] https://www.fbo.gov/utils/view?id=ae0b129bca1080cc7c517e8dad...

[2] https://computing.ece.vt.edu/~ygoyal/papers/vqa-interpretabi...

[3] http://arxiv.org/pdf/1603.08507.pdf

[4] https://blog.foretellix.com/2016/08/31/machine-learning-veri...

If there is real progress towards Explainable AI, this would also be very useful for _verifying_ machine-learning-based systems (i.e. finding the bugs in them).

I wrote about this in [1], but I am not a machine-learning expert (I am coming from the verification side), so would love to hear comments from other people.

[1] https://blog.foretellix.com/2016/08/31/machine-learning-veri...

Well yes, you _can_ verify ML-based systems (and I discuss briefly how in the linked article). It is just that this is much harder with such systems than with HW or SW systems for which "you have the source code".

What I meant by "Because ML systems are opaque, you cannot really reason about what they do" (perhaps I was not being clear) was this: You can indeed _observe_ what they do, but being able to actually inspect the source makes verification much easier and more reliable: You know what parts of the logic you have covered, you can think of "danger areas" (and direct testing to them), and you can simply check whether all the cases you can think about have been covered in the source.

With opaque systems, you have no idea whether e.g. your ML-based autonomous vehicle will recognize people-painted-on-a-bus as people-on-the-road, until you actually test for that. And then you have to test people-painted-on-a-truck.

What I meant regarding "modular verification" is that you can check sub-modules according to some spec (or at least according to informal comments). This is quite different from what you can do when analyzing NN layers.

I suspect you are right in claiming (in your last paragraph) that one will always have to choose between "more understandable" and "more accurate". But I think we can do various things (the DARPA suggestion being one of them) to make the "more accurate" solution more verifiable.

I think this issue of "Explainable Machine Learning" and interpretability is just going to get more and more important as ML grows. It will also be important for verifying ML-based systems - another problem area.

See [1] for a discussion of both.

[1] https://blog.foretellix.com/2016/08/31/machine-learning-veri...

I like the idea of using fuzzing "to show a direct correlation between programs that score low in their algorithmic code analysis and ones shown by fuzzing to have actual flaws".

I hope they'll use AFL, and publish the parameters / settings, so others will be able to repeat the experiments.

See also [2] for a description of the verification challenges of a fictitious (but informative) Amazon last-mile autonomous delivery vehicle.

[2] https://www.cs.york.ac.uk/ftpdir/reports/2015/YCS/496/YCS-20...

"Last mile" delivery may perhaps be done with much smaller, mostly-autonomous vehicles (with remote operators getting involved only when needed).

See related article and thread in [1] - article also discusses some startup ideas for mostly-autonomous systems.

[1] https://news.ycombinator.com/item?id=11565601

I think you are absolutely correct. It is the price/performance of creating these "interactive specs" that will determine whether this idea is any good.

From what I have seen (I looked a bit at the what people are doing in UAVs, autonomous vehicles and so on - see e.g. http://blog.foretellix.com/2015/07/03/my-impressions-from-th...), I think a lot can be done to improve both price and performance.

In other words, I think it is possible to invent new tools / methodologies to make simulation (especially high-level simulation) easier, and especially to get a lot more out of it, at all stages of design / verification / maintenance.

Right. Cutting-edge military systems are, indeed, risky business, and one has to balance (as you say) more testing against not having those systems when you need them.

This puts a high premium on the efficiency of bug-finding, especially spec bugs of new systems. My intuition is that this could improve by a lot.

Absolutely. What I meant was that there should have been some "are you sure" confirmation in this case.