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
C. Thi Nguyen: Values, Legibility, and Gamification [not-audio_url] [/not-audio_url]

Duration: 1:30:13
Episode 127I spoke with Christopher Thi Nguyen about:* How we lose control of our values* The tradeoffs of legibility, aggregation, and simplification* Gamification and its risksEnjoy—and let me know what you think!C. Th…
Vivek Natarajan: Towards Biomedical AI [not-audio_url] [/not-audio_url]

Duration: 1:55:03
Episode 126I spoke with Vivek Natarajan about:* Improving access to medical knowledge with AI* How an LLM for medicine should behave* Aspects of training Med-PaLM and AMIE* How to facilitate appropriate amounts of trust…
Thomas Mullaney: A Global History of the Information Age [not-audio_url] [/not-audio_url]

Duration: 1:43:45
Episode 125False universalism freaks me out. It doesn’t freak me out as a first principle because of epistemic violence; it freaks me out because it works. I spoke with Professor Thomas Mullaney about:* Telling stories a…
Seth Lazar: Normative Philosophy of Computing [not-audio_url] [/not-audio_url]

Duration: 1:50:17
Episode 124You may think you’re doing a priori reasoning, but actually you’re just over-generalizing from your current experience of technology.I spoke with Professor Seth Lazar about:* Why managing near-term and long-te…
Suhail Doshi: The Future of Computer Vision [not-audio_url] [/not-audio_url]

Duration: 1:08:07
Episode 123I spoke with Suhail Doshi about:* Why benchmarks aren’t prepared for tomorrow’s AI models* How he thinks about artists in a world with advanced AI tools* Building a unified computer vision model that can gener…
Azeem Azhar: The Exponential View [not-audio_url] [/not-audio_url]

Duration: 1:46:25
Episode 122I spoke with Azeem Azhar about:* The speed of progress in AI* Historical context for some of the terminology we use and how we think about technology* What we might want our future to look likeAzeem is an entr…
David Thorstad: Bounded Rationality and the Case Against Longtermism [not-audio_url] [/not-audio_url]

Duration: 2:19:02
Episode 122I spoke with Professor David Thorstad about:* The practical difficulties of doing interdisciplinary work* Why theories of human rationality should account for boundedness, heuristics, and other cognitive limit…
Michael Sipser: Problems in the Theory of Computation [not-audio_url] [/not-audio_url]

Duration: 1:28:21
In episode 119 of The Gradient Podcast, Daniel Bashir speaks to Professor Michael Sipser.Professor Sipser is the Donner Professor of Mathematics and member of the Computer Science and Artificial Intelligence Laboratory a…

«1234567...10»