RAISE AI Safety prerequisites map entirely in one post

post by RAISE · 2019-07-17T08:57:18.226Z · score: 15 (7 votes) · LW · GW · 5 comments

Contents

  How to use this
  Credits
  Main path
    Level 1. Basic logic
    Level 2. Basic set theory
    Level 3. Set Theoretic Relations and Enumerability
    Level 4. Formal Semantics
    Level 5. Formal Proof
    Level 6. Turing Machines and the Halting Problem
    Level 7. Equivalence Relations and Orderings
    Level 8. Abacus Computability and Mathematical Proof by Induction
    Level 9. The Natural Numbers in Set Theory and More Induction
    Level 10. Recursive Functions
    Level 11. Set Theoretic Recursion
    Level 12. The Equivalence of Different Notions of Computability
    Level 13. Isomorphisms
    Level 14. Logic Review and The Relationship Between Computation and Logic
    Level 15. Finite and Countable Sets
    Level 16 (elective). Linear Orders and Completing the Real Numbers
    Level 17. Basic Model Theory
    Level 18 (elective). A quick look at cardinal and ordinal numbers
    Level 19. Arithmetization and Representation of Recursive Functions
    Level 20. Godel’s Incompleteness Theorems and Axiomatic ZFC
  Logic and proof path
    Level 1. Basic logic
    Level 2. Quantified logic. Introduction to mathematical arguments
    Level 3. Formal semantics basics
    Level 4. Formal proofs
    Level 5. Proof by induction
  Set theory path
    Level 1. Basic set theory
    Level 2. Set theoretic relations
    Level 3. Equivalence relations and orderings
    Level 4. Natural numbers and induction
    Level 5. Set theoretic recursion
    Level 6. Operations, structures, isomorphism
    Level 7. Cardinality. Finite and countable sets
    Elective: Level 8. Linear orderings. Completeness. Uncountable sets
    Elective: Level 9. Cardinal numbers
    Elective: Level 10. Ordinal numbers. Axiom of replacement. Transfinite induction and recursion
    Elective: Level 11. Axiom of choice
    Level 12. ZF(C) set theory
  Computability theory path
    Level 1. Enumerability and diagonalization
    Level 2. Turing machines and the halting problem
    Level 3. Abacus computability
    Level 4. Recursive functions
    Level 5. The equivalence of different notions of computability
    Level 6. First order logic
    Level 7. Undecidability of first order logic
    Level 8. Models, their existence. Proofs and completeness.
    Level 9. Arithmetization. Representability of recursive functions
    Level 10. Indefinability, undecidability, incompleteness. The unprovability of consistency.
None
5 comments

After reflecting on recent criticism [LW · GW], all RAISE projects have been discontinued, and a postmortem is in our plans. One of those projects was the AI Safety prerequisites online course originally announced here [LW · GW]. We're sharing the curriculum here in almost plaintext format so that people can easily find and access it. There is also a GDoc here. (Note: two other products of RAISE are series of lessons on IRL and IDA. They don't have such neatly formed curriculums, and they are still accessible as online lessons.)

It was supposed to be a guide for helping people who want to get into AI safety research. It contains only foundations of math topics (Logic and proof, ZF(C) Set theory, Computability theory to be precise), which are more useful for agent foundations stuff and not useful for machine learning stuff. It was planned to be extended to cover more topics, but that never happened.

How to use this

The main path contains 20 levels. It is the recommended path through the curriculum. Its levels are actually short sequences of levels from the three other paths.

To see what textbooks are required to study a path, see its beginning. Computability theory and set theory paths require two paid textbooks.

13 out of 20 levels of the main path are covered by our online course, which is free (but still requires paid textbooks). To use the online course, register here. You might prefer to use it instead of the text below because it provides more sense of progress, contains solutions to the exercises, has some writing mistakes fixed, maybe feels like a less tedious thing, and provides some additional exercises which we don't think are important.

Credits

The curriculum was made by Erik Istre [LW · GW] and Trent Fowler [LW · GW]. People who created the online course are: Philip Blagoveschensky [LW · GW], Davide Zagami, Toon Alfrink [LW · GW], Hoagy Cunningham, Danilo Naiff, Lewis Hammond. Also these people contributed: Jacob Spence, Roland Pihlakas. Also, thanks to Grasple for providing their services for free.

