4 ms·

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, w

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.

detaro 11y ago
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.
shorodei 11y ago
There are certain subsystems of self driving (visual recognition) that are inherently learning/pattern based.
seanmcdirmid 11y ago
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.
- cscurmudgeon 11y ago
  This just FUD. Formal proofs are quite prevalent. Look at ACL2 for a start.
  - seanmcdirmid 11y ago
    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-position-paper.pdf 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).pdf 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.
    - cscurmudgeon 11y ago
      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_32 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 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 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-verification 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.
      - seanmcdirmid 11y ago
        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.
        cscurmudgeon 11y ago
        > 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)
        seanmcdirmid 11y ago
sklogic 11y ago
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.

detaro 11y ago

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.

shorodei 11y ago

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

seanmcdirmid 11y ago

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.

cscurmudgeon 11y ago
This just FUD. Formal proofs are quite prevalent. Look at ACL2 for a start.
- seanmcdirmid 11y ago
  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-position-paper.pdf 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).pdf 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.
  - cscurmudgeon 11y ago
    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_32 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 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 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-verification 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.
    - seanmcdirmid 11y ago
      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.
      - cscurmudgeon 11y ago
        > 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)
        seanmcdirmid 11y ago

sklogic 11y ago

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.