Computer-aided Mathematics: Successes, Advances, and Trust

Thursday, November 2, 2023
11am
BA 3200

Abstract:

Progress in satisfiability (SAT) solving has made it possible to determine the correctness of complex systems and answer long-standing open questions in mathematics. The SAT-solving approach is completely automatic and can produce clever though potentially gigantic proofs. We can have confidence in the correctness of the answers because highly trustworthy systems can validate the underlying proofs regardless of their size.

We demonstrate the effectiveness of the SAT approach by presenting some recent successes, including the solution of the Boolean Pythagorean Triples problem, computing the fifth Schur number, and resolving the remaining case of Keller’s conjecture. Moreover, we constructed and validated proofs for each of these results. The second part of the talk focuses on notorious math challenges for which automated reasoning may well be suitable. In particular, we discuss advances in applying SAT-solving techniques to the Hadwiger-Nelson problem (chromatic number of the plane), optimal schemes for matrix multiplication, and the Collatz conjecture.

Bio:

Marijn Heule is an Associate Professor of Computer Science at Carnegie Mellon University. His contributions to automated reasoning have enabled him and others to solve hard problems in formal verification and mathematics. He has developed award-winning satisfiability (SAT) solvers. His preprocessing and proof-producing techniques are used in many state-of-the-art automated reasoning tools. Marijn won multiple best paper awards at international conferences, including at SAT, CADE, IJCAR, TACAS, HVC, LPAR, and IJCAI-JAIR. He is one of the editors of the Handbook of Satisfiability. This 1500+ page handbook (second edition) has become the reference for SAT research.

A Semantical Journey

Thursday, November 30, 2023
11am
BA 3200

Abstract:

In recent joint work with Ningning Xie, we propose an approach to choice-based learning via a combination of algebraic effect handlers and the selection monad. Choice operations are used in training programs written as effectful computations using choose and loss operations; optimization algorithms are implemented separately as choice operation effect handlers making use of losses.

In this talk, I look at the semantical journey which led me to this work. The journey began with Eugenio Moggi's 1989 notions of computation as monads. This inspired my work with John Power and others on the algebraic theory of effects. There was a problem in that theory: how to incorporate exception handlers. This led Matija Pretnar and myself (and now with many others) to algebraic effect handlers. 

In a different direction, Carbune et al's Smart Choices approach to making machine learning a first-class citizen in programming languages gave Martín Abadi the idea that Martín Escardó and Paulo Oliva's selection monad could provide the right semantical framework for programs making smart choices. He and I worked on selection monad semantics for languages making optimal choices. However, optimization algorithms certainly need not make optimal choices, so one needed a way to make optimizing choices. Given the above history it then seemed natural, as hinted at above, to combine selection monad ideas and algebraic effect handlers, thus bringing my semantic journey to the present, with Ningning's and my joint research program on languages for choice-based learning.

Bio:

Professor Gordon Plotkin has been a faculty member at Edinburgh University since 1973. His main interests are in the connections between programming languages and logic, with particular interest in the semantics of programming languages. He has also worked a little on natural language and, more extensively, on systems biology. He may be best known for his invention of structural operational semantics. He is a fellow of the Royal Society and, recently, a member of the American Academy of Arts and Sciences; he is a recipient of the ACM Programming Languages Achievement Award and the EATCS Distinguished Achievements Award. He currently remains on the Edinburgh faculty and is also a Senior Staff Research Scientist at Google DeepMind.

Digital Biomarkers and Immersive Therapeutics in the Age of Virtual Care

Tuesday, December 5, 2023

Abstract:

This talk will present both opportunities and challenges associated with developing and leveraging patient-centric data and devices in the context of virtual care. The past 15 years have witnessed pervasive consumer adoption of digital devices. The application of these technologies to health started with early text-message services, followed by a proliferation of health-related smartphone apps and wearables, chatbots and voice agents, and most recently Extended Reality (XR) based therapies. Meanwhile, clinical research communities are grappling with how to effectively validate and integrate the resulting patient-generated data, digital biomarkers, and digital therapeutics into care. These developments are particularly pertinent today given the increased adoption of virtual care and increasing reliance on recovery and aging in the home setting. 

Bio:

Deborah Estrin is a Professor of Computer Science at Cornell Tech in New York City where she holds The Robert V. Tishman Founder's Chair, serves as the Associate Dean for Impact, and is an Affiliate Faculty at Weill Cornell Medicine. Estrin's current research activities include technologies for caregiving, immersive health, and Public Interest Technology. Estrin was previously the Founding Director of the NSF Center for Embedded Networked Sensing (CENS) at UCLA; pioneering the development of mobile and wireless systems to collect and analyze real time data about the physical world. Estrin co-founded the non-profit startup, Open mHealth, and has served on several scientific advisory boards for early stage mobile health startups and as an Amazon Scholar. Estrin's honors include: the IEEE Internet Award (2017), MacArthur Fellowship (2018), and the IEEE John von Neumann Medal (2022). She is an elected member of the American Academy of Arts and Sciences (2007), the National Academy of Engineering (2009), and the National Academy of Medicine (2019). She received honorary doctorates from EPFL (2008), Uppsala (2011), and Concordia (2023).

Firm Foundations for Private Machine Learning and Statistics

Tuesday, February 27, 2024

Abstract:

