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. Then that derived specification should become primary.

The place where I get stuck is why we assumed centrality of humans in the value-identification problem, and I’ll explain two kinds of objections, in this section and the next, one philosophical and one grounded in the pragmatics of formal verification. These objections stand independently of each other.

I think it’s widely recognized in the field that formulating this CEV objective is very challenging, which certainly sounds right from a formal-methods perspective. Still, I run into an objection to it, even presuming perfect formalization of what it means to learn human preferences. The problem is potential conduct of an AI during the period when it is learning our preferences. Assume it doesn’t yet have perfect models of our behavior, so it can only learn through real observation of humans. What’s to stop it from putting us all in vats, Matrix-style, constantly running us through different VR scenarios, to most efficiently figure out our preference structure? Or, substantially less outlandishly, what’s to stop it from taking over our social-media feeds to try to provoke different emotions, learning our preferences at the same time as triggering social problems as we already see from infinite-scroll social media today? It’s not like we can assume some bootstrap morality that flags those tactics as unsavory; finding the bootstrap morality isn’t obviously an easier or different problem. Even if the AI eventually creates genuine paradise compatible with our values, we might object to the intervening dark ages of manipulation. (ChatGPT directed me to a recent paper by Emmons et al. studying a related problem more technically.) Now, it turns out that the rest of this section can proceed independently of this point, so I mostly include it in case readers have good references to share for prior art.

At some level, human centrality is obvious: humans are designing AI (for now), and humans want what we want. However, there is a familiar historical narrative of progress that depends on seeing ourselves as less and less central in the grand scheme of things. Copernicus argued that the Earth revolves around the Sun, not the other way around. Darwin argued that humans resulted from an evolutionary process that produced all of life as we know it, giving us no special place in the grand scheme of things. If we’re not a natural endpoint of a universal process, why should we give ourselves that status in the goals of powerful AI?

Bostrom in Superintelligence considers other approaches to indirect normativity, which try to avoid centering human values, but to me these formulations seem to run into trouble for assuming the major problem of specifying human morality is already solved, even if one formulation (“moral rightness”) is couched in terms of universal, not human, morality. I personally am convinced by moral anti-realism and see the case for universal morality as weak, as morality arises from evolutionary forces and should be expected to be different in different times and places.

My argument here is related to moral circle expansion, a philosophical concept that explains our potential granting of more moral standing to nonhuman animals and AIs alike. For instance, imagining our ancestors formulating alignment as recently as 150 years ago, it may have been “clear” that only a writer’s own race deserved consideration, a principle that we now find repugnant. We could perhaps say that I’m taking that principle to a more abstract level, where we see, say, humans and cows as representatives of roughly the same abstraction level of the universe, raising the question of what makes that level special.

Let’s consider the same question from more of an engineering perspective. Life can naturally be organized in layers, and we can imagine formulating alignment from the perspective of each layer, which can lead to very different outcomes via powerful AI systems, each outcome looking undesirable from other layers’ vantage points. What makes the layer of individual humans special – special enough to get this treatment in alignment?

I will have more to say on the biological version of this picture next time. I’m not, by the way, implying that atoms have human-style preferences. The point is more that it’s hard to formalize “preference” in some way that isn’t sneaking in a special role for humans. One common answer is that the organism layer is distinguished in supporting consciousness, but I’ve already argued against the big-picture utility of that word and won’t relitigate here.

One related alignment idea is natural abstraction: the idea that well-engineered thinking systems will develop the same abstractions for making sense of the vast physical world, because those abstractions just work, and thus we can assume that AI will evolve toward abstractions familiar to us, and we can specify alignment in terms of those abstractions without worry of (gross) misinterpretation. This perspective doesn’t tell us which of many abstractions to extract values from, though, including in situations as in the diagram with agents nested inside each other. That nesting also figures in the idea of embedded agency, which considers how agents should plan changes to complex worlds that include themselves. One subproblem is how agents should plan the creation of nested agents that do helpful supporting work. This perspective doesn’t seem to answer who deserves to be allowed to specify values: in the case of evolution optimizing humans who optimize Python programs, neither extreme orientation (toward highest-level or lowest-level optimizers) gives us the expected answer.

Engineers are used to thinking of systems at different levels of abstraction, and it’s jarring to call out one level as getting special treatment. Kurzweil in The Singularity is Near grounds the history of the universe in development of increasingly complex patterns, with nesting structure like I just sketched, but overloads the term “humanity” to cover whatever artificial intelligence we design, too. On one level, it solves the puzzle to decide that “human” is a synonym for the whole history of the universe, or at least the upcoming part for our own neighborhood in space! That move seems to me like hiding from the problem, though, if we think in terms of some greater cosmic destiny centered on forms of intelligence beyond our comprehension – and which, by the way, would be very helpful to us if they liked us.

