Hacker News Reader

Comment by raverbashing | Hacker News Reader

Especially in the (possibly very lucrative market) of Deep Learning powered devices, like self-driving cars

nVidia has already demoed hardware on that area

Is deep learning suitable for self-driving cars? I would expect that cars, like other safety critical systems, need to be formally proven to work as intended, which AFAIK can't really be done with neural networks.

I don't think it would be possible to formally prove that e.g. any image recognition system will work correctly given all realistic real world inputs, so that requirement doesn't work out anyways. It's more likely that they are required to perform extensive real world tests + maybe beforehand tests against video material.

There are certain subsystems of self driving (visual recognition) that are inherently learning/pattern based.

Where did you get this idea from?

Formal proofs even in avionics are very limited, and planes aren't exactly dropping out of the sky. Safety critical systems need a degree of auditing and testing, to be sure, but formal proofs have never been a requirement since they aren't that practical.

This just FUD. Formal proofs are quite prevalent. Look at ACL2 for a start.

Not FUD at all. Pointing at a system doesn't provide any evidence that proofs are prevalent in industry. Check out:

https://chess.eecs.berkeley.edu/hcssas/papers/Cleaveland-pos...

> Although formal proofs of correctness are (rightly) touted as providing superior guarantees to those of testing, DO-178B makes no mention of formal methods, except in an Annex given over to techniques deemed not yet mature enough for certification purposes.

Or http://ti.arc.nasa.gov/m/pub-archive/1023h/1023%20(Denney).p...:

> In principle, formal methods offer many advantages for aerospace software development: they can help to achieve ultra-high reliability, and they can be used to provide evidence of the reliability claims which can then be subjected to external scrutiny. However, despite years of research and many advances in the underlying formalisms of specification, semantics, and logic, formal methods are not much used in practice. In our opinion this is related to three major shortcomings. First, the application of formal methods is still expensive because they are labor- and knowledge-intensive. Second, they are difficult to scale up to complex systems because they are based on deep mathematical insights about the behavior of the systems (i.e., they rely on the “heroic proof”). Third, the proofs can be difficult to interpret, and typically stand in isolation from the original code.

The situation will just get worse as we increasingly move away from hand written logic to machine learned logic. Now, there is probably a place for formal methods in this newer order, but it will take awhile for researchers to find it, and it is definitely not going to be at the level of verifying hand-encoded logic that doesn't exist.

I meant to point out formal verification is used in the industry quite a bit (not in aviation alone).

1. Replacing testing with formal verification at Intel (2009)

http://link.springer.com/chapter/10.1007/978-3-642-02658-4_3...

2. Fifteen years of formal property verification at Intel (2008)

http://link.springer.com/chapter/10.1007/978-3-540-69850-0_8

3. seL4: formal verification of an OS kernel

http://dl.acm.org/citation.cfm?id=1629596

There is such a big need that DARPA has even come up with a contest.

http://www.darpa.mil/program/crowd-sourced-formal-verificati...

I could go on, but I would rather not spend my time combating FUD and the general incivility here.

Formal verification is used a lot, but it is not a rule and definitely not a requirement by the FAA for aircraft certification. The idea that formal verification would be obviously necessary for the logic of a self-driving car is what was being challenged here. You could call that FUD, but you obviously have an agenda to push, I guess.

> not a requirement by the FAA for aircraft certification.

I never said that. Where did you get that?

> Safety critical systems need a degree of auditing and testing, to be sure, but formal proofs have never been a requirement since they aren't that practical. (emphasis mine)

I was challenging this idea.

Are systems for self-driving cars the only safety critical systems? What about Intel manufactured chips used in those same cars and flights and a gazillion other devices?

You have an agenda to push and got called out on facts :)

Have a good day. (Someone just went around down voting my other posts. Not you)

I guess it depends on how you interpret "that", which I meant to refer to "requirement" (they are not practical enough to be a requirement). But I guess I should have been more clear in my sentence structure.

Still not clear but we will leave it here :)

Btw, I use both deep learning and knowledge based systems in my work (but not formal verification) but don't like advertising that goes in AI by academics from all camps(don't want another AI winter).

Fair enough. I have no skin in this game since I'm a PL researcher...

Intel uses verification after they fumbled the Pentium FPU, verifying silicon is a good idea (also it's complex but doable)

Now good luck verifying a machine learning system beyond the basics.

Umm that is the point being made ...

I don't necessarily disagree with your points here, but for completeness you should note that DO-178B has been moving to DO-178C for a few years now, which includes references to formal methods for systems verification, specifically DO-333. Also, that paper by Denney is 10 years old, and some strides have been made since then to improve formal method tools for viable verification.

Even with a lack of formal proof, a reproducible, and therefore thoroughly testable black-box AI is still much safer than a diverse human drivers population which include drink-drivers, partially blind, psychopaths and so on.

Reply on news.ycombinator.com