Main path

Level 1. Basic logic

The big ideas:

  1. Sentential Logic
  2. Truth Tables
  3. Predicate Logic
  4. Methods of Mathematical Proof

To move to the next level you need to be able to:

  1. Translate informal arguments into formal logic.
  2. Evaluate an argument as either valid or invalid.
  3. Explain how to prove an implication/conditional, a conjunction, a disjunction, and a negation and know what this looks like informally (i.e. in words and not symbols).

Why this is important:

Skill Guides for this Level:

Level 2. Basic set theory

The big ideas:

  1. Axioms of Set Theory
  2. Set Operations

To move to the next level you need to be able to:

  1. Explain what a set is.
  2. Calculate the intersection, union and difference of sets.
  3. Prove two sets are equal.
  4. Apply basic axioms of Zermelo-Fraenkel set theory.

Why this is important:

Skill Guides for this level:

Level 3. Set Theoretic Relations and Enumerability

The big ideas:

  1. Ordered Pairs
  2. Relations
  3. Functions
  4. Enumerability
  5. Diagonalization

To move to the next level you need to be able to:

  1. Define functions in terms of relations, relations in terms of ordered pairs, and ordered pairs in terms of sets.
  2. Define what a one-to-one (or injective) and onto (or surjective) function is. A function that is both is called a one-to-one correspondence (or bijective).
  3. Prove a function is one-to-one and/or onto.
  4. Explain the difference between an enumerable and a non-enumerable set.

Why this is important:

Skill Guides for this level:

Level 4. Formal Semantics

The big ideas:

  1. Formal Semantics
  2. Model

To move to the next level you need to be able to:

  1. Evaluate the truth value of logical sentences in a given model.
  2. Build models for a set of logical sentences and then use those models to deduce information about the sentences.

Why this is important:

Skill guides for this level:

Level 5. Formal Proof

The big ideas:

  1. Natural Deduction Proof System

To move to the next level you need to be able to:

  1. Explain the difference between a formal system of proof and our informal notion of proof.
  2. Derive proofs of logical formula in the system of natural deduction.

Why this is important:

Skill guides for this level:

Milestone - You’re now a !

Take a moment to reflect on what you’ve learned so far. Remind yourself of the important concepts that you’ve come across, and mark down any concepts which are still giving you trouble. Determine whether you need to seek out further resources to clear up any confusions.

Level 6. Turing Machines and the Halting Problem

The big ideas:

  1. Turing Machine
  2. The Halting Problem

To move to the next level you need to be able to:

  1. Describe a turing machine and write basic turing algorithms.
  2. Give the basic idea of the halting problem.
  3. Give the basic idea of the proof that the halting function isn’t computable.

Why this is important:

Skill guides for this level:

Level 7. Equivalence Relations and Orderings

The big ideas:

  1. Equivalence Relations
  2. Partitions
  3. Orderings

To move to the next level you need to be able to:

  1. Explain the relationship between equivalence relations and partitions.
  2. Name two different kinds of orderings and the conditions on the ordering relations required for these kinds.

Why this is important:

Skill guides for this level:

Level 8. Abacus Computability and Mathematical Proof by Induction

The big ideas:

  1. Proof by Induction
  2. Abacus Computability

To move to the next level you need to be able to:

  1. Explain mathematical proof by induction.
  2. Explain the abacus machine and the differences between a turing machine and an abacus machine.
  3. Build basic algorithms for an abacus machine.

Why this is important:

Skill guides for this level:

Level 9. The Natural Numbers in Set Theory and More Induction

The big ideas:

  1. Representing Natural Numbers with Sets

To move to the next level you need to be able to:

  1. Explain the relationship between inductive sets and the set theoretic construction of the natural numbers.
  2. Use the method of mathematical induction to prove claims about the natural numbers.

Why this is important:

Skill guides for this level:

Level 10. Recursive Functions

The big ideas:

  1. Primitive Recursive Functions
  2. Recursive Functions
  3. Primitive Recursive Sets
  4. Recursive Sets

To move to the next level you need to be able to:

  1. Translate the formal syntax of the recursive functions into an informal representation of a function and vice versa.
  2. Explain the difference between primitive recursion and recursion.
  3. Explain the difference between semi-recursive and recursive.

