Talia Ringer: Formal Verification and Deep Learning

Talia Ringer: Formal Verification and Deep Learning

Author: Daniel Bashir May 25, 2023 Duration: 1:45:35
The Gradient: Perspectives on AI
TechnologyScience

In episode 74 of The Gradient Podcast, Daniel Bashir speaks to Professor Talia Ringer.

Professor Ringer is an Assistant Professor with the Programming Languages, Formal Methods, and Software Engineering group at the University of Illinois at Urbana Champaign. Their research leverages proof engineering to allow programmers to more easily build formally verified software systems.

Have suggestions for future podcast guests (or other feedback)? Let us know here or reach us at editor@thegradient.pub

Subscribe to The Gradient Podcast:  Apple Podcasts  | Spotify | Pocket Casts | RSSFollow The Gradient on Twitter

Outline:

* (00:00) Daniel’s long annoying intro

* (02:15) Origin Story

* (04:30) Why / when formal verification is important

* (06:40) Concerns about ChatGPT/AutoGPT et al failures, systems for accountability

* (08:20) Difficulties in making formal verification accessible

* (11:45) Tactics and interactive theorem provers, interface issues

* (13:25) How Prof Ringer’s research first crossed paths with ML

* (16:00) Concrete problems in proof automation

* (16:15) How ML can help people verifying software systems

* (20:05) Using LLMs for understanding / reasoning about code

* (23:05) Going from tests / formal properties to code

* (31:30) Is deep learning the right paradigm for dealing with relations for theorem proving?

* (36:50) Architectural innovations, neuro-symbolic systems

* (40:00) Hazy definitions in ML

* (41:50) Baldur: Proof Generation & Repair with LLMs

* (45:55) In-context learning’s effectiveness for LLM-based theorem proving

* (47:12) LLMs without fine-tuning for proofs

* (48:45) Something ~ surprising ~ about Baldur results (maybe clickbait or maybe not)

* (49:32) Asking models to construct proofs with restrictions, translating proofs to formal proofs

* (52:07) Methods of proofs and relative difficulties

* (57:45) Verifying / providing formal guarantees on ML systems

* (1:01:15) Verifying input-output behavior and basic considerations, nature of guarantees

* (1:05:20) Certified/verifies systems vs certifying/verifying systems—getting LLMs to spit out proofs along with code

* (1:07:15) Interpretability and how much model internals matter, RLHF, mechanistic interpretability

* (1:13:50) Levels of verification for deploying ML systems, HCI problems

* (1:17:30) People (Talia) actually use Bard

* (1:20:00) Dual-use and “correct behavior”

* (1:24:30) Good uses of jailbreaking

* (1:26:30) Talia’s views on evil AI / AI safety concerns

* (1:32:00) Issues with talking about “intelligence,” assumptions about what “general intelligence” means

* (1:34:20) Difficulty in having grounded conversations about capabilities, transparency

* (1:39:20) Great quotation to steal for your next thinkpiece + intelligence as socially defined

* (1:42:45) Exciting research directions

* (1:44:48) Outro

Links:

* Talia’s Twitter and homepage

* Research

* Concrete Problems in Proof Automation

* Baldur: Whole-Proof Generation and Repair with LLMs

* Research ideas



Get full access to The Gradient at thegradientpub.substack.com/subscribe

Hosted by Daniel Bashir, The Gradient: Perspectives on AI moves beyond surface-level headlines to explore the intricate machinery and human ideas shaping artificial intelligence. Each episode is built on a foundation of deep research, leading to conversations that are both technically substantive and broadly accessible. You'll hear from researchers, engineers, and philosophers who are actively building and critiquing our technological future, discussing not just how AI systems work, but the larger implications of their integration into society. This isn't about speculative hype; it's a grounded examination of real progress, persistent challenges, and ethical considerations from those on the front lines. The discussions peel back layers on topics like model architecture, policy, and the fundamental science behind the algorithms becoming part of our daily lives. For anyone curious about the substance behind the buzz-whether you have a technical background or are simply keen to understand a defining technology of our age-this podcast offers a crucial and thoughtful resource. Tune in for a consistently detailed and nuanced take that treats artificial intelligence with the complexity it deserves.
Author: Language: English Episodes: 100

Official website RSS
spotify
The Gradient: Perspectives on AI
Podcast Episodes
Stevan Harnad: AI's Symbol Grounding Problem [not-audio_url] [/not-audio_url]

Duration: 1:58:21
In episode 88 of The Gradient Podcast, Daniel Bashir speaks to Professor Stevan Harnad.Stevan Harnad is professor of psychology and cognitive science at Université du Québec à Montréal, adjunct professor of cognitive sci…
Terry Winograd: AI, HCI, Language, and Cognition [not-audio_url] [/not-audio_url]

Duration: 1:33:21
In episode 87 of The Gradient Podcast, Daniel Bashir speaks to Professor Terry Winograd. Professor Winograd is Professor Emeritus of Computer Science at Stanford University. His research focuses on human-computer interac…
Gil Strang: Linear Algebra and Deep Learning [not-audio_url] [/not-audio_url]

Duration: 1:00:36
In episode 86 of The Gradient Podcast, Daniel Bashir speaks to Professor Gil Strang. Professor Strang is one of the world’s foremost mathematics educators and a mathematician with contributions to finite element theory,…
Anant Agarwal: AI for Education [not-audio_url] [/not-audio_url]

Duration: 47:40
In episode 85 of The Gradient Podcast, Andrey Kurenkov speaks to Anant AgarwalAnant Agarwal is the chief platform officer of 2U, and founder of edX. Anant taught the first edX course on circuits and electronics from MIT,…
Peli Grietzer: A Mathematized Philosophy of Literature [not-audio_url] [/not-audio_url]

Duration: 2:33:33
In episode 83 of The Gradient Podcast, Daniel Bashir speaks to Peli Grietzer. Peli is a scholar whose work borrows mathematical ideas from machine learning theory to think through “ambient” and ineffable phenomena like m…
Ryan Drapeau: Battling Fraud with ML at Stripe [not-audio_url] [/not-audio_url]

Duration: 1:06:31
In episode 82 of The Gradient Podcast, Daniel Bashir speaks to Ryan Drapeau.Ryan is a Staff Software Engineer at Stripe and technical lead for Stripe’s Payment Fraud organization, which uses machine learning to help prev…
Shiv Rao: Enabling Better Patient Care with AI [not-audio_url] [/not-audio_url]

Duration: 1:00:51
In episode 81 of The Gradient Podcast, Daniel Bashir speaks to Shiv Rao.Shiv Rao, MD is the co-founder and CEO of Abridge, a healthcare conversation company that uses cutting-edge NLP and generative AI to bring context a…
Hugo Larochelle: Deep Learning as Science [not-audio_url] [/not-audio_url]

Duration: 1:48:28
In episode 80 of The Gradient Podcast, Daniel Bashir speaks to Professor Hugo Larochelle. Professor Larochelle leads the Montreal Google DeepMind team and is adjunct professor at Université de Montréal and a Canada CIFAR…
Jeremie Harris: Realistic Alignment and AI Policy [not-audio_url] [/not-audio_url]

Duration: 1:30:35
In episode 79 of The Gradient Podcast, Daniel Bashir speaks to Jeremie Harris.Jeremie is co-founder of Gladstone AI, author of the book Quantum Physics Made Me Do It, and co-host of the Last Week in AI Podcast. Jeremy pr…

«1...345678910»