The Nonlinear Library: Alignment Forum

Link to original article

Welcome to The Nonlinear Library, where we use Text-to-Speech software to convert the best writing from the Rationalist and EA communities into audio. This is: Apollo Research 1-year update, published by Marius Hobbhahn on May 29, 2024 on The AI Alignment Forum.

This is a linkpost for: www.apolloresearch.ai/blog/the-first-year-of-apollo-research

About Apollo Research

Apollo Research is an evaluation organization focusing on risks from deceptively aligned AI systems. We conduct technical research on AI model evaluations and interpretability and have a small AI governance team. As of 29 May 2024, we are one year old.

Executive Summary

For the UK AI Safety Summit, we developed a demonstration that Large Language Models (

LLMs) can strategically deceive their primary users when put under pressure. The accompanying paper was referenced by experts and the press (e.g.

AI Insight forum,

BBC,

Bloomberg) and accepted for oral presentation at the ICLR LLM agents workshop.

The evaluations team is currently working on capability evaluations for precursors of deceptive alignment, scheming model organisms, and a responsible scaling policy (RSP) on deceptive alignment. Our goal is to help governments and AI developers understand, assess, and address the risks of deceptively aligned AI systems.

The interpretability team published three papers:

An improved training method for sparse dictionary learning,

a new conceptual framework for 'loss-landscape-based interpretability', and

an associated empirical paper. We are beginning to explore concrete white-box evaluations for deception and continue to work on fundamental interpretability research.

The governance team communicates our technical work to governments (e.g., on evaluations, AI deception and interpretability), and develops recommendations around our core research areas for international organizations and individual governments.

Apollo Research works with several organizations, including partnering with the UK AISI and being a member of the US AISI Consortium. As part of our partnership with UK AISI, we were contracted to develop deception evaluations. Additionally, we engage with various AI labs, e.g. red-teaming OpenAI's fine-tuning API before deployment and consulting on the deceptive alignment section of an AI lab's RSP.

Like any organization, we have also encountered various challenges. Some projects proved overly ambitious, resulting in delays and inefficiencies. We would have benefitted from having dedicated regular exchanges with senior official external advisors earlier. Additionally, securing funding took more time and effort than expected.

We have more room for funding. Please

reach out if you're interested.

Completed work

Evaluations

For the UK AI Safety Summit, we developed a demonstration that

LLMs can strategically deceive their primary users when put under pressure, which was presented at the UK AI Safety Summit. It was referenced by experts and the press (e.g. Yoshua Bengio's

statement for Senator Schumer's AI insight forum,

BBC,

Bloomberg, US Security and Exchange Commission Chairperson Gary Gensler's

speech on AI and law, and many other media outlets). It was accepted for an oral presentation at this year's

ICLR LM agents workshop.

In our role as an independent third-party evaluator, we work with a range of organizations. For example, we were contracted by the UK AISI to build deceptive capability evaluations with them. We also worked with OpenAI to red-team their fine-tuning API before deployment.

We published multiple conceptual research pieces on evaluations, including

A Causal Framework for AI Regulation and Auditing and

A Theory of Change for AI Auditing. Furthermore, we published

conceptual clarifications on deceptive alignment and strategic deception.

We were part of multiple collaborations, including:

SAD: a situational awareness benchmark with researchers from Owain Evan's group, led by Rudolph Laine (forthcoming).

Black-Box Access is Insufficient for Rigorous...

Link to original article

Welcome to The Nonlinear Library, where we use Text-to-Speech software to convert the best writing from the Rationalist and EA communities into audio. This is: Reward hacking behavior can generalize across tasks, published by Kei Nishimura-Gasparian on May 28, 2024 on The AI Alignment Forum.

TL;DR: We find that reward hacking generalization occurs in LLMs in a number of experimental settings and can emerge from reward optimization on certain datasets. This suggests that when models exploit flaws in supervision during training, they can sometimes generalize to exploit flaws in supervision in out-of-distribution environments.

Abstract

Machine learning models can display

reward hacking behavior, where models score highly on imperfect reward signals by acting in ways not intended by their designers. Researchers have

hypothesized that sufficiently capable models trained to get high reward on a diverse set of environments could become general reward hackers. General reward hackers would use their understanding of human and automated oversight in order to get high reward in a variety of novel environments, even when this requires exploiting gaps in our evaluations and acting in ways we don't intend. It appears likely that