Why this is important:

Skill guides for this level:

Level 11. Set Theoretic Recursion

The big ideas:

  1. The Recursion Theorem
  2. Peano Axioms

To move to the next level you need to be able to:

  1. State the recursion theorem and explain how this theorem coincides with our informal notion of recursion.
  2. Use the recursion theorem to create new functions.
  3. Explain what the axioms of Peano arithmetic are.

Why this is important:

Skill guides for this level:

Level 12. The Equivalence of Different Notions of Computability

The big ideas:

  1. Equivalence of Turing Machines and Recursive Computability

To move to the next level you need to be able to:

  1. Describe the general process of coding turing machines.
  2. Explain what a universal turing machine is.

Why this is important:

Skill guides for this level:

Milestone - You’re now a !

As last time, take a moment to reflect on what you’ve learned so far. Remind yourself of the important concepts that you’ve come across, and mark down any concepts which are still giving you trouble. Determine whether you need to seek out further resources to clear up any confusions.

Level 13. Isomorphisms

The big ideas:

  1. Isomorphism

To move to the next level you need to be able to:

  1. Define isomorphism between structures.
  2. Prove that two structures are isomorphic.

Why this is important:

Skill guides for this level:

Level 14. Logic Review and The Relationship Between Computation and Logic

The big ideas:

  1. First Order Logic Syntax
  2. First Order Logic Semantics
  3. The Relationship Between Logic and Computability

To move to the next level you need to be able to:

  1. Read and translate the syntax for formal logic, and translate informal sentences to logic.
  2. Build models to evaluate logical claims.
  3. Explain how logic and turing machines/primitive recursion are related and how this leads to showing the undecidability of first-order logic.

Why this is important:

Skill guides for this level:

Level 15. Finite and Countable Sets

The big ideas:

  1. Finite Set
  2. Countable Set

To move to the next level you need to be able to:

  1. State the Cantor-Bernstein Theorem.
  2. Understand basic properties of finite and countable sets.
  3. Define what a countable set is.
  4. Prove that a set is of countable size.

Why this is important:

Skill guides for this level:

Level 16 (elective). Linear Orders and Completing the Real Numbers

The big ideas:

  1. Constructing the Real Numbers

To move to the next level you need to be able to:

  1. Define when two linear orders are similar.
  2. Explain how the concept of completeness motivates the real numbers.
  3. Explain how Dedekind cuts generate completeness for the rational numbers.

Why this is important:

Skill guides for this level:

Level 17. Basic Model Theory

The big ideas:

  1. Models
  2. Soundness
  3. Completeness
  4. Sequent Calculus

To move to the next level you need to be able to:

  1. Define a model.
  2. Explain the Lowenheim-Skolem theorem and the compactness theorem.
  3. Use a Gentzen style system or sequent calculus to derive proofs.
  4. Explain the concepts of soundness and completeness.

Why this is important:

Skill guides for this level:

Milestone - You’re now a !

As last time, take a moment to reflect on what you’ve learned so far. Remind yourself of the important concepts that you’ve come across, and mark down any concepts which are still giving you trouble. Determine whether you need to seek out further resources to clear up any confusions.

Level 18 (elective). A quick look at cardinal and ordinal numbers

To move to the next level you need to be able to:

  1. Explain what a cardinal number is.
  2. Demonstrate the general idea behind the proof of Cantor’s Theorem.
  3. Explain what an ordinal number is.
  4. Use the generalized notions of transfinite induction and transfinite recursion to prove statements about large sets.

Why this is important:

Skill guides for this level:

Level 19. Arithmetization and Representation of Recursive Functions

The big ideas:

  1. The Axiom of Choice
  2. Arithmetization of Syntax
  3. Mathematical Induction
  4. Representability of Functions

To move to the next level you need to be able to:

  1. Elective: State the axiom of choice and at least loosely explain it to someone with basic set theory.
  2. Describe the process of generating Godel numbers for logical statements.
  3. Define what it means for a recursive function to be representable in a system of arithmetic.

Why this is important:

Skill guides for this level:

Level 20. Godel’s Incompleteness Theorems and Axiomatic ZFC

