V&V takes on “Pacing the frontier”

[Cross-posted to LW. These short takes try to put a verification-and-validation slant on AI-safety / alignment topics – they are not full treatments. I co-originated coverage-driven verification (CDV), and spent several decades doing verification of chips and AVs. See intro post for background.] Summary: The latest frontier model incidents resulted in the “Pacing the frontier” letter and subsequent … More V&V takes on “Pacing the frontier”

V&V takes on OpenAI’s long-horizon incidents

[Cross-posted to LW. These short takes try to put a verification-and-validation slant on AI-safety / alignment topics – they are not full treatments. I co-originated coverage-driven verification (CDV), and spent several decades doing verification of chips and AVs. See intro post for background.] On July 20 and 21, OpenAI published two unusually candid incident reports: … More V&V takes on OpenAI’s long-horizon incidents

When is misalignment just a bug? 

[LW linkpost is here] Introduction and epistemic status: This is the first post in a planned series, “Alignment as a verification problem”. I co-originated coverage-driven verification (CDV), which became the standard methodology for chip verification and is heavily used in AV safety. Back in 2015 I wrote that verifying “Friendly AI” would be our biggest … More When is misalignment just a bug? 

Coverage-driven alignment – What ‘Teaching Claude Why’ can borrow from AV verification

Summary: This post suggests that alignment training could benefit from coverage-driven verification. Anthropic recently reported that teaching Claude alignment rules (via pretraining-style next-token learning on alignment-related stories) is more effective than relying primarily on RL-style behavioral shaping. Some AV developers reached a related conclusion, but in addition tend to use a systematic, coverage-driven methodology for … More Coverage-driven alignment – What ‘Teaching Claude Why’ can borrow from AV verification

GPT-3 and verification

Summary: This post talks about GPT-3, a new Machine Learning (ML) system currently making waves in the ML community. It explains why GPT-3 is a big deal, and then considers the verification implications of such systems. One way to look at GPT-3 (and the even-bigger GPT-4, GPT-5 etc. which are sure to follow) is as … More GPT-3 and verification

On Mobileye’s formal model of AV safety

Summary: This short post talks about Mobileye’s new paper (regarding a formal approach to Autonomous Vehicles safety). It claims that the paper has several issues, but is nevertheless an important start. Mobileye came out with a paper titled “On a Formal Model of Safe and Scalable Self-driving Cars” (Bloomberg coverage, summary paper, full pdf). Their … More On Mobileye’s formal model of AV safety

Where Machine Learning meets rule-based verification

Summary: This post addresses some high-level questions like: Longer term, how much of the verification of Intelligent Autonomous Systems can be done with just Machine Learning (ML)? Should most requirements remain rule-based, and if so – how does that connect to the ML part? And how will the uneasy interface between ML and rules influence … More Where Machine Learning meets rule-based verification

DeepXplore and new ideas for verifying ML systems

Summary: This post talks about the DeepXplore paper, and uses it to revisit the topic of verification of ML-based systems The paper DeepXplore: Automated Whitebox Testing of Deep Learning Systems (by folks from Columbia U and Lehigh U) describes a new and (in my view) pretty important way to verify ML-based systems. And it somehow … More DeepXplore and new ideas for verifying ML systems