Previous Talks
View a playlist of recordings of our previous talks.
Date: Monday, November 30th, 2020 @ 2PM.
Talk Title: Deep Learning in Adversarial Environments
Bio: Chaowei Xiao is a research scientist at NVIDIA Research. He earned his Ph.D. at the University of Michigan, working with Professor Mingyan Liu. His research interests lie at the intersection of computer security, privacy, and machine learning. His works have been featured in multiple media outlets, including Wired, Fortune, IEEE SPECTRUM. One of his research outputs is now on display at the Science Museum in London. He has received the best paper award at Mobicom 2014.
Talk Title: Deep Learning in Adversarial Environments
Bio: Chaowei Xiao is a research scientist at NVIDIA Research. He earned his Ph.D. at the University of Michigan, working with Professor Mingyan Liu. His research interests lie at the intersection of computer security, privacy, and machine learning. His works have been featured in multiple media outlets, including Wired, Fortune, IEEE SPECTRUM. One of his research outputs is now on display at the Science Museum in London. He has received the best paper award at Mobicom 2014.
Date: Monday, December 14th, 2020 @ 4PM.
Talk Title: A Tale of Two Applications of Verification in Machine Learning
Abstract: The rise of machine learning, particularly in the form of deep learning, has created a qualitative shift in our conception of what software is and what software can accomplish. But, of course, it’s not all rainbows and butterflies. Researchers have been hard at work trying to understand the fragility of the machine-learning pipeline: from training to inference, small changes to the input can result in radical changes to the output, which can lead to security, safety, as well as ethical problems. In this talk, I will show how new techniques from software verification can help us reason about, and ensure, robustness of machine-learning techniques against training-time (poisoning) and test-time (adversarial-example) attacks.
This talk is based on joint work with Yuhao Zhang, Samuel Drews, and Loris D’Antoni.
Bio: Aws Albarghouthi is an assistant professor at the University of Wisconsin-Madison. He studies automated synthesis and verification of programs. He received his PhD from the University of Toronto in 2015. He has received a number of best-paper awards for his work (at FSE, UIST, and FAST), an NSF CAREER award, a Google Faculty Research Award, and Facebook Research Awards. Aws is very excited about his virtual visit to Waterloo.
Date: Monday, December 21st, 2020 @ 4PM.
Talk Title: Understanding and Repairing Deep Neural Networks
Abstract: Deep neural networks (DNNs) have been successfully applied to a wide variety of problems, including image recognition, natural-language processing, medical diagnosis, and self-driving cars. As the accuracy of DNNs has increased so has their complexity and size, making the outputs of such models difficult to meaningfully interpret. The talk describes a new symbolic representation for DNNs that allowed us to exactly compute the integrated gradients, a state-of-the-art network attribution method that until now has only been approximated. Moreover, DNNs are far from infallible, and mistakes made by DNNs have led to loss of life, motivating research on verification and testing to find mistakes in DNNs. In contrast, the talk describes techniques and tools for repairing a trained DNN once a mistake has been discovered. We present Provable Repair of DNNs, which computes a minimal change to the parameters of a trained DNN to correct its behavior according to a given specification, and ensures that the patch is provably effective, generalizing, local, and efficient.
Aditya Thakur's Bio: Aditya Thakur is an assistant professor of Computer Science at the University of California, Davis. He received his Ph.D. from the University of Wisconsin, Madison, and has held positions at Google, Microsoft Research, and the University of California, Berkeley. His research interests include programming languages, machine learning, formal methods, and software engineering. He was the recipient of the Facebook Probability and Programming Research Award 2019 and 2020, and Facebook Testing and Verification Research Award 2018.
Matthew Ali Sotoudeh's Bio: Matthew Sotoudeh is a senior undergraduate student at the University of California, Davis, majoring in Computer Science and Mathematics, where he is a Regents Scholar.
Date: Monday, January 11th, 2021 @ 1PM.
Talk Title: What does it mean for ML to be trustworthy?
Abstract: The attack surface of machine learning is large: training data can be poisoned, predictions manipulated using adversarial examples, models exploited to reveal sensitive information contained in training data, etc. This is in large parts due to the absence of security and privacy considerations in the design of ML algorithms. Yet, adversaries have clear incentives to target these systems. Thus, there is a need to ensure that computer systems that rely on ML are trustworthy. Fortunately, we are at a turning point where ML is still being adopted, which creates a rare opportunity to address the shortcomings of the technology before it is widely deployed. Designing secure ML requires that we have a solid understanding as to what we expect legitimate model behavior to look like. We structure our discussion around two directions, which we believe are likely to lead to significant progress. The first encompasses a spectrum of approaches to verification and admission control, which is a prerequisite to enable fail-safe defaults in machine learning systems. The second pursues formal frameworks for security and privacy in machine learning, which we argue should strive to align machine learning goals such as generalization with security and privacy desiderata like robustness or privacy. We illustrate these directions with recent work on adversarial examples, privacy-preserving ML, machine unlearning, and deepfakes.
Bio: Nicolas Papernot is an Assistant Professor in the Department of Electrical and Computer Engineering and the Department of Computer Science at the University of Toronto. He is also a faculty member at the Vector Institute where he holds a Canada CIFAR AI Chair, and a faculty affiliate at the Schwartz Reisman Institute. His research interests span the security and privacy of machine learning. Nicolas is a Connaught Researcher and was previously a Google PhD Fellow. His work on differentially private machine learning received a best paper award at ICLR 2017. He serves on the program committees of several conferences including ACM CCS, IEEE S&P, and USENIX Security. He is also the co-author of CleverHans and TensorFlow Privacy, two open-source libraries widely adopted in the technical community to benchmark the security and privacy of machine learning. He earned his Ph.D. at the Pennsylvania State University, working with Prof. Patrick McDaniel. Upon graduating, he spent a year as a research scientist at Google Brain in Úlfar Erlingsson's group.
Date: Monday, January 18th, 2021 @ 4PM.
Talk Title: Robustness in unsupervised and supervised machine learning
Abstract: Recently, the need for robust machine learning algorithms has become apparent. Whether due to errors in data collection, model misspecification, or adversarial attacks, contaminated datasets arise in many areas. This is an issue, as existing methods appear to be quite brittle to small amounts of errors. Even more worryingly, these models are being deployed in many security-critical settings, such as self-driving cars, where reliability is an absolute must. In this talk, I will describe a line of work in which we provide provable guarantees for robust machine learning in several fundamental settings. I’ll begin by discussing the problem of robust estimation of mean and covariance of a Gaussian distribution, and how to relax this to distributions with weaker assumptions on the moments. I will then describe how these methods can be used to “robustify” supervised learning algorithms by applying robust mean estimation algorithms to the gradients of the dataset. While theoretically sound, the algorithms are also realizable and efficient, and I will present experimental results on both synthetic and real-world data. Based on joint works with Ilias Diakonikolas, Daniel M. Kane, Jerry Li, Ankur Moitra, Jacob Steinhardt, and Alistair Stewart.
Bio: Gautam Kamath is an Assistant Professor at the David R. Cheriton School of Computer Science at the University of Waterloo. He has a B.S. in Computer Science and Electrical and Computer Engineering from Cornell University, and an M.S. and Ph.D. in Computer Science from the Massachusetts Institute of Technology. His research interests lie in methods for statistics and machine learning, with a focus on challenges which arise in modern data analysis, including data privacy and robustness. He was a Microsoft Research Fellow, as a part of the Simons-Berkeley Research Fellowship Program at the Simons Institute for the Theory of Computing. He is recipient of an NSERC Discovery Accelerator Supplement, and was awarded the Best Student Presentation Award at the ACM Symposium on Theory of Computing in 2012.
Date: Monday, January 25th @4PM EST.
Talk Title: Fairness in ML
Date: Monday, February 1st @4PM EST.
Talk Title: Clustering - what both practitioners and theoreticians are doing wrong.
Date: Monday, February 8th @4PM EST.
Talk Title: A learning problem that is independent of the set theory ZFC axioms
Bio: Shai Ben-David earned his Ph.D. in mathematics from the Hebrew University in Jerusalem and has been a professor of computer science at the Technion (Israel Institute of Technology). He held visiting faculty positions at the Australian National University, Cornell University, ETH Zurich, TTI Chicago and the Simons Institute at Berkeley. Since 2004 Shai has been a professor at the David Cheriton School of Computer Science at the University of Waterloo. Since 2019 he is also a faculty member at the Toronto Vector institute. In recent years his research focus turned to machine learning theory. Among his notable contributions in that field are pioneering steps in the analysis of domain adaptation, learnability of real-valued functions, and change detection in streaming data. Shai has also made fundamental contributions to the theory of clustering and published seminal works on average-case complexity, competitive analysis of algorithms and alternatives to worst-case complexity.
Highlights:
- President of the Association for Computational Learning Theory (2009-2012).
- Program chair for the major machine learning theory conferences (COLT and ALT, and frequent area chair for ICML, NIPS and AISTATS).
- Co-authored the textbook “Understanding machine learning: from theory to algorithms” (Cambridge University Press 2015).
- Co-author of Best Paper awards, most recently in NIPS 2018.
- CIFAR AI Chair.
- University Research Chair at U Waterloo
Date: Monday, February 15th, 2021 @ 4PM EST.
Talk Title: Certified Artificial Intelligence
Abstract: Despite surpassing human-level performance in many challenging domains such as vision, planning, and natural sciences, there remain concerns about the fragility of modern data-driven AI systems when applied in the real-world, which poses a threat to their wider adoption. Indeed, obtaining AI systems theoretically guaranteed to be safe and reliable is a fundamental challenge of critical importance. In this talk, Gagandeep will present a path towards addressing this fundamental problem. Specifically, He will introduce new mathematical methods combining convex optimization with the classical abstract interpretation framework that enables scalable and precise logical reasoning about the (potentially infinite number of) behaviors of an AI system (e.g., a deep neural network). He will then show how these methods enable both the creation of state-of-the-art automated verifiers for modern AI systems and the design of new provable training techniques. Finally, He will outline several promising future research directions.
Bio: Gagandeep Singh will be starting as a tenure-track Assistant Professor in the Department of Computer Science at the University of Illinois Urbana-Champaign (UIUC) from Fall 2021. He is currently working with VMWare Research. His research interests lie at the intersection of artificial intelligence (AI) and programming languages. His long term goal is to design end-to-end automated formal reasoning tools for real-world systems with both software and AI components such as autonomous vehicles, robots, and AI-powered healthcare devices. Previously, he obtained a Ph.D. in Computer Science from ETH Zurich in 2020, where he designed new scalable and precise automated reasoning methods and tools for programs and deep neural networks.
Date: Monday, February 22nd, 2021 @ 4PM EST.
Talk Title: Towards ML for Quantification in SMT
Abstract: We aim to use ML to guide quantifier instantiation in SMT solving. What is the motivation for this? Quantifiers are indispensable in logic-based modeling, yet infamously hard to reason about. It can already be shown that exponential speedups are obtained by clever instantiation of quantifiers in finite domains. We will look at this in the context of Quantified Boolean Formulas (QBF). Further, we will look at the use of ML in the context of finite first-order models. The second part of the talk will outline how ML can help in general SMT quantifier instantiation and what ML methods are applicable in this domain.
Bio: Mikoláš Janota was born in Prague, when it was still Czechoslovakia, where he did his Masters at the Charles University and where he also developed a passion for solving and applying logic-based reasoning. He did his Ph.D. at University College Dublin, Ireland, where he worked on software verification and product configuration followed by postdoctoral positions in Portugal and Microsoft Research, Cambridge UK. He held the position of assistant lecturer at the University of Lisbon, Portugal until last year. Last September he moved back to the Czech Republic accepting the position of a senior researcher at Czech Technical University.
Talk Title: Towards ML for Quantification in SMT
Abstract: We aim to use ML to guide quantifier instantiation in SMT solving. What is the motivation for this? Quantifiers are indispensable in logic-based modeling, yet infamously hard to reason about. It can already be shown that exponential speedups are obtained by clever instantiation of quantifiers in finite domains. We will look at this in the context of Quantified Boolean Formulas (QBF). Further, we will look at the use of ML in the context of finite first-order models. The second part of the talk will outline how ML can help in general SMT quantifier instantiation and what ML methods are applicable in this domain.
Bio: Mikoláš Janota was born in Prague, when it was still Czechoslovakia, where he did his Masters at the Charles University and where he also developed a passion for solving and applying logic-based reasoning. He did his Ph.D. at University College Dublin, Ireland, where he worked on software verification and product configuration followed by postdoctoral positions in Portugal and Microsoft Research, Cambridge UK. He held the position of assistant lecturer at the University of Lisbon, Portugal until last year. Last September he moved back to the Czech Republic accepting the position of a senior researcher at Czech Technical University.
Date: Monday, March 8th, 2021 @ 4PM EST.
Talk Title: Formal Verification for Neural Networks and Cyber-Physical Systems with Reachability Methods
Abstract: Neural Networks have made great advances in vision and game-playing in the last decade. Beyond these core areas, however, almost every other field has at least attempted to use neural networks to some extent. Cyber-physical systems (CPS), where computers interact with the physical world, are no different. Although learning-based controllers have long been looked at in control theory, recent interest in combining CPS with neural networks has soared. One important distinction with CPS, however, is that these systems are not confined to the digital world. Behaviors of a neural network in a CPS may manifest in the physical world. CPS are often safety-critical and cannot tolerate any mistakes.
The field of formal verification has traditionally looked at proving properties about finite state machines or software programs. Recent research has also looked at other classes of systems such as CPS models given with differential equations, or even systems that include neural networks. This talk reviews some of our research in these areas, as well as results from the first international verification competition for neural networks (VNN-COMP) which took place last July. For a set of neural networks that performs automated aircraft collision avoidance, our nnenum tool was both the fastest and the only one to successfully prove all of the formal properties in the competition.
Bio: Stanley Bak is a computer scientist investigating the verification of autonomy, cyber-physical systems, and neural networks. He strives to develop practical formal methods that are both scalable and useful, which demands developing new theory, programming efficient tools and building experimental systems.
Stanley Bak received a Bachelor's degree in Computer Science from Rensselaer Polytechnic Institute (RPI) in 2007 (summa cum laude), and a Master's degree in Computer Science from the University of Illinois at Urbana-Champaign (UIUC) in 2009. He completed his PhD from the Department of Computer Science at UIUC in 2013. He received the Founders Award of Excellence for his undergraduate research at RPI in 2004, the Debra and Ira Cohen Graduate Fellowship from UIUC twice, in 2008 and 2009, and was awarded the Science, Mathematics and Research for Transformation (SMART) Scholarship from 2009 to 2013. From 2013 to 2018, Stanley was a Research Computer Scientist at the US Air Force Research Lab (AFRL), both in the Information Directorate in Rome, NY, and in the Aerospace Systems Directorate in Dayton, OH. He helped run Safe Sky Analytics, a research consulting company investigating verification and autonomous systems, and performed teaching at Georgetown University before joining Stony Brook University as an assistant professor in Fall 2020.
Date: Monday, March 15th, 2021 @ 1PM EST.
Talk Title: Functional Synthesis: An Ideal Meeting Ground for Formal Methods and Machine Learning
Abstract: Don't we all dream of the perfect assistant whom we can just tell what to do and the assistant can figure out how to accomplish the tasks? Formally, given a specification F(X,Y) over the set of input variables X and output variables Y, we want the asssistant, aka functional synthesis engine, to design a function G such that (X,Y=G(X)) satisfies F. Functional synthesis has been studied for over 150 years, dating back Boole in 1850's and yet scalability remains a core challenge. Motivated by progress in machine learning, we design a new algorithmic framework Manthan, which views functional synthesis as a classification problem, relying on advances in constrained sampling for data generation, and advances in automated reasoning for a novel proof-guided refinement and provable verification. On an extensive and rigorous evaluation over 609 benchmarks, we demonstrate that Manthan significantly improves upon the current state of the art, solving 356 benchmarks in comparison to 280, which is the most solved by a state of the art technique; thereby, we demonstrate an increase of 76 benchmarks over the current state of the art. The significant performance improvements, along with our detailed analysis, highlights several interesting avenues of future work at the intersection of machine learning, constrained sampling, and automated reasoning.
Bio: Kuldeep Meel is Sung Kah Kay Assistant Professor in the Computer Science Department of School of Computing at National University of Singapore. His research interests lie at the intersection of Formal Methods and Artificial Intelligence. He is a recipient of 2019 NRF Fellowship for AI, and was named AI's 10 to Watch by IEEE Intelligent Systems in 2020. His work received the 2018 Ralph Budd Award for Best PhD Thesis in Engineering, 2014 Outstanding Masters Thesis Award from Vienna Center of Logic and Algorithms and Best Student Paper Award at CP 2015.He received his Ph.D. (2017) and M.S. (2014) degree from Rice University, and B. Tech. (with Honors) degree (2012) in Computer Science and Engineering from Indian Institute of Technology, Bombay.
Talk Title: Fairness, Explainability, and Privacy in AI/ML Systems
Abstract: How do we develop machine learning models and systems taking fairness, accuracy, explainability, and transparency into account? How do we protect the privacy of users when building large-scale AI based systems? Model fairness and explainability and protection of user privacy are considered prerequisites for building trust and adoption of AI systems in high stakes domains such as lending and healthcare requiring reliability, safety, and fairness.
We will first motivate the need for adopting a “fairness, explainability, and privacy by design” approach when developing AI/ML models and systems for different consumer and enterprise applications from the societal, regulatory, customer, end-user, and model developer perspectives. We will then focus on the application of fairness-aware ML, explainable AI, and privacy-preserving AI techniques in practice through industry case studies. We will discuss the sociotechnical dimensions and practical challenges, and conclude with the key takeaways and open challenges.
Bio: Krishnaram Kenthapadi is a Principal Scientist at Amazon AWS AI, where he leads the fairness, explainability, and privacy initiatives in Amazon AI platform. Until recently, he led similar efforts at LinkedIn AI team, and served as LinkedIn’s representative in Microsoft’s AI and Ethics in Engineering and Research Advisory Board. Previously, he was a Researcher at Microsoft Research, where his work resulted in product impact (and Gold Star / Technology Transfer awards), and several publications/patents. Krishnaram received his Ph.D. in Computer Science from Stanford University in 2006. He serves regularly on the program committees of KDD, WWW, WSDM, and related conferences, and co-chaired the 2014 ACM Symposium on Computing for Development. His work has been recognized through awards at NAACL, WWW, SODA, CIKM, ICML AutoML workshop, and Microsoft’s AI/ML conference. He has published 40+ papers, with 2500+ citations and filed 140+ patents (30+ granted). He has presented lectures/tutorials on privacy, fairness, and explainable AI at KDD ’18 ’19, WSDM ’19, WWW ’19 ’20, FAccT ’20, and AAAI ’20.
Date: Monday, April 19th, 2021 @ 4PM.
Talk Title: Where Neural Networks Fail: The Case for a Little Help from Knowledge
Abstract: Today's dominant approach for modeling complex tasks involving human language calls for training neural networks using massive datasets. While the agenda is undeniably successful, we may not have the luxury of annotated data for every task or domain of interest. Reducing dependence on labeled examples may require us to rethink how we supervise models.
In this talk, I will discuss some failures of today's end-to-end trained neural networks. Specifically, I will focus on examples that illustrate their inability to internalize knowledge about the world. Following this, I will describe our work on using knowledge to inform neural networks without introducing additional parameters. Declarative rules stated in logic can be systematically compiled into computation graphs that augment the structure of neural models, and also into regularizers that can use labeled or unlabeled examples. I will present experiments involving text understanding which show that such declaratively constrained neural networks can successfully internalize the information in the rules, providing an easy-to-use mechanism for supervising neural networks that does not involve data annotation.
Bio: Vivek Srikumar is associate professor in the School of Computing at the University of Utah. His research lies in the areas of natural language processing and machine learning and has been driven by questions arising from the need to reason about textual data with limited explicit supervision and to scale NLP to large problems. His work has been published in various AI, NLP and machine learning venues and has been recognized by paper awards/honorable mention from EMNLP and CoNLL. His work has been supported by awards from the National Science Foundation, and also from Google, Intel and Verisk. He obtained his Ph.D. from the University of Illinois at Urbana-Champaign in 2013 and was a post-doctoral scholar at Stanford University.
Date: Monday, April 26th, 2021 @ 4PM.
Talk Title: Unifying Logical and Statistical AI with Markov Logic
Abstract: Intelligent systems must be able to handle the complexity and uncertainty of the real world. Markov logic enables this by unifying first-order logic and probabilistic graphical models into a single representation. Many deep architectures are instances of Markov logic. An extensive suite of learning and inference algorithms for Markov logic has been developed, along with open source implementations like Alchemy. Markov logic has been applied to natural language understanding, information extraction and integration, robotics, social network analysis, computational biology, and many other areas.
Bio: Pedro Domingos is a professor of computer science at the University of Washington and the author of "The Master Algorithm". He is a winner of the SIGKDD Innovation Award and the IJCAI John McCarthy Award, two of the highest honors in data science and AI, and a Fellow of the AAAS and AAAI. His research spans a wide variety of topics in machine learning, artificial intelligence, and data science. He helped start the fields of statistical relational AI, data stream mining, adversarial learning, machine learning for information integration, and influence maximization in social networks.
Talk Title: Unifying Logical and Statistical AI with Markov Logic
Abstract: Intelligent systems must be able to handle the complexity and uncertainty of the real world. Markov logic enables this by unifying first-order logic and probabilistic graphical models into a single representation. Many deep architectures are instances of Markov logic. An extensive suite of learning and inference algorithms for Markov logic has been developed, along with open source implementations like Alchemy. Markov logic has been applied to natural language understanding, information extraction and integration, robotics, social network analysis, computational biology, and many other areas.
Bio: Pedro Domingos is a professor of computer science at the University of Washington and the author of "The Master Algorithm". He is a winner of the SIGKDD Innovation Award and the IJCAI John McCarthy Award, two of the highest honors in data science and AI, and a Fellow of the AAAS and AAAI. His research spans a wide variety of topics in machine learning, artificial intelligence, and data science. He helped start the fields of statistical relational AI, data stream mining, adversarial learning, machine learning for information integration, and influence maximization in social networks.