The big ideas:

  1. Godel’s Incompleteness Theorems
  2. Independence Result
  3. Zermelo-Fraenkel Set Theory

To move to the next level you need to be able to:

  1. Explain the diagonal lemma and why it leads to the limitative results of formal systems. Further, explain under what precise conditions we must be for these results to accurately apply.
  2. Explain Godel’s first and second incompleteness theorems and the general procedure of their proofs.
  3. Define what an independence result is and a particular example of such a result for ZFC.
  4. Explain why Godel’s Incompleteness theorems also apply to a formal set theory like ZFC.

Why this is important:

Skill guides for this level:

Milestone - You’re now a !

As last time, take a moment to reflect on what you’ve learned so far. Remind yourself of the important concepts that you’ve come across, and mark down any concepts which are still giving you trouble. Determine whether you need to seek out further resources to clear up any confusions.

Logic and proof path

The main textbook used in this path is a free textbook "Forall x" version 1.4. download v1.4 another link for v1.4 latext version Note that numbering of exercises sometimes changes between versions.

Another resource used in this path is Introduction to Mathematical Arguments by Michael Hutchings.

Level 1. Basic logic

Level 2. Quantified logic. Introduction to mathematical arguments

This level on Grasple

Level 3. Formal semantics basics

This level on Grasple

Level 4. Formal proofs

This level on Grasple

Level 5. Proof by induction

This level on Grasple

Set theory path

This path uses the Introduction to set theory. Third edition. Revised and expanded by Hrbacek, Jech.

Level 1. Basic set theory

This level on Grasple

Level 2. Set theoretic relations

This level on Grasple

This level uses Introduction to Set Theory by Hrbacek and Jech.

Level 3. Equivalence relations and orderings

This level on Grasple

Resources: Introduction to Set Theory by Hrbacek and Jech

Level 4. Natural numbers and induction

This level on grasple

Resources: Introduction to Set Theory by Hrbacek and Jech

Level 5. Set theoretic recursion

This level at grasple

Resources: Introduction to Set Theory by Hrbacek and Jech

Level 6. Operations, structures, isomorphism

This level on Grasple

Resources: Introduction to Set Theory by Hrbacek and Jech

Level 7. Cardinality. Finite and countable sets

Resources: Introduction to Set Theory by Hrbacek and Jech

Elective: Level 8. Linear orderings. Completeness. Uncountable sets

Resources: Introduction to Set Theory by Hrbacek and Jech

Elective: Level 9. Cardinal numbers

Resources: Introduction to Set Theory by Hrbacek and Jech

Elective: Level 10. Ordinal numbers. Axiom of replacement. Transfinite induction and recursion

Resources: Introduction to Set Theory by Hrbacek and Jech

Elective: Level 11. Axiom of choice

Resources: Introduction to Set Theory by Hrbacek and Jech

Level 12. ZF(C) set theory

Resources: Introduction to Set Theory by Hrbacek and Jech

Computability theory path

This path uses Computability and Logic (Fifth Edition) by Boolos, Burgess and Jeffrey. An instructor's manual is available, it has hints for many problems.

Level 1. Enumerability and diagonalization

This level on grasple

Resources: Computability and Logic Fifth Edition by Boolos, Burgess, Jeffrey

Level 2. Turing machines and the halting problem

This level on grasple

Resources: Computability and Logic Fifth Edition by Boolos, Burgess, Jeffrey

Level 3. Abacus computability

This level on grasple

Resources: Computability and Logic Fifth Edition by Boolos, Burgess, Jeffrey

Level 4. Recursive functions

This level on grasple

Resources: Computability and Logic Fifth Edition by Boolos, Burgess, Jeffrey

Level 5. The equivalence of different notions of computability

This level on grasple

Resources: Computability and Logic Fifth Edition by Boolos, Burgess, Jeffrey

Level 6. First order logic

Resources: Computability and Logic Fifth Edition by Boolos, Burgess, Jeffrey

Level 7. Undecidability of first order logic

Resources: Computability and Logic Fifth Edition by Boolos, Burgess, Jeffrey

Level 8. Models, their existence. Proofs and completeness.

Resources: Computability and Logic Fifth Edition by Boolos, Burgess, Jeffrey