model supervision will be imperfect and incentivize some degree of reward hacking on the training data. Can models generalize from the reward hacking behavior they experience in training to reward hack more often out-of-distribution?

We present the first study of reward hacking generalization. In our experiments, we find that:

Using RL via expert iteration to optimize a scratchpad (hidden chain-of-thought) variant of GPT 3.5 Turbo on 'reward hackable' training datasets results in a 2.6x increase in the rate of reward hacking on held-out datasets.

Using fine-tuning or few-shot learning to get GPT 3.5 Turbo to imitate synthetic high-reward completions to hackable and unhackable prompts leads to a 1.3x to 2.0x increase in reward hacking frequency relative to our baselines on held-out datasets.

Our results suggest that reward hacking behavior could emerge and generalize out-of-distribution from LLM training if the reward signals we give them are sufficiently misspecified.

Figure 1: Example model completions from before and after expert iteration training: Training on datasets with misspecified rewards can make models significantly more likely to reward hack on held-out datasets. Note that the expert iteration training process only reinforces high-reward outputs generated by the model; it does not train on any external high-reward examples.

Introduction

One common failure mode of machine learning training is reward hacking, also known as

specification gaming, where models game the reward signals they are given in order to achieve high reward by acting in unintended ways. Examples of reward hacking seen in real models include:

A robot hand trained to grab an object tricking its human evaluator by placing its hand between the camera and the object

A simulated creature trained to maximize jumping height exploiting a bug in the physics simulator to gain significant height

A language model trained to produce high-quality summaries exploiting flaws in the summary evaluation function ROUGE to get a high score while generating barely-readable summaries

Reward hacking is possible because of

reward misspecification. For a large number of real world tasks, it is difficult to exactly specify what behavior we want to incentivize. For example, imagine trying to hand-write a reward function that specifies exactly what it means for a model to be honest. Due to the difficulty of generating perfect reward specifications, we instead optimize our models on proxy reward signals that are easier to measure but are slightly incorrect.

In the honesty example, our proxy reward might be whether a human judges a model's statements as honest. When we optimize a model against a proxy reward signal, the model sometimes learns to take advantage of t...

Link to original article

Welcome to The Nonlinear Library, where we use Text-to-Speech software to convert the best writing from the Rationalist and EA communities into audio. This is: Paper in Science: Managing extreme AI risks amid rapid progress, published by JanB on May 23, 2024 on The AI Alignment Forum.

https://www.science.org/doi/10.1126/science.adn0117

Authors:

Yoshua Bengio, Geoffrey Hinton, Andrew Yao, Dawn Song, Pieter Abbeel, Yuval Noah Harari, Ya-Qin Zhang, Lan Xue, Shai Shalev-Shwartz, Gillian Hadfield, Jeff Clune, Tegan Maharaj, Frank Hutter, Atılım Güneş Baydin, Sheila McIlraith, Qiqi Gao, Ashwin Acharya, David Krueger, Anca Dragan, Philip Torr, Stuart Russell, Daniel Kahneman, Jan Brauner*, Sören Mindermann*

Abstract:

Artificial intelligence (AI) is progressing rapidly, and companies are shifting their focus to developing generalist AI systems that can autonomously act and pursue goals. Increases in capabilities and autonomy may soon massively amplify AI's impact, with risks that include large-scale social harms, malicious uses, and an irreversible loss of human control over autonomous AI systems. Although researchers have warned of extreme risks from AI, there is a lack of consensus about how to manage them.

Society's response, despite promising first steps, is incommensurate with the possibility of rapid, transformative progress that is expected by many experts. AI safety research is lagging. Present governance initiatives lack the mechanisms and institutions to prevent misuse and recklessness and barely address autonomous systems.

Drawing on lessons learned from other safety-critical technologies, we outline a comprehensive plan that combines technical research and development with proactive, adaptive governance mechanisms for a more commensurate preparation.

Thanks for listening. To help us out with The Nonlinear Library or to learn more, please visit nonlinear.org.

Link to original article

Welcome to The Nonlinear Library, where we use Text-to-Speech software to convert the best writing from the Rationalist and EA communities into audio. This is: Announcing Human-aligned AI Summer School, published by Jan Kulveit on May 22, 2024 on The AI Alignment Forum.

