Opportunity: Software systems are incorporating deep learning to solve diverse tasks including robotics control, medical diagnosis, code generation, protein synthesis, and question answering.

Challenge: How can we design such systems in a way that provides guarantees on their correctness?