Max Harms argues that corrigibility is a single, intuitive property that should be the sole training target for AGI, rather than one desideratum among many. Since a nearly-corrigible AI would assist efforts to make it more corrigible, careful refinement might converge on safe superintelligence. He's unsure this works, and later found serious flaws.
(If you're already familiar with all basics and don't want any preamble, skip ahead to Section B for technical difficulties of alignment proper.)
I have several times failed to write up a well-organized list of reasons why AGI will kill you. People come in with different ideas about why AGI would be survivable, and want to hear different obviously key points addressed first. Some fraction of those people are loudly upset with me if the obviously most important points aren't addressed immediately, and I address different points first instead.
Having failed to solve this problem in any good way, I now give up and solve it poorly with a poorly organized list of individual rants. I'm not particularly happy with this list; the alternative was publishing nothing, and publishing this seems marginally...
One of the great advantages of working with Gödel-Löb provability logic is that it's possible to implement an evaluator which efficiently checks whether a sentence in the language of GL is true. Mihaly and Marcello used this to write a program that checks whether two modal agents cooperate or defect against each other. Today, Nate and I extended this with an implementation of modal UDT, which allows us to check what UDT does on different decision problems---see Program.hs in the Github repository. No guarantees for correctness, since this was written rather quickly; if anybody is able to take the time to check the code, that would be very much appreciated!
The implementation of UDT is rather pleasing, I think. Here's the informal definition of modal UDT, using PA
TLDR: The first in a planned series of three or more papers, which constitute the first major in-road in the compositional learning programme, and a substantial step towards bridging agent foundations theory with practical algorithms.
Official Abstract: We propose novel algorithms for sequence prediction based on ideas from stringology. These algorithms are time and space efficient and satisfy mistake bounds related to particular stringological complexity measures of the sequence. In this work (the first in a series) we focus on two such measures: (i) the size of the smallest straight-line program that produces the sequence, and (ii) the number of states in the minimal automaton that can compute any symbol in the sequence when given its position in base