The fourth Human-aligned AI Summer School will be held in Prague from 17th to 20th July 2024. We will meet for four intensive days of talks, workshops, and discussions covering latest trends in AI alignment research and broader framings of AI alignment research.

Apply now

, applications are evaluated on a rolling basis.

The intended audience of the school are people interested in learning more about the AI alignment topics, PhD students, researchers working in ML/AI outside academia, and talented students.

Format of the school

The school is focused on teaching and exploring approaches and frameworks, less on presentation of the latest research results. The content of the school is mostly technical - it is assumed the attendees understand current ML approaches and some of the underlying theoretical frameworks.

This year, the school will cover these main topics:

Overview of the alignment problem and current approaches.

Alignment of large language models: RLHF, DPO and beyond. Methods used to align current large language models and their shortcomings.

Evaluating and measuring AI systems: How to understand and oversee current AI systems on the behavioral level.

Interpretability and the science of deep learning: What's going on inside of the models?

AI alignment theory: While 'prosaic' approaches to alignment focus on current systems, theory aims for deeper understanding and better generalizability.

Alignment in the context of complex systems and multi-agent settings: What should the AI be aligned to? In most realistic settings, we can expect there are multiple stakeholders and many interacting AI systems; any solutions to alignment problem need to solve multi-agent settings.

The school consists of lectures and topical series, focused smaller-group workshops and discussions, expert panels, and opportunities for networking, project brainstorming and informal discussions.

Detailed program of the school will be announced shortly before the event. See below for a program outline and e.g.

the program of the previous school for an illustration of the program content and structure.

Confirmed speakers

Stephen Casper - Algorithmic Alignment Group, MIT.

Stanislav Fort - Google DeepMind.

Jesse Hoogland - Timaeus.

Jan Kulveit - Alignment of Complex Systems, Charles University.

Mary Phuong - Google DeepMind.

Deger Turan - AI Objectives Institute and Metaculus.

Vikrant Varma - Google DeepMind.

Neel Nanda - Google DeepMind.

(more to be announced later)

Thanks for listening. To help us out with The Nonlinear Library or to learn more, please visit nonlinear.org.

Link to original article

Welcome to The Nonlinear Library, where we use Text-to-Speech software to convert the best writing from the Rationalist and EA communities into audio. This is: EIS XIII: Reflections on Anthropic's SAE Research Circa May 2024, published by Stephen Casper on May 21, 2024 on The AI Alignment Forum.

Part 13 of 12 in the

Engineer's Interpretability Sequence.

TL;DR

On May 5, 2024,

I made a set of 10 predictions about what the next sparse autoencoder (SAE) paper from Anthropic would and wouldn't do.

Today's new SAE paper from Anthropic was full of brilliant experiments and interesting insights, but it ultimately underperformed my expectations. I am beginning to be concerned that Anthropic's recent approach to interpretability research might be better explained by safety washing than practical safety work.

Think of this post as a curt editorial instead of a technical piece. I hope to revisit my predictions and this post in light of future updates.

Reflecting on predictions

Please

see my original post for 10 specific predictions about what

today's paper would and wouldn't accomplish. I think that Anthropic obviously did 1 and 2 and obviously did not do 4, 5, 7, 8, 9, and 10. Meanwhile, I think that their experiments to identify

specific and

safety-relevant features should count for 3 (proofs of concept for a useful type of task) but definitely do not count for 6 (*competitively* finding and removing a harmful behavior that was represented in the training data).

Thus, my assessment is that Anthropic did 1-3 but not 4-10.

I have been wrong with mech interp predictions in the past, but this time, I think I was 10 for 10: everything I predicted with >50% probability happened, and everything I predicted with <50% probability did not happen.

Overall, the paper underperformed my expectations. If you scored the paper relative to my predictions by giving it (1-p) points when it did something that I predicted it would do with probability p and -p points when it did not, the paper would score -0.74.

A review + thoughts

I think that Anthropic's new SAE work has continued to be like lots of prior high-profile work on mechanistic interpretability - it has focused on presenting illustrative examples, streetlight demos, and cherry-picked proofs of concept. This is useful for science, but it does not yet show that SAEs are helpful and competitive for diagnostic and debugging tasks that could improve AI safety.

I feel increasingly concerned about how Anthropic motivates and sells its interpretability research in the name of safety. Today's paper makes some major Motte and Bailey claims that oversell what was accomplished like "

