Formal Methods for Frontier AI Systems
summary
Claims a concrete verifier that computes the probability mass of unsafe outputs for a single prompt (not just samples), implements a token-tree/ frontier search and prunes by prefix, and scales to 70B models using the Beaver algorithm (33 forward passes often suffices). Rejection sampling is the baseline; on 204 cyber‑sec jailbreak prompts the method flags >10% unsafe mass where sampling misses it. A DSL Lumos defines prompt distributions and Amazon uses these evaluations for Nova; synthesized SEA self‑evolving agents verify with Daphne and reach ≈97% conformance while improving task utility.
AI-written summary · about
chapters (15)
- 0:00Introduction
- 1:54Why formal methods matter
- 7:15Offline evaluation with verification
- 17:16Single prompt risk assessment
- 26:22Math reasoning and code generation
- 31:16Prompt distribution testing
- 37:39Reading comprehension tests
- 42:59Catastrophic risk in long conversations
- 46:29Online enforcement constraints
- 51:10Decoding strategies for constraints
- 53:57Enforcing LTL constraints
- 56:49Auto agents and self-evolving programs
- 1:00:23Formal constraints in synthesis
- 1:04:18Interpretability and regularization
- 1:05:41Future directions
related talks
50mFrom Prompt Hacking to Architectural Determinism: Engineering Reliable GenAI Systems
37mShort Industry Talks pt.2
11mThe Unreasonable Effectiveness of Prompt Learning
13mPrompt Engineering Simplified
01h 04mIn Prompts We Trust
46mIncreasing the Analysis Surface of Large Language Models
16mNavigating the Uncharted: Ensuring Prompt Quality in the Age of Language Models
43mAdvanced Prompt Engineering and Beyond