Level 9. Arithmetization. Representability of recursive functions

Resources: Computability and Logic Fifth Edition by Boolos, Burgess, Jeffrey

Level 10. Indefinability, undecidability, incompleteness. The unprovability of consistency.

Resources: Computability and Logic Fifth Edition by Boolos, Burgess, Jeffrey

5 comments

Comments sorted by top scores.

comment by moridinamael · 2019-07-17T12:44:20.914Z · score: 22 (11 votes) · LW · GW

I'm going to burn some social capital on asking a stupid question, because it's something that's been bothering me for a long time. The question is, why do we think we know that it's necessary to understand a lot of mathematics to productively engage in FAI research?

My first line of skepticism can perhaps be communicated with a simplified analogy: It's 10,000 BC and two people are watching a handful of wild sheep grazing. The first person wonders out loud if it would be possible to somehow teach the sheep to be more docile.

The second person scoffs, and explains that they know everything there is to know about training animals, and it's not in the disposition of sheep to be docile. They go on to elaborate all the known strategies for training dogs, and how none of them can really change the underlying temperament of the animal.

The first person has observed that certain personality traits seem to pass on from parent to child and from dog to puppy. In a flash of insight they conceive of the idea of intentional breeding.

They cannot powerfully articulate this insight at the level of genetics or breeding rules. They don't even know for a fact that sheep can be bred to be more docile. But nonetheless, in a flash, in something like one second of cognitive experience they've gone from not-knowing to knowing this important secret.

End of analogy. The point being: it is obviously possible to have true insights without having the full descriptive apparatus needed to precisely articulate and/or prove the truth of the insight. In fact I have a suspicion that most true, important insight comes in the form of new understandings that are not well-expressed by existing paradigms, and eventually necessitate a new communication idiom to express the new insight. Einstein invented Einstein notation because not just because it's succinct, but because it visually rearranges the information to emphasize what's actually important in the new concept he was communicating and working with.

So maybe my steelman of "why learn all this math" is something like "because it gives you the language that will help you construct/adapt the new language which will be required to express the breakthrough insight." But that doesn't actually seem like it would be important in being able to come up with that insight in the first place.

I will admit I feel a note of anxiety at the thought that people are looking at this list of "prerequisites" and thinking, wow, I'm never going to be useful in thinking about FAI. Thinking that because they don't know what Cantor's Diagonalization is and don't have the resources in terms of time to learn, their brainpower can't be productively applied to the problem. Whereas, in contrast, I will be shocked if the key, breakthrough insight that makes FAI possible is something that requires understanding Cantor's Diagonalization to grasp. In fact, I will be shocked if the key, breakthrough insight can't be expressed almost completely in 2-5 sentences of jargon-free natural language.

I have spent a lot of words here trying to point at the reason for my uncertainty that "learn all of mathematics" is a prerequisite for FAI research, and my concerns with what I perceive to be the unproven assumption that the pathway to the solution necessarily lies in mastering all these existing techniques. It seems likely that there is an answer here that will make me feel dumb, but if there is, it's not one that I've seen articulated clearly despite being around for a while.

comment by gwern · 2019-07-18T00:36:05.160Z · score: 21 (7 votes) · LW · GW