Eight months ago, we demonstrated that sparse autoencoders could recover monosemantic features from a small one-layer transformer," "

Sparse autoencoders produce interpretable features for large models," and "

The resulting features are highly abstract: multilingual, multimodal, and generalizing between concrete and abstract references." The paper also made some omissions of past literature on interpretability illusions (e.g., Bolukbasi et al., 2021), which their methodology seems prone to. Normally, problems like this are mitigated by peer review, which Anthropic does not participate in.

Meanwhile, whenever Anthropic puts out new interpretability research, I see a laundry list of posts from the company and employees to promote it. They always seem to claim the same thing - that some 'groundbreaking new progress has been made' and that 'the model was even more interpretable than they thought' but that 'there remains progress to be made before interpretability is solved'. I won't link to any specific person's posts, but here is Anthropic's post from

today and

October 2023.

The way that Anthropic presents its interpretability work has real-world consequences. For example, it seems to have led to

viral claims that interpretability will be solved and that we are bound for safe models. It has also led to at least one claim in a pol...

Link to original article

Welcome to The Nonlinear Library, where we use Text-to-Speech software to convert the best writing from the Rationalist and EA communities into audio. This is: The Problem With the Word 'Alignment', published by peligrietzer on May 21, 2024 on The AI Alignment Forum.

This post was written by Peli Grietzer, inspired by internal writings by TJ (tushant jha), for AOI[1]. The original post, published on Feb 5, 2024, can be found here: https://ai.objectives.institute/blog/the-problem-with-alignment.

The purpose of our work at the AI Objectives Institute (AOI) is to direct the impact of AI towards human autonomy and human flourishing.

In the course of articulating our mission and positioning ourselves -- a young organization -- in the landscape of AI risk orgs, we've come to notice what we think are serious conceptual problems with the prevalent vocabulary of 'AI alignment.' This essay will discuss some of the major ways in which we think the concept of 'alignment' creates bias and confusion, as well as our own search for clarifying concepts.

At AOI, we try to think about AI within the context of humanity's contemporary institutional structures: How do contemporary market and non-market (eg. bureaucratic, political, ideological, reputational) forces shape AI R&D and deployment, and how will the rise of AI-empowered corporate, state, and NGO actors reshape those forces? We increasingly feel that 'alignment' talk tends to obscure or distort these questions.

The trouble, we believe, is the idea that there is a single so-called Alignment Problem. Talk about an 'Alignment Problem' tends to conflate a family of related but distinct technical and social problems, including:

P1: Avoiding takeover from emergent optimization in AI agents

P2: Ensuring that AI's information processing (and/or reasoning) is intelligible to us

P3: Ensuring AIs are good at solving problems as specified (by user or designer)

P4: Ensuring AI systems enhance, and don't erode, human agency

P5: Ensuring that advanced AI agents learn a human utility function

P6: Ensuring that AI systems lead to desirable systemic and long term outcomes

Each of P1-P6 is known as 'the Alignment Problem' (or as the core research problem in 'Alignment Research') to at least some people in the greater AI Risk sphere, in at least some contexts. And yet these problems are clearly not simply interchangeable: placing any one of P1-P6 at the center of AI safety implies a complicated background theory about their relationship, their relative difficulty, and their relative significance.

We believe that when different individuals and organizations speak of the 'Alignment Problem,' they assume different controversial reductions of the P1-P6 problems network to one of its elements. Furthermore, the very idea of an 'Alignment Problem' precommits us to finding a reduction for P1-P6, obscuring the possibility that this network of problems calls for a multi-pronged treatment.

One surface-level consequence of the semantic compression around 'alignment' is widespread miscommunication, as well as fights over linguistic real-estate. The deeper problem, though, is that this compression serves to obscure some of a researcher's or org's foundational ideas about AI by 'burying' them under the concept of alignment.

Take a familiar example of a culture clash within the greater AI Risk sphere: many mainstream AI researchers identify 'alignment work' with incremental progress on P3 (task-reliability), which researchers in the core AI Risk community reject as just safety-washed capabilities research. We believe working through this culture-clash requires that both parties state their theories about the relationship between progress on P3 and progress on P1 (takeover avoidance).