How can researchers use sensitive datasets for machine learning and statistics without compromising the privacy of the individuals who contribute their data?  In this talk I will describe my work on the foundations of differential privacy, a rigorous framework for answering this question.  In the past decade, differential privacy has gone from largely theoretical to widely deployed, and a theme of the talk will be how new deployments are forcing us to revisit foundational questions about differential privacy.  This talk will cover a range of issues from the fundamental---like optimal private statistical inference---to the applied---like auditing differentially private machine learning.

Bio:

Jonathan Ullman is an Associate Professor in the Khoury College of Computer Sciences at Northeastern University.  Before joining Northeastern, he received his PhD from Harvard in 2013, and in 2014 was a Junior Fellow in the Simons Society of Fellows.   His research centers on privacy for machine learning and statistics, and its surprising connections to topics like statistical validity, robustness, cryptography, and fairness.  He has been recognized with an NSF CAREER award, research awards from Google and Apple, and the Ruth and Joel Spira Outstanding Teacher Award.

Shaping the Responsible Adoption of AI in Healthcare

Tuesday, April 30, 2024

Abstract:

As the use of artificial intelligence (AI) moves from being a curiosity to a necessity, it is clear that the benefit obtained from using AI models to prioritize care interventions is an interplay of the model’s performance, the capacity to intervene, and the benefit/harm profile of the intervention. We will begin the conversation reviewing the necessary data strategy to enable organization wide AI adoption and leading into a discussion of the core intuition behind foundation models. After a brief review of the kinds of use-cases that AI can serve across multiple medical specialties, we will discuss Stanford Healthcare’s efforts to shape the adoption of health AI tools to be useful, reliable, and fair so that they lead to cost-effective solutions that meet health care's needs. We will conclude with the rationale and vision for collaborative activities such as the Coalition for Health AI. The conversation will draw on examples from multiple specialities including Pathology, Cardiology, Internal Medicine, Surgery, Psychiatry and Oncology.

Bio:

Dr. Nigam Shah is Professor of Medicine at Stanford University, and Chief Data Scientist for Stanford Health Care. His research is focused on bringing AI into clinical use, safely, ethically and cost-effectively. Dr. Shah is an inventor on eight patents, has authored over 200 scientific publications, and has co-founded three companies. Dr. Shah was inducted into the American College of Medical Informatics (ACMI) in 2015 and the American Society for Clinical Investigation (ASCI) in 2016. He holds an MBBS from Baroda Medical College, India, a PhD from Penn State University and completed postdoctoral training at Stanford University.

Memory-Centric Computing

Tuesday May 7, 2024

Abstract:

Computing is bottlenecked by data. Large amounts of application data overwhelm storage capability, communication capability, and computation capability of the modern machines we design today. As a result, many key applications' performance, efficiency, and scalability are bottlenecked by data movement. In this talk, we describe three major shortcomings of modern architectures in terms of 1) dealing with data, 2) taking advantage of the vast amounts of data, and 3) exploiting different semantic properties of application data. We argue that an intelligent architecture should be designed to handle data well. We posit that handling data well requires designing architectures based on three key principles: 1) data-centric, 2) data-driven, 3) data-aware. We give several examples for how to exploit each of these principles to design a much more efficient and high performance computing system. We especially discuss recent research that aims to fundamentally reduce memory latency and energy, and practically enable computation close to data, with at least two promising directions: 1) processing using memory, which exploits analog operational properties of memory chips to perform massively-parallel operations in memory, with low-cost changes, 2) processing near memory, which integrates sophisticated additional processing capability in memory controllers, the logic layer of 3D-stacked memory technologies, or memory chips to enable high memory bandwidth and low memory latency to near-memory logic. We show both types of architectures can enable orders of magnitude improvements in performance and energy consumption of many important workloads, such as graph analytics, database systems, machine learning, video processing, climate modeling, genome analysis. We discuss how to enable adoption of such fundamentally more intelligent architectures, which we believe are key to efficiency, performance, and sustainability. We conclude with some research opportunities in and guiding principles for future computing architecture and system designs.

Bio:

Onur Mutlu is a Professor of Computer Science at ETH Zurich. He is also a Visiting Professor at Stanford University and a faculty member at Carnegie Mellon University, where he previously held the Strecker Early Career Professorship. His current broader research interests are in computer architecture, systems, hardware security, and bioinformatics. A variety of techniques he, along with his group and collaborators, has invented over the years have influenced industry and have been employed in commercial microprocessors and memory/storage systems. He obtained his PhD and MS in ECE from the University of Texas at Austin and BS degrees in Computer Engineering and Psychology from the University of Michigan, Ann Arbor. He started the Computer Architecture Group at Microsoft Research (2006-2009), and held various product and research positions at Intel Corporation, Advanced Micro Devices, VMware, and Google. He received various honors for his research, including the Persistent Impact Prize of the Non-Volatile Memory Systems Workshop, the Intel Outstanding Researcher Award, the IEEE High Performance Computer Architecture Test of Time Award, the IEEE Computer Society Edward J. McCluskey Technical Achievement Award, ACM SIGARCH Maurice Wilkes Award and a healthy number of best paper or “Top Pick” paper recognitions at various computer systems, architecture, and security venues. He is an ACM Fellow, IEEE Fellow, and an elected member of the Academy of Europe.