Programming by examples: PL meets ML
Sumit Gulwani (Microsoft, USA)
Programming by Examples (PBE) involves synthesizing intended programs in an underlying domain-specific language from example-based specifications. PBE systems are already revolutionizing the application domain of data wrangling and are set to significantly impact several other domains including code refactoring. There are three key components in a PBE system. (i) A search algorithm that can efficiently search for programs that are consistent with the examples provided by the user. We leverage a divide-and-conquer-based deductive search paradigm to inductively reduce the problem of synthesizing a program expression of a certain kind that satisfies a given specification into sub-problems that refer to sub-expressions or sub-specifications. (ii) Program ranking techniques to pick an intended program from among the many that satisfy the examples provided by the user. We leverage features of the program structure as well of the outputs generated by the program on test inputs. (iii) User interaction models to facilitate usability and debuggability. We leverage active-learning techniques based on clustering inputs and synthesizing multiple programs. Each of these three PBE components leverage both formal methods and heuristics. We make the case for synthesizing these heuristics from training data using appropriate machine learning methods. This not only leads to better heuristics, but also enables easier development, maintenance, and even personalization of a PBE system.
Sumit Gulwani is a Research manager at Microsoft, leading the PROSE research and engineering team that develops APIs for program synthesis and incorporates them into real products. He is the inventor of the Flash Fill feature in Microsoft Excel used by hundreds of millions of people. He has published 110+ papers in top-tier conferences/journals across multiple computer science areas, and delivered 40+ keynotes/invited talks at various forums. He was awarded the ACM SIGPLAN Robin Milner Young Researcher Award in 2014 for his pioneering contributions to end-user programming and intelligent tutoring systems. He obtained his PhD in Computer Science from UC-Berkeley in 2005, and was awarded the ACM SIGPLAN Outstanding Doctoral Dissertation Award. He obtained his BTech in Computer Science and Engineering from IIT Kanpur in 2000, and was awarded the President’s Gold Medal.
Influence-directed explanations for machine learning systems
Anupam Datta (Carnegie Mellon University, USA)
Machine learning systems are often inscrutable black boxes: they are effective predictors but lack human-understandable explanations. I will describe a new paradigm for influence-directed explanations that address this problem. Influence-directed explanations shed light on the inner workings of black-box machine learning systems by identifying components that causally influence system behavior and by providing human-understandable interpretation to the concepts represented by these components. I will describe instances of this paradigm that are model-agnostic and instances that are specific to deep neural networks. Influence-directed explanations serve as a foundation for reasoning about fairness and privacy of machine learning models. Our initial exploration suggests that formal methods for analysis of probabilistic systems have an important role to play in efficient generation of influence-directed explanations. Joint work with colleagues at Carnegie Mellon University.
Anupam Datta is Professor of Electrical and Computer Engineering and (by courtesy) Computer Science at Carnegie Mellon University. He is Director of the Accountable Systems Lab. His research focuses on enabling real-world complex systems to be accountable for their behavior, especially as they pertain to privacy, fairness, and security. His work has helped create foundations and tools for accountable big data systems and cryptographic protocols. Specific examples include a privacy compliance tool chain deployed at Microsoft. the AdFisher tool that discovered gender bias in the targeting of job-related ads in online behavioral advertising, and Protocol Composition Logic, which was applied to prove security properties of a number of real-world security protocols. Datta obtained Ph.D. (2005) and M.S. (2002) degrees from Stanford University and a B.Tech. (2000) from IIT Kharagpur, all in Computer Science.
Provably beneficial artificial intelligence
Stuart Russell, Turing Speaker (University of California at Berkeley, USA)
I will briefly survey recent and expected developments in AI and their implications. Beyond these, one must expect that AI capabilities will eventually exceed those of humans across a range of real-world-decision making scenarios. Should this be a cause for concern, as Elon Musk, Stephen Hawking, and others have suggested? And, if so, what can we do about it? While some in the mainstream AI community dismiss the issue, I will argue instead that a fundamental reorientation of the field is required. Instead of building systems that optimize arbitrary objectives, we need to learn how to build systems that will, in fact, be beneficial for us. I will show that it is useful to imbue systems with explicit uncertainty concerning the true objectives of the humans they are designed to help, as well as the ability to learn more about those objectives from observation of human behaviour.
Stuart Russell is a Professor of Computer Science at the University of California at Berkeley, holder of the Smith-Zadeh Chair in Engineering, and Director of the Center for Human-Compatible AI. He is a recipient of the IJCAI Computers and Thought Award and from 2012 to 2014 held the Chaire Blaise Pascal in Paris. He is a Fellow of the American Association for Artificial Intelligence, the Association for Computing Machinery, and the American Association for the Advancement of Science. His book “Artificial Intelligence: A Modern Approach” (with Peter Norvig) is the standard text in AI, used in over 1300 universities in 118 countries. His research covers a wide range of topics in artificial intelligence, with an emphasis on the long-term future of artificial intelligence and its relation to humanity. He has developed a new global seismic monitoring system for the nuclear-test-ban treaty and is currently working to ban lethal autonomous weapons.
Towards robust and explainable artificial intelligence
Pushmeet Kohli (DeepMind, UK)
Deep learning has led to rapid progress being made in the field of machine learning and artificial intelligence, leading to dramatically improved solutions of many challenging problems such as image understanding, speech recognition, and automatic game playing. Despite these remarkable successes, researchers have observed some intriguing and troubling aspects of the behaviour of these models. A case in point is the presence of adversarial examples which make learning based systems fail in unexpected ways. Such behaviour and the difficultly of interpreting the behaviour of neural networks is a serious hindrance in the deployment of these models for safety-critical applications. In this talk, I will review the challenges in developing models that are robust and explainable and discuss the opportunities for collaboration between the formal methods and machine learning communities.
Pushmeet is a principal scientist and team leader at DeepMind. His research revolves around Intelligent Systems and Computational Sciences. His current research interests include Safe and Verified AI, Probabilistic Programming, Interpretable and Verifiable Knowledge Representations of Deep Models. In terms of application domains, he is interested in goal-directed conversation agents, machine learning systems for healthcare, and 3D reconstruction and tracking for augmented and virtual reality. Pushmeet’s papers has appeared in conferences in the field of machine learning, computer vision, game theory and human computer interaction and have won awards in CVPR, WWW, CHI, ECCV, ISMAR, TVX and ICVGIP. His research has also been the subject of a number of articles in popular media outlets such as Forbes, Wired, BBC, New Scientist and MIT Technology Review. Pushmeet is on the editorial board or PAMI, IJCV and CVIU.
The realities of applied AI
Alison Lowndes (NVIDIA, USA)
Artificial Intelligence will improve productivity across a broad range of applications and across a broad range of industries. The benefit to humanity will be substantial but there are important lessons to learn and steps to take. NVIDIA works closely with world-wide researchers, Enterprise & startups in both getting started & problem-solving. This talk will address some of the issues to be considered and explain why software and community are key to success with AI.
After spending her first year with NVIDIA as a Deep Learning Solutions Architect, Alison is now responsible for NVIDIA’s Artificial Intelligence Developer Relations in the EMEA region. She is a mature graduate in Artificial Intelligence combining technical and theoretical computer science with a physics background & over 20 years of experience in international project management, entrepreneurial activities and the internet. She consults on a wide range of AI applications, including planetary defence with NASA & ESA, and continues to manage the community of AI & ML researchers around the world, staying knowledgeable in state of the art across all areas of research. She also travels and advises, teaches and evangelizes NVIDIA’s platform, around the globe.
Explaining the effectiveness of random testing
Rupak Majumdar (Max Planck Institute for Software Systems, Germany)
Random testing is a popular technique to test large and complex systems. It is surprisingly effective in many different scenarios but for the most part, its success is often contrary to academic wisdom: programs have large state spaces and one should not expect to find subtle bugs by randomly running up against them. In this talk, I will describe a few situations where we can provide a theoretical understanding of the effectiveness of random testing using methods from combinatorics. For example, we show that bugs in distributed systems are empirically correlated with certain coverage notions and a small set of randomly chosen tests can be shown to cover all coverage goals under this notion. While the application domains do not concern machine learning, I would like to “reason by analogy” about debugging and explaining behaviors of machine learning components in a software system.
Rupak Majumdar is a Scientific Director at the Max Planck Institute for Software Systems. His research interests are in the theory and applications of formal methods in software, hardware, and cyber-physical systems. He received the President’s Gold Medal from IIT, Kanpur, the Leon O. Chua award from UC Berkeley, an NSF CAREER award, a Sloan Foundation Fellowship, an ERC Synergy award, “Most Influential Paper” awards from PLDI and POPL, and several best paper awards (including from SIGBED, EAPLS, and SIGDA).
Machine learning and logic: fast and slow thinking
Moshe Vardi (Rice University, USA)
There is a recent perception that computer science is undergoing a Kuhnian paradigm shift, with CS as a model-driven science being replaced as a data-driven science. I will argue that, in general new scientific theories refine old scientific theories, rather than replace them. Thus, data-driven CS and model-driven CS complement each other, just as fast thinking and slow thinking complement each other in human thinking, as explicated by Daniel Kahneman. I will then use automated vehicles as an example, where in recent years, car makers and tech companies have been racing to be the first to market. In this rush there has been little discussion of how to obtain scalable standardization of safety assurance, without which this technology will never be commercially deployable. Such assurance requires formal methods, and combining machine learning with logic is the challenge of the day.
Moshe Y. Vardi is the George Distinguished Service Professor in Computational Engineering and Director of the Ken Kennedy Institute for Information Technology at Rice University. He is the recipient of three IBM Outstanding Innovation Awards, the ACM SIGACT Goedel Prize, the ACM Kanellakis Award, the ACM SIGMOD Codd Award, the Blaise Pascal Medal, the IEEE Computer Society Goode Award, the EATCS Distinguished Achievements Award, and the Southeastern Universities Research Association’s Distinguished Scientist Award. He is the author and co-author of over 500 papers, as well as two books: Reasoning about Knowledge and Finite Model Theory and Its Applications. He is a Fellow of the Association for Computing Machinery, the American Association for Artificial Intelligence, the American Association for the Advancement of Science, the European Association for Theoretical Computer Science, the Institute for Electrical and Electronic Engineers, and the Society for Industrial and Applied Mathematics. He is a member of the US National Academy of Engineering and National Academy of Science, the American Academy of Arts and Science, the European Academy of Science, and Academia Europaea. He holds honorary doctorates from the Saarland University in Germany, Orleans University in France, UFRGS in Brazil, and the University of Liege in Belgium. He is currently a Senior Editor of the Communications of the ACM, after having served for a decade as Editor-in-Chief.
AI2: AI safety and robustness with abstract interpretation
Martin Vechev (ETH Zurich, Switzerland, and DeepCode.ai)
I will present AI2 (ai2.ethz.ch), a new approach for ensuring safety and robustness of AI systems based on abstract interpretation. AI2 is based on symbolic over-approximation and can automatically reason about safety properties (e.g., robustness) of realistic deep neural networks (e.g., convolutional). In the talk I will discuss how to soundly and precisely approximate the behavior of fully-connected layers with rectified linear unit activations (ReLU), convolutional layers with ReLU, and max pooling layers, allowing AI2 to scale to larger networks. I will also present a new abstraction which allows a trade-off between scalability and precision. Finally, I will discuss several open research challenges in applying symbolic methods to AI systems.
Martin Vechev is an Associate Professor at ETH Zurich, where he leads the SRL Lab. Prior to ETH, he was a researcher at the IBM T.J. Watson Research Center, USA. He obtained his PhD from Cambridge University, UK. His current research work spans a range of AI topics including: systems that combine programming languages and machine learning to solve tasks not previously possible, foundations and applications of probabilistic programming, and making AI systems more secure, reliable and interpretable. He is the recipient of various awards including an ERC Starting Grant, SIGPLAN and CACM Research Highlights, several faculty awards (Facebook, Google), an Atanasoff prize for outstanding young researchers awarded by the President of Bulgaria, and others. He is also a co-founder of Deepcode.ai, a start-up building the next-generation of AI-based programming tools.
Ethically aligned AI systems
Francesca Rossi, Turing Speaker (IBM and University of Padova, Italy)
AI systems are increasingly acting in the same environment as humans, in areas as diverse as driving, assistive technology, and health care. Humans and machines will often need to work together and agree on common decisions. This requires alignment around some common moral values and ethical principles. Humans will accept and trust more machines that behave at least as ethically as other humans in the same environment. Also, this would make it easier for machines to explain their behavior in terms understandable by humans. Moreover, shared moral values and ethical principles will help in collective human-machine decision making, where consensus or compromise is needed. In this talk I will present some challenges in designing ethically aligned AI systems that humans can trust, and describe technical solutions for such challenges.
Francesca Rossi is the AI Ethics Global Leader and a Distinguished Research Staff Member at IBM Research AI. She is also a professor of computer science at the University of Padova, Italy, currently on leave. Her research interests focus on artificial intelligence, specifically they include constraint reasoning, preferences, multi-agent systems, computational social choice, and collective decision making. She is also interested in ethical issues in the development and behaviour of AI systems, in particular for decision support systems for group decision making. She has published over 190 scientific articles in journals and conference proceedings, and as book chapters. She has co-authored a book and she has edited 17 volumes, between conference proceedings, collections of contributions, special issues of journals, as well as the Handbook of Constraint Programming. She is a AAAI and a EurAI fellow, and a Radcliffe fellow 2015. She has been president of IJCAI and an executive councillor of AAAI. She is Editor in Chief of the Journal of AI Research (JAIR) and a member of the editorial board of Constraints, Artificial Intelligence, AMAI, and KAIS. She co-chairs the AAAI committee on AI and ethics and she is a member of the scientific advisory board of the Future of Life Institute and of the Leverhulme Centre for the Future of Intelligence. She is in the executive committee of the IEEE global initiative on ethical considerations on the development of autonomous and intelligent systems and she belongs to the World Economic Forum Global Council on AI and robotics. She is a member of the board of directors of the Partnership on AI, where she represents IBM as one of the founding partners.
Deep learning methods for large scale theorem proving
Christian Szegedy (Google, USA)
Machine Learning (with hand engineered features) has become an enabling factor for reasoning in large theories. Here I will give overview of some recent work utilizing deep neural networks for both premise selection and guiding automated theorem provers. Also we will highlight connections and recent efforts on utilizing natural language corpora for automated reasoning.
Christian Szegedy is an artificial intelligence researcher at Google, his interests include deep learning based computer vision (the designer of the Inception computer vision architecture and is co-inventor of the MultiBox object detector and DeepPose human pose estimator). He is also know for his work on adversarial examples and batch-normalization. His most current research direction is focused on auto-formalizing mathematics by utilizing the latest AI methods at large scale.
Program fairness – a formal methods perspective
Aditya Nori (Microsoft Research Cambridge, UK)
With the range and sensitivity of algorithmic decisions expanding at a break-neck speed, it is imperative that we seriously investigate fairness and bias in decision-making programs. First, we show that a number of recently proposed formal definitions of fairness can be encoded as probabilistic program properties. Second, with the goal of enabling rigorous reasoning about fairness, we design a novel technique for verifying probabilistic properties that admits a wide class of decision-making programs. Third, we present the first verification tool for automatically certifying that a program meets a given fairness property. We evaluate our tool on a range of decision-making programs. Our evaluation demonstrates the tool’s ability to verify fairness for a range of different programs, which we show are out-of-reach for state-of-the-art program analysis techniques.
Aditya Nori is a principal researcher and member of the InnerEye team at MSR Cambridge. His research interests are in the design and analysis of reliable intelligent systems. Over the past few years, he has explored various synergies between programming languages, formal methods and machine learning. These include the use of machine learning in program verification and specification inference, and probabilistic programming. He has built a number of programmer productivity tools, and this includes the Yogi software model checker that shipped with the Static Driver Verifier toolkit for Microsoft Windows, and the R2 probabilistic programming system. He is also winner of the ACM SIGSOFT Distinguished Paper awards at FSE 2006 and 2015. He is currently working on precise and robust medical image analysis for cancer treatment.
Safe reinforcement learning via formal methods
André Platzer (Carnegie Mellon University, USA)
Formal verification provides a high degree of confidence in safe system operation, but only if reality matches the verified model. Although a good model will be accurate most of the time, even the best models are incomplete. This is especially true in Cyber-Physical Systems because high-fidelity physical models of systems are expensive to develop and often intractable to verify. Conversely, reinforcement learning-based controllers are lauded for their flexibility in unmodelled environments, but do not provide guarantees of safe operation.
This talk presents joint work with Nathan Fulton on provably safe learning that provides the best of both worlds: the exploration and optimization capabilities of learning along with the safety guarantees of formal verification. The main insight is that formal verification combined with verified runtime monitoring can ensure the safety of a learning agent. Verification results are preserved whenever learning agents limit exploration within the confounds of verified control choices as long as observed reality comports with the model used for off-line verification. When a model violation is detected, the agent abandons efficiency and instead attempts to learn a control strategy that guides the agent to a modelled portion of the state space.
André Platzer’s research develops the logical foundations of cyber-physical systems to characterize their fundamental principles and to show how we can design computers that are guaranteed to interact correctly with the physical world. The solution to this challenge is the key to enabling computer assistance that we can bet our lives on. He pursues this challenge with the principled design of programming languages with logics that can provide proofs as correctness guarantees.