In our own work at AOI, we've had occasion to closely examine a viewpoint we call the Berkeley Model of Alignment -- a popular reduction of P1-P6 to P5 (agent value-learning) based on a paradigm consolidated at UC Berkeley's CHAI research gr...

Link to original article

Welcome to The Nonlinear Library, where we use Text-to-Speech software to convert the best writing from the Rationalist and EA communities into audio. This is: The Local Interaction Basis: Identifying Computationally-Relevant and Sparsely Interacting Features in Neural Networks, published by Marius Hobbhahn on May 20, 2024 on The AI Alignment Forum.

This is a linkpost for our two recent papers, produced at Apollo Research in collaboration with Kaarel Hanni (Cadenza Labs), Avery Griffin, Joern Stoehler, Magdalena Wache and Cindy Wu:

1. An exploration of using degeneracy in the loss landscape for interpretability https://arxiv.org/abs/2405.10927

2. An empirical test of an interpretability technique based on the loss landscape https://arxiv.org/abs/2405.10928

Not to be confused with Apollo's recent Sparse Dictionary Learning paper.

A key obstacle to mechanistic interpretability is finding the right representation of neural network internals. Optimally, we would like to derive our features from some high-level principle that holds across different architectures and use cases. At a minimum, we know two things:

1. We know that the training loss goes down during training. Thus, the features learned during training must be determined by the loss landscape. We want to use the structure of the loss landscape to identify what the features are and how they are represented.

2. We know that models generalize, i.e. that they learn features from the training data that allow them to accurately predict on the test set. Thus, we want our interpretation to explain this generalization behavior.

Generalization has been linked to basin broadness in the loss landscape in several ways, most notably including singular learning theory, which introduces the learning coefficient as a measure of basin broadness that doubles as a measure of generalization error that replaces the parameter count in Occam's razor.

Inspired by both of these ideas, the first paper explores using the structure of the loss landscape to find the most computationally natural representation of a network. We focus on identifying parts of the network that are not responsible for low loss (i.e. degeneracy), inspired by singular learning theory.

These degeneracies are an obstacle for interpretability as they mean there exist parameters which do not affect the input-output behavior in the network (similar to the parameters of a Transformer WV and WO matrices that do not affect the product WOV).

We explore 3 different ways neural network parameterisations can be degenerate:

1. when activations are linearly dependent

2. when gradient vectors are linearly dependent

3. when ReLU neurons fire on the same inputs.

This investigation leads to the interaction basis, and eventually the local interaction basis (LIB) that we test in the second paper. This basis removes computationally irrelevant features and interactions, and sparsifies the remaining interactions between layers.

Finally, we analyse how modularity is connected to degeneracy in the loss landscape. We suggest a preliminary metric for finding the sorts of modules that the neural network prior is biased towards.

The second paper tests how useful the LIB is in toy and language models. In this new basis we calculate integrated gradient based interactions between features, and analyse the graph of all features in a network. We interpret strongly-interacting features, and identify modules in this graph using the modularity metric of the first paper.

To derive the LIB basis we coordinate-transform the activations of neural networks in two steps: Step 1 is a transformation into the PCA basis, removing activation space directions which don't explain any variance. Step 2 is a transformation of the activations to align the basis with the right singular vectors of the gradient vector dataset.

The 2nd step is the key new ingredient which aims to make interactions between adjacent layers sparse, and removes directions which do not affect downstre...

Link to original article

Welcome to The Nonlinear Library, where we use Text-to-Speech software to convert the best writing from the Rationalist and EA communities into audio. This is: Infra-Bayesian haggling, published by hannagabor on May 20, 2024 on The AI Alignment Forum.

Preface

I wrote this post during my scholarship at MATS. My goal is to describe a research direction of the learning theoretic agenda (LTA). Namely, a natural infra-Bayesian learning algorithm proposal that arguably leads to Pareto-optimal solutions in repeated games. The idea originates from Vanessa, I'm expanding a draft of her into a more accessible description.

The expected audience are people who are interested in ongoing work on LTA. It is especially suitable for people who are looking for a research direction to pursue in this area.

Introduction

There has been much work on the theory of agents who cooperate in the Prisoner's dilemma and other situations. Some call this behavior

superrationality

. For example, functional decision theory (FDT) is a decision theory that prescribes such behavior. The strongest results so far are those coming from "modal combat", e.g. Critch. However, these results are of very limited scope: among other issues, they describe agents crafted for specific games, rather than general reasoners that produce superrational behavior in a "naturalized" manner (i.e. as a special case of the general rules of reasoning.)

