Machine Learning as Program Synthesis, Swarat Chaudhuri, Rice University
Time: Monday, July 15, 09:00-10:00
Abstract: Most recent efforts on formal methods for machine learning have focused on the verification of deep neural networks. While exciting, this line of work faces two key challenges. First, the size of modern neural models makes end-to-end symbolic reasoning difficult to scale. Second, why should we even expect a model to satisfy a correctness property that wasn’t part of its training objective?
These are good reasons to investigate approaches in which formal methods are tightly coupled with training, rather than applied post hoc. In this talk, I will present such an approach, centered around a view of machine learning as program synthesis. Here, a statistical model is represented as a program in a structured, high-level language (that allows the restricted use of neural modules). Correct-by-construction learning is posed as a quantitative synthesis problem: find a program that optimally fits a dataset and also satisfies a set of correctness requirement.
Using recent work in the setting of deep reinforcement learning and transfer learning, I will show that this problem can be effectively solved using a tight coupling of methods from deep learning and symbolic program synthesis. The programmatic models discovered in this way are easier to interpret and verify than neural networks, and are more likely to satisfy correctness properties such as robustness. Most intriguingly, program synthesis has benefits beyond verification and interpretability, and can be used to “regularize” deep learning, transfer knowledge from one learning setting to another, and in general, enable learning tasks that cannot be solved using deep learning alone. Collectively, these results open up a new way in which ideas from formal methods can help realize the dream of high-performance, high-assurance machine learning.
Bio: Swarat Chaudhuri is an Associate Professor of Computer Science at Rice University. His research lies in the intersection of formal methods and machine learning. Swarat received a bachelor’s degree in computer science from the Indian Institute of Technology, Kharagpur, in 2001, and a doctoral degree in computer science from the University of Pennsylvania in 2007. From 2008-2011, he was an Assistant Professor at the Pennsylvania State University. He is a recipient of the National Science Foundation CAREER award, the ACM SIGPLAN John Reynolds Doctoral Dissertation Award, the Morris and Dorothy Rubinoff Dissertation Award, and a Google Research Award. He has served on program committees of many conferences in formal methods, programming languages, and artificial intelligence, and co-chaired CAV 2016.
Open Challenges in AI and Formal Verification, Dawn Song, UC Berkeley
Time: Tuesday, July 16, 09:00-10:00
Abstract: In this talk, I will talk about recent work and open challenges at the intersection of AI and Formal Verification. First, I’ll talk about adversarial deep learning and certified robustness and open challenges in this area. Second, I’ll talk about how deep learning can help automate theorem proving tasks and the remaining open challenges in this domain.
Bio: Dawn Song is a Professor in the Department of Electrical Engineering and Computer Science at UC Berkeley. Her research interest lies in deep learning, security, and blockchain. She has studied diverse security and privacy issues in computer systems and networks, including areas ranging from software security, networking security, distributed systems security, applied cryptography, blockchain and smart contracts, to the intersection of machine learning and security. She is the recipient of various awards including the MacArthur Fellowship, the Guggenheim Fellowship, the NSF CAREER Award, the Alfred P. Sloan Research Fellowship, the MIT Technology Review TR-35 Award, the Faculty Research Award from IBM, Google and other major tech companies, and Best Paper Awards from top conferences in Computer Security and Deep Learning. She is ranked the most cited scholar in computer security (AMiner Award). She obtained her Ph.D. degree from UC Berkeley. Prior to joining UC Berkeley as a faculty, she was a faculty at Carnegie Mellon University from 2002 to 2007. She is also a serial entrepreneur, including Ensighta Security (acquired by FireEye Inc.) and Menlo Security. She is currently the founder and CEO of Oasis Labs, creating privacy-first cloud computing on blockchain.
Specifying and Testing QUIC with Ivy, Ken McMillan, Microsoft Research
Time: Wednesday, July 17, 09:00-10:00
Abstract: QUIC is a new Internet secure transport protocol currently in the process of IETF standardization. It is intended as a replacement for the TLS/TCP stack and will be the basis of HTTP/3, the next official version of the hypertext transfer protocol. As a result, it is likely, in the near future, to carry a substantial fraction of traffic on the Internet. I will describe the application of a light-weight formal methodology to QUIC, using compositional specification-based testing. A formal specification of the wire protocol was developed in the Ivy language and used to generate automated randomized black-box testers for implementations of QUIC. The testers effectively take one role of the QUIC protocol, interacting with the other role to generate full protocol executions, and verifying that the implementations conform to the formal specification. This form of testing generates significantly more diverse stimuli and stronger correctness criteria than interoperability testing, the primary method used to date to validate QUIC and its implementations. As a result, numerous implementation errors have been found. These include some vulnerabilities at the protocol and implementation levels, such as an off-path denial of service scenario and an information leak similar to the “heartbleed” vulnerability in OpenSSL.
Distilling a formal wire specification of a protocol from standards documents is difficult, both because the documents are ambiguous and because standards tend to provide an internal description of system components rather than an external behavioral view. Because the compositional testing approach uses the same specification for both generation of stimulus and validation of responses, the approach provides feedback about cases in which the specification is either too strong or too weak. This makes it possible to use knowledge implicit in the various implementations to converge to a common behavioral specification. I will discuss both how the specification process helps to flush out bugs in the implementation, and conversely how the testing process helps to refine the specification.
This is joint work with Lenore Zuck of the University of Illinois at Chicago.
Bio: Ken McMillan is a principal researcher at Microsoft Research in Redmond, Washington. He works in formal verification and light-weight formal methods, particularly in applications to hardware and distributed protocols. His main interest is in tools, languages and methodologies that can be applied practically in an engineering environment. His current work centers on a tool called Ivy, whose design goal is to make maximally effective use of proof automation in the verification of distributed systems. His past work includes the development of Symbolic Model Checking and Craig interpolation methods in model checking. He holds a BS in electrical engineering from the University of Illinois at Urbana (1984), an MS in electrical engineering from Stanford (1986) and a Ph.D. in computer science from Carnegie Mellon (1992). He is the author of the book “Symbolic Model Checking”, and the SMV symbolic model checking system. For his work in model checking, he has received the ACM doctoral dissertation award, the SRC technical excellence award, the ACM Paris Kannelakis award, the Alan Newell award from Carnegie Mellon and the CAV award. He was formerly a member of the technical staff at AT&T Bell Laboratories and a fellow at Cadence Research Labs.