As a historical fact, you certainly can invent selective breeding without knowing anything we would consider true: consider Robert Bakewell and the wildly wrong theories of heredity current when he invented line breeding and thus demonstrated that breeds could be created by artificial selection. (It's unclear what Bakewell and/or his father thought genetics was, but at least in practice, he seems to have acted similarly to modern breeding practices in selecting equally on mothers/fathers, taking careful measurements and taking into account offspring performance, preserving samples for long-term comparison, and improving the environment as much as possible to allow maximum potential to be reached.) More broadly, humans had no idea what they were doing when they were domesticated everything; if Richard Dawkins is to be trusted, it seems that the folk genetics belief was that traits are not inherited and everything regressed to an environmental mean, and so one might as well eat one's best plants/animals since it'll make no difference. And even more broadly, evolution has no idea what 'it' is doing for anything, of course.

The problem is, as Eliezer always pointed out, that selection is extremely slow and inefficient compared to design - the stupidest possible optimization process that'll still work within the lifetime of Earth - and comes with zero guarantees of any kind. Genetic drift might push harmful variants up, environmental fluctuations might extinguish lineages, reproductively fit changes which Goodhart the fitness function might spread, nothing stops a 'treacherous turn', evolved systems tend to have minimal modularity and are incomprehensible, evolution will tend to build in instrumental drives which are extremely dangerous if there is any alignment problem (which there will be), sexual selection can drive a species extinct, evolved replicators can be hijacked by replicators on higher levels like memetics, any effective AGI design process will need to learn inner optimizers/mesa-optimizers which will themselves be unpredictable and only weakly constrained by selection, and so on. If there's one thing that evolutionary computing teaches, it's that these are treacherous little buggers indeed (Lehman et al 2018). The optimization process gives you what you ask for, not what you wanted.

So, you probably can 'evolve' an AGI, given sufficient computing power. Indeed, considering how many things in DL or DRL right now take the form of 'we tried a whole bunch of things and X is what worked' (note that a lot of papers are misleading about how many things they tried, and tell little theoretical stories about why their final X worked, which are purely post hoc) and only much later do any theoreticians manage to explain why it (might) work, arguably that's how AI is proceeding right now. Things like doing population-based training for AlphaStar or NAS to invent EfficientNet are just conceding the obvious and replacing 'grad student descent' with gradient descent.

The problem is, we won't understand why they work, won't have any guarantees that they will be Friendly, and they almost certainly will have serious blindspots/flaws (like adversarial examples or AlphaGo's 'delusions' or how OA5/AlphaStar fell apart when they began losing despite playing apparently at pro level before). NNs don't know what they don't know, and neither do we.

Nor are these flaws easy to fix with just some more tinkering. Much like computer security, you can't simply patch your way around all the problems with software written in C (as several decades of endless CVEs has taught us); you need to throw it out and start with formal methods to make errors like buffer overflows impossible. Adversarial examples, for instance: I recall that one conference had something like 5 adversarial defenses, all defined heuristically without proof of efficacy, and all of them were broken between the time of submission and the actual conference. Or AlphaGo's delusions couldn't be fixed despite quite elaborate methods being used to produce Master (which at least had better ELO) until they switched to the rather different architecture of AlphaZero. Neither OA5 nor AlphaStar has been convincingly fixed that I know of, they simply got better to the point where human players couldn't exploit them without a lot of practice to find reproducible ways of triggering blindspots.

So, that's why you want all the math. So you can come up with provably Friendly architectures without hidden flaws which simply haven't been triggered yet.

comment by moridinamael · 2019-07-18T06:17:28.928Z · score: 7 (4 votes) · LW · GW

To be clear, I didn't mean to say that I think AGI should be evolved. The analogy to breeding was merely to point out that you can notice a basically correct trick for manipulating a complex system without being able to prove that the trick works a priori and without understanding the mechanism by which it works. You notice the regularity on the level of pure conceptual thought, something closer to philosophy than math. Then you prove it afterward. As far as I'm aware, this is indeed how most truly novel discoveries are made.

You've forced me to consider, though, that if you know all the math, you're probably going to be much better and faster at spotting those hidden flaws. It may not take great mathematical knowledge to come up with a new and useful insight, but it may indeed require math knowledge to prove that the insight is correct, or to prove that it only applies in some specific cases, or to show that, hey, it wasn't actually that great after all.

comment by Pattern · 2019-07-18T05:44:21.528Z · score: 4 (3 votes) · LW · GW
The problem is, we won't understand why they work, won't have any guarantees that they will be Friendly, and they almost certainly will have serious blindspots/flaws (like adversarial examples or AlphaGo's 'delusions' or how OA5/AlphaStar fell apart when they began losing despite playing apparently at pro level before). NNs don't know what they don't know, and neither do we.

I hadn't heard about that. I suppose that's what happens when you don't watch all the videos of their play.

comment by rohinmshah · 2019-07-17T15:55:54.990Z · score: 10 (4 votes) · LW · GW

Fwiw I also think it is not necessary to know lots of areas of math for AI safety research. Note that I do in fact know a lot of areas of math relatively shallowly.

I do think it is important to be able to do mathematical reasoning, which I can roughly operationalize as getting to the postrigorous stage in at least one area of math.