At the same time, understanding multi-agent learning theory is another major open problem. Attempts to prove convergence to game-theoretic solution concepts (a much weaker goal than superrationality) in a learning-theoretic setting are impeded by the so-called grain-of-truth problem (originally observed by Kalai and Lehrer, its importance was emphasized by Hutter).

An agent can learn to predict the environment via Bayesian learning only if it assigns non-zero prior probability to that environment, i.e. its prior contains a grain of truth. What's the grain-of-truth problem? Suppose Alice's environment contains another agent, Bob. If Alice is a Bayesian agent, she can learn to predict Bob's behavior only if her prior assigns a positive probability to Bob's behavior.

(That is, Alice's prior contains a grain of truth.) If Bob has the same complexity level as Alice, then Alice is not able to represent all possible environments. Thus, in general, Alice's prior doesn't contain a grain of truth. A potential solution based on "reflective oracles" was proposed by Leike, Taylor and Fallenstein. However it involves arbitrarily choosing a fixed point out of an enormous space of possibilities, and requires that all agents involved choose the same fixed point.

Approaches to multi-agent learning in the mainstream literature (see e.g. Cesa-Bianchi and Lugosi) also suffer from restrictive assumptions and are not naturalized.

Infra-Bayesianism (IB) was originally motivated by the problem of non-realizability, of which the multi-agent grain-of-truth problem is a special case. Moreover, it converges to FDT-optimal behavior in most Newcombian problems. Therefore, it seems natural to expect IB agents to have strong multi-agent guarantees as well, hopefully even superrationality.

In this article, we will argue that an infra-Bayesian agent playing a repeated game displays a behavior dubbed "infra-Bayesian haggling". For two-player games, this typically (but, strictly speaking, not always) leads to Pareto-efficient outcome. The latter can be a viewed as a form of superrationality. Currently, we only have an informal sketch, and even that in a toy model with no stochastic hypotheses. However, it seems plausible that it can be extended to a fairly general setting.

Certainly it allows for asymmetric agents with different priors and doesn't have any strong mutual compatibility condition. The biggest impediment to naturality is the requirement that the learning algorithm is of a particular type (namely, Upper Confidence Bound). However, we believe that it should be po...

Link to original article

Welcome to The Nonlinear Library, where we use Text-to-Speech software to convert the best writing from the Rationalist and EA communities into audio. This is: The consistent guessing problem is easier than the halting problem, published by Jessica Taylor on May 20, 2024 on The AI Alignment Forum.

The halting problem is the problem of taking as input a Turing machine M, returning true if it halts, false if it doesn't halt. This is known to be uncomputable. The consistent guessing problem (named by Scott Aaronson) is the problem of taking as input a Turing machine M (which either returns a Boolean or never halts), and returning true or false; if M ever returns true, the oracle's answer must be true, and likewise for false. This is also known to be uncomputable.

Scott Aaronson inquires as to whether the consistent guessing problem is strictly easier than the halting problem. This would mean there is no Turing machine that, when given access to a consistent guessing oracle, solves the halting problem, no matter which consistent guessing oracle (of which there are many) it has access too. As prior work, Andrew Drucker has written a paper describing a proof of this, although I find the proof hard to understand and have not checked it independently.

In this post, I will prove this fact in a way that I at least find easier to understand. (Note that the other direction, that a Turing machine with access to a halting oracle can be a consistent guessing oracle, is trivial.)

First I will show that a Turing machine with access to a halting oracle cannot in general determine whether another machine with access to a halting oracle will halt. Suppose M(O, N) is a Turing machine that returns true if N(O) halts, false otherwise, when O is a halting oracle. Let T(O) be a machine that runs M(O, T), halting if it returns false, running forever if it returns true. Now M(O, T) must be its own negation, a contradiction.

In particular, this implies that the problem of deciding whether a Turing machine with access to a halting oracle halts cannot be a Σ01 statement in the arithmetic hierarchy, since these statements can be decided by a machine with access to a halting oracle.

Now consider the problem of deciding whether a Turing machine with access to a consistent guessing oracle halts for all possible consistent guessing oracles. If this is a Σ01 statement, then consistent guessing oracles must be strictly weaker than halting oracles.

Since, if there were a reliable way to derive a halting oracle from a consistent guessing oracle, then any machine with access to a halting oracle can be translated to one making use of a consistent guessing oracle, that halts for all consistent guessing oracles if and only if the original halts when given access to a halting oracle. That would make the problem of deciding whether a Turing machine with access to a halting oracle halts a Σ01 statement, which we have shown to be impossible.

What remains to be shown is that the problem of deciding whether a Turing machine with access to a consistent guessing oracle halts for all consistent guessing oracles, is a Σ01 statement.

To do this, I will construct a recursively enumerable propositional theory T that depends on the Turing machine. Let M be a Turing machine that takes an oracle as input (where an oracle maps encodings of Turing machines to Booleans). Add to the T the following propositional variables:

ON for each Turing machine encoding N, representing the oracle's answer about this machine.

H, representing that M(O) halts.

Rs for each possible state s of the Turing machine, where the state includes the head state and the state of the tape, representing that s is reached by the machine's execution.

Clearly, these variables are recursively enumerable and can be computably mapped to the natural numbers.

We introduce the following axiom schemas:

(a) For any machine N that halts and returns true, ON.

(b) For any machine N that halts and returns false, ON.

(c) For any ...

Link to original article

Welcome to The Nonlinear Library, where we use Text-to-Speech software to convert the best writing from the Rationalist and EA communities into audio. This is: Towards Guaranteed Safe AI: A Framework for Ensuring Robust and Reliable AI Systems, published by Joar Skalse on May 17, 2024 on The AI Alignment Forum.

I want to draw attention to a new paper, written by myself, David "davidad" Dalrymple, Yoshua Bengio, Stuart Russell, Max Tegmark, Sanjit Seshia, Steve Omohundro, Christian Szegedy, Ben Goldhaber, Nora Ammann, Alessandro Abate, Joe Halpern, Clark Barrett, Ding Zhao, Tan Zhi-Xuan, Jeannette Wing, and Joshua Tenenbaum.

In this paper we introduce the concept of "guaranteed safe (GS) AI", which is a broad research strategy for obtaining safe AI systems with provable quantitative safety guarantees. Moreover, with a sufficient push, this strategy could plausibly be implemented on a moderately short time scale. The key components of GS AI are:

1. A formal safety specification that mathematically describes what effects or behaviors are considered safe or acceptable.

2. A world model that provides a mathematical description of the environment of the AI system.

3. A verifier that provides a formal proof (or some other comparable auditable assurance) that the AI system satisfies the safety specification with respect to the world model.

The first thing to note is that a safety specification in general is not the same thing as a reward function, utility function, or loss function (though they include these objects as special cases). For example, it may specify that the AI system should not communicate outside of certain channels, copy itself to external computers, modify its own source code, or obtain information about certain classes of things in the external world, etc.

The safety specifications may be specified manually, generated by a learning algorithm, written by an AI system, or obtained through other means. Further detail is provided in the main paper.

The next thing to note is that most useful safety specifications must be given relative to a world model. Without a world model, we can only use specifications defined directly over input-output relations. However, we want to define specifications over input-outcome relations instead. This is why a world model is a core component of GS AI. Also note that:

1. The world model need not be a "complete" model of the world. Rather, the required amount of detail and the appropriate level of abstraction depends on both the safety specification(s) and the AI system's context of use.

2. The world model should of course account for uncertainty, which may include both stochasticity and nondeterminism.

3. The AI system whose safety is being verified may or may not use a world model, and if it does, we may or may not be able to extract it. However, the world model that is used for the verification of the safety properties need not be the same as the world model of the AI system whose safety is being verified (if it has one).

The world model would likely have to be AI-generated, and should ideally be interpretable. In the main paper, we outline a few potential strategies for producing such a world model.

Finally, the verifier produces a quantitative assurance that the base-level AI controller satisfies the safety specification(s) relative to the world model(s). In the most straightforward form, this could simply take the shape of a formal proof. However, if a direct formal proof cannot be obtained, then there are weaker alternatives that would still produce a quantitative guarantee.

For example, the assurance may take the form of a proof that bounds the probability of failing to satisfy the safety specification, or a proof that the AI system will converge towards satisfying the safety specification (with increasing amounts of data or computational resources, for example). Such proofs are of course often very hard to obtain. However, further progress in automated theorem proving (and relat...