Controlling Specification Complexity

Let’s snap back to the formal-methods engineer’s perspective. Whether we are formalizing human values directly or expressing what it means for a system to seek them out and then honor them, it sounds like one heck of a complex specification, and formal-methods people know that complex specifications create the biggest risk for assurance. Humans become an example of a complex legacy system, absolutely the worst kind to tackle for correctness-critical specifications. We evolved without selection pressure for our values to be understandable to computer code, so there’s no reason to think this problem is especially tractable. Maybe this problem is nonetheless the important one, and we just have to find a way to solve it, but let me continue explaining why it’s worrying (and then the next article will get into considering how the problem might actually be avoidable).

The trouble is that complexity in a specification tends to force complexity in an implementation, as code is added to deal with all the challenges that have been spelled out. Then, in turn, complexity of these two promotes complexity of a mathematical proof of correctness, which naturally references all parts of the specification and implementation. We may find that the specification includes N distinct concerns, and interaction among every pair of them (the feature interaction problem) needs to be treated explicitly in the proof, for N^2 required cases. This phenomenon should make us very wary to put a complex legacy system in the specification.

At this point, I’m imagining objections that sometimes we only know how to build systems including some complex parts. The usual saving grace for formal methods is the one I explained around surprising payoffs of end-to-end formal verification. Namely, sometimes it is easier to be sure we got a specification problem right by doing proof about a larger artifact that includes the original as one component. Why? The new top-level system may admit a simpler specification, and the original system’s specification becomes just part of internal implementation and proof details. If the inner system has a specification bug, either we catch it in the course of verifying the larger system or the bug turned out to be inconsequential for our larger goal.

Maybe the hard-to-decipher “humans” of the programming world are complex, popular programming languages like C. Assume for the moment (though I have argued to the contrary and will come back to doing so in later articles!) that building realistic computer systems requires using these programming languages. Are we out-of-luck, now needing to include formal semantics of the languages in our top-level system specifications? Not if we make the right architectural choices! If we also formally verify the implementations of the programming languages, then choice of language becomes an internal implementation detail, with no representation in the top-level specification that we should submit to careful auditing, testing, and so on. I presented one of my own projects that achieves as much, also crossing the hardware-software interface off the list of top-level specification complexities, by verifying the hardware, too.

Another great example from programming is memory safety. Here we are dealing with what is, in practice, a somewhat-nebulous property, governing how different pieces of code can share computer memory harmoniously, with clear rules for who is allowed to access what. Everyone knows C is not memory-safe, while Rust is memory-safe – but what does that statement really mean? We could try to put together a grand unifying theory of memory safety, but I argue that the real importance of memory safety is that it allows modular reasoning. That is, in the presence of memory safety, it is tractable to divide a program up into modules and give each one a separate specification and proof, without unreasonable interaction across the specifications, because we know modules won’t generally trash each others’ memory. Therefore, the mere ability to prove interesting behavioral theorems modularly demonstrates a desirable quality that subsumes what we really wanted from memory safety – and we avoided needing to define “memory safety” formally. (Incidentally, others have formalized a related intuition.) This observation is related to the one I wrote about where resistance to security vulnerabilities follows almost for free.

So, even if humans are central to the story for what constitutes AI alignment, it need not mean that the “top-level specification” of AI says anything about humans! Future AI systems could construct sophisticated models of humans, and the utility of those models to meet some ultimate goal could be proved from first principles, without putting those models in the trusted base. While we humans differ from programming languages in having evolved rather than been designed, the gap could perhaps be made up by formally verified AI scientists studying humans or whatever other relevant phenomenon, a topic I hope to return to in later articles.

Conclusion

Maybe we just won’t be smart enough to construct an initial specification of alignment that avoids bringing in complex modeling of humans, but I hope I’ve made some kind of case that it’s worth trying. I also want to reiterate that I’m using this article partly to get feedback about existing writing I should check out for its connections to (and potential poking of holes in) what I’ve written here. My next article will give one example of an approach to alignment that genuinely avoids including anything about humans in its top-level specification, while plausibly meeting our informal requirements for alignment. The last article in the trio will consider the infamous example of the paperclip maximizer and some potential mitigations against allowing one to develop.