AI Alignment at Which Abstraction Level?

This post is crossposted from my Substack, Structure and Guarantees, where I explore how formal verification and related ideas might scale to more complex intelligent systems. Here I start from the observation that AI alignment usually takes for granted a privileged role for human values, without asking why values should come from that particular abstraction level. I then give an independent engineering reason to worry about putting humans at the center of an alignment specification, drawing on lessons from formal verification at scale. I’ve been arguing recently for a solution to the apparent chaos of current use of generative AI to write software: perhaps use these AI systems to help write truly unambiguous formal specifications, but then let those formal descriptions persist, auditing them carefully and using tools that reliably write code as we know it, given specifications. I made the case in one original article and then a follow-up responding to comments on the first. I ended the latter by promising to get into the highest-profile specification-writing challenge of our times: AI alignment. Here is the first of three articles giving my perspective. First, I think a bit about my personal background is relevant. I have specialized in how to scale formal verification to apply to realistic systems without imposing unrealistic costs on engineers. Just to keep things interesting, I typically add another requirement: we want to minimize the trusted base of any given verification. In other words, imagine someone builds an artifact and formally verifies it. The trusted base includes every line of code where a bug could have led to accepting an artifact that actually doesn’t align with the author’s intent. We can find that the trusted base includes code of the artifact, say for the hardware if we have only proved software; code of the formal-verification tool, in the common case where it hasn’t itself been formally verified; or code of further infrastructure underneath either, like an operating system we trust to run the verification software. I’ll have plenty to say in later articles about the best practices of my community in this regard and how they may be helpful to seemingly new problems around AI. The important upshot for now, though, is that my perspective is one of an engineer. My projects almost always involve building nontrivial artifacts alongside their machine-checked proofs. These are serious proofs checked into version control and often developed by multiple collaborating engineers. Little conceptual mistakes can lead to the proofs being rejected. It’s an activity that doesn’t seem to map well to mainstream AI-alignment work. On the one hand, we have best-effort projects to align and evaluate current AI models, without any particular theoretical guarantees. On the other hand, we have writing more in the register of philosophy (some to be cited shortly) that tackles the big questions of artificial general intelligence and how it may come about from recursive self-improvement. There are no rigorous proofs about complex implementations, because those implementations don’t exist yet or are diabolically unstructured in our present understanding and thus resistant to proof. As a result, it is easy to miss small conceptual problems that doom certain frameworks. I’m not saying I’ve pinpointed those problems! I just know from experience that the probability is near 100% that any complex system that hasn’t gone through rigorous formal verification is actually incorrect. So let’s talk what makes for a good specification in the spirit of AI alignment, treated as part of a formal-methods project with familiar engineering considerations. By the way, I’m a newcomer to the world of alignment and will appreciate any dialogue about influential and related writing that I’ve missed. Our first stop in this article may seem like a bit of a swerve from the topic I just promised, but please bear with me. We will return to a formal-methods perspective on why we may not want to center humans in the top-level formulation of alignment, even if we play an important role internally. Abstraction Layers of Life as We Know It The field of AI alignment so far has generated some big and nonobvious ideas. What is called the value identification problem is basically figuring out the right specification for AI, from the perspective of some thinking agent that we want to privilege morally. The principle of complexity of value asserts that there is no short description of human values; there is fundamental complexity in what we have wound up wanting. This principle sounds like bad news for writing down human values as a formal specification! A well-known alternative proposal involves a kind of epistemic humility by advanced AIs, through the notion of coherent extrapolated volition (CEV). The idea is that the AI’s starting specification is that it should figure out what humans would really want, if they were augmented in certain ways. Th