Intelligence Depends on Organizing Computation Correctly and Efficiently

A unifying outline of topics covered so far and where the blog is headed

This post summarizes content so far in one framework, which may feel more coherent than the individual posts as they’ve been flying by. All hyperlinks in this post are to prior posts, so it also serves as a kind of index. I’ll go light on backing up some of the claims I make here. If you’re not convinced by a sentence, follow some of the nearby links for more.

It’s no controversial statement that, as artificial intelligence advances, the details of the computation underneath it matter a lot. My goal with this blog is to think through the design considerations from a new perspective. There are two main “thesis statement” framings that will drive the different topics we cover. They both sound anodyne on the surface, but I’ll be taking them further than most commentators do.

Principle #1: the bidirectional interplay between correctness and efficiency (e.g. running time and power usage) should be central to designing the AI systems of the future. I’m arguing for a central role for formal verification in supporting more ambitious optimization of systems, as the details of optimizations grow past the point that humans can analyze reliably. By using engineering approaches that guarantee correctness, engineers are emboldened to experiment more rapidly with new ideas that improve performance; and then the performance of the tools for formal reasoning becomes an important enabler of a virtuous cycle.

Principle #2: we miss critical opportunities for improvement when we look at systems as they exist today and assume that future systems will have roughly the same kinds of parts with the same local requirements as today. I’ll be arguing for significant changes to both computer hardware and programming languages, but I think it would be a mistake to stop there. We can expand the scope of the systems we are designing to what may be best summarized today as “society-level.” Fields like evolutionary psychology help us understand how humans function today as parts of such systems, leading to certain requirements on computer systems that are not fundamental and that can be beneficial to modify.

Let’s take a look at each principle in more detail.

The Interplay Between Correctness and Efficiency

This principle is going to be more of the usual kind that engineers propose to each other, without threatening professional identities as much as the next one does!

We can see all of scientific and engineering progress as one big distributed algorithm, traditionally staffed by people but with AI increasingly taking over the ideation process. The self-referential process of building high-performance AI systems is a good example (and one that I will return to in later posts), with e.g. algorithmic breakthroughs by human researchers, coupled to automatic translation (e.g. by compilers) of those breakthroughs into low-level code. The boundary between the human and machine contributions is already shifting and may shift dramatically more, making it helpful to consider more broadly the process of finding and validating ideas.

In fact, the evolutionary process that created our brains to do most of the work can be seen as just one part of the same continuing optimization problem. The great challenge of an evolutionary system is getting fast-enough feedback on quality of new variants, whether they are organisms or new software programs. The phenomenon of signaling from psychology and economics can be seen as a neat trick to get earlier high-fidelity feedback on individuals, though there are natural downsides to a convention of intentionally costly displays. An alternative way of moving high-fidelity feedback earlier is formal verification, which lets us evaluate variants in terms of mathematical proof about their behavior in all possible scenarios.

Sometimes lack of confidence in a system optimization or other improvement holds us back from adopting it. Cryptography can help us overcome certain trust problems as ideas and code spread. However, I’m more focused on formal verification as a crucial enabler of adopting ideas, even when we have them ourselves but especially when they come from others we have reason to distrust.

In the first category, consider the example of a recursively self-improving, highly parallel compiler. It constantly invents new tricks to make itself faster and thus able to produce better programs within a given time budget, but how do we know it doesn’t modify itself in a way that compiles all programs into “kill all humans” agents? It is possible to prove that such a process maintains the original purpose of the compiler, through any number of improvement rounds.

In the second category, consider the example of mutually distrusting AI agents sharing code libraries with each other. The paradigm of proof-carrying code makes it possible to distribute code with proofs of fitness for purpose, security, and so on. AI agents can adopt new “brain modules” much more quickly and confidently than humans can, thanks to the chance to check them against the most exacting standards instantly, which is likely to be an important enabler of accelerated progress in science and engineering.

Sometimes poor performance of formal verification limits how much we can achieve of the benefits I just sketched. For example, most of the student research projects I supervise at MIT wind up bottlenecked on the performance of automated-theorem-proving tools. There’s been a successful full-stack effort, from hardware through software programming tools, to enable machine-learning computation based on linear algebra. Formal verification deserves the same effort, and every level of the stack probably winds up looking interestingly different than GPUs and CUDA. I’ve written very little so far about the specifics I have in mind, but expect plenty of posts coming up.

The Importance of Holistic Design

Engineers will all agree that sometimes focusing in on one part of an existing system doesn’t leave enough degrees of freedom to meet some target for improvement. My proposal to reimplement the hardware-software stack to accelerate formal verification fits into that tradition, even as it remains speculative and therefore fair to be skeptical about. And, again, I’ll have plenty to write about details at this level, geeking out about hardware-software codesign. However, more controversially, I want to argue that we can realize even more improvement by broadening the scope of system we consider.

Here are some examples covered by full posts so far, moving up a ladder of abstraction from the physical world to broader cognition.

• Controlling self-driving vehicles seems to involve hard problems of computer vision and more. However, we can circumvent those problems by changing the physical environment so that autonomous vehicles have their own dedicated lanes with intentionally simpler geometry.

• Natural-language processing seems fundamental to many compelling applications of AI. However, a future of AI agents can rely on synthetic languages that are much easier to process.

• AI coding assistants solve hard problems in applying today’s popular programming languages to solve new programming challenges. However, we can make the problem much easier by changing the programming languages. (I am going to have a lot more to write in future posts on “the right way” to automate both software programming and digital hardware design, delivering strong correctness guarantees.)

As we go up the ladder, evolutionary psychology starts being more helpful to understand the origins of the AI challenges we’re used to. Natural language is an especially pernicious example that evolution has shaped to be hard on purpose due to its use in signaling; we don’t need to choose engineering abstractions that are hard on purpose! A theme we’ll return to in many later posts is how we can harness an outside view of our own cognition and where it comes from to spot opportunities to simplify intelligence through bigger changes to how the world works.

I’ve also spent several posts on how a holistic-design approach reveals weaknesses of deep learning, the most-popular AI technique today. Its triumphs are based on its ability to look up and combine prior art, to solve new problems in consulting vast training sets of prior solutions. However, it has major weaknesses in both of the system dimensions I emphasized above. The correctness problems are well-known, given the inscrutability of learned models and thus the risks that they will make decisions that go against our wishes. The efficiency problem is right there in the word “deep,” indicating a required structure of computation that guarantees long delays to answer prompts, compounding multiplicatively as layers of additional functionality are added (despite the intensive effort to optimize the whole stack from algorithms to hardware, which has paid off much more for throughput than latency). I’ll be proposing a new approach or two that solve both problems, using the out-of-style symbolic mode of AI (sometimes cooperating with deep learning), in one of its most-visible modern garbs as formal verification.

But wasn’t that style discredited, with deep learning knocking its socks off in so many important domains? I argue that the hardest AI problems are disproportionately like the ones I listed above, where we have paths toward avoiding them through more-holistic system design. There the principle is that we should reconfigure the world for greater legibility to intelligence technologies with good properties. Some of the pushback will come from human nature, as people across the tech industry and elsewhere are reluctant to give up on hard problems and expensive solutions that are helpful to signal competence and wealth. However, it’s worth overcoming those perverse incentives to push for lower-costs systems that deliver more-reliable answers.

Next Steps

My next arc of posts is going to cover the central ingredient of specifications for formal verification. It doesn’t help much to show that a system follows a specification that fails to cover our real objectives. I’ll review some examples from formal verification today, interleaved with scenarios that may feel more like sci-fi today but may be here before we know it.

Put differently: The first level of enlightenment is realizing the potential of formal verification to support rapid development of complex systems so that they are correct by construction. The second level of enlightenment (which luminaries of formal verification have realized and written about for decades) is noticing that systems must be proved against specifications, and the engineering of the specifications is not obviously more tractable than for the artifacts they apply to. The third level of enlightenment is realizing the suite of techniques that make dangerous specification mistakes easier to avoid than we might think, as I will explain in the coming posts.

Afterward, we can come back to considering how extracting more parallelism in computation may be one of the most important activities for the future of intelligent life in the universe, feeding a virtuous cycle of improving the formally assured intelligence that can improve itself.