This is from 2017, but I only just read it, and it did a lot to clarify for me why MIRI thinks work like Logical Induction is relevant to AI. Also does a good job crystalizing the reasons I (and the author) find this unpersuasive.
Funnily enough, I saw this message just after returning to tumblr from MR, because I wanted to repost here the reply I wrote to you! So, your time was definitely not wasted from my perspective, since it led me to think about an aspect of the topic I had not thought about before.
Thanks for the reply, Lee. I agree with you that assigning probabilities to theorems *at all* is a nontrivial problem, and insofar as the LI paper moves forward our understanding of this problem, that is good.
However, I am not convinced that the paper ever gives us a satisfying “assignment of probabilities to theorems.” What it gives us is two things — the limiting probabilities P_{\infty}, and the finite-time “probabilities” P_n. The former has some pleasant properties like assigning 0 < P < 1 to sentences independent of the axioms, but is essentially irrelevant to the original motivation of “how do we reason about things we can’t prove yet?”, since it is obtained “at the end” after every possible deduction has been made. (So it can make use of every possible proof, and the only thing it does above and beyond deduction is to put numbers on independent sentences.)
On the other hand, the finite-time P_n do not even have to form a probability measure at any time, and we cannot use them to do the sorts of things we would like do with probabilities, like decision theory. For instance, the authors define expectation values at time n but only prove that they behave well in the limit, and indeed the definition at time n involves an arbitrary choice which the authors justify because it washes out in the limit (see p. 40). Of course, any way that P_n fails to be a probability measure will disappear in the limit, because the limit is P_{\infty}; but if we let ourselves wait for P_{\infty} we forfeit any ability to reason probabilistically about theorems before they are proven. If we want to do that, we have to use the finite-time P_n, but in fact we cannot reason probabilistically with these at all.
After their more careful review process in 2016, with 7 external reviewers and 4 papers under review, OpenPhil has just decided to give MIRI 2.5 times as much money for 3 guaranteed years because one ~super-special~ expert (unnamed) liked the Logical Induction paper
On the one hand, aaaargghhhhh
On the other hand, I’m curious about this unnamed reviewer, who is apparently “generally regarded as outstanding by the ML community” – I can’t imagine they didn’t notice the same flaws in the LI paper that I did, so maybe they came up with some next-level glowing-brain take on why it’s actually good?
People who follow MIRI are probably aware of the extensive, somewhat negative evaluation of MIRI that OpenPhil did in fall 2016
But one thing about this evaluation that took me a while to notice – and which I suspect a lot of people still aren’t aware of? – is that OpenPhil released a supplement (PDF) containing the text of the anonymous external reviews, as well as MIRI’s internal reviews of the same papers, and MIRI’s responses (PDF) to the external reviews
(It’s linked in the evaluation post, but it’s one little link in a long post, and is easy to miss)
The external comments are very interesting, both from the general “what do academics think of MIRI’s work?” perspective and for many of the specific things the reviewers say.
For instance, the one external review for a paper on reflection was quite positive, while the external reviews for the two papers related to logical induction were much more negative. These reviews were done before the LI paper was published; in the evaluation post, the material in the LI paper is referred to as the mystery-shrouded “Result 5,” as in this noteworthy sentence:
MIRI feels its most recent result (the unpublished Result 5) is more impressive than its older work, but we will have substantial uncertainty on this point until the work has been written up and we have had a chance to review it more thoroughly.
Below, I quote some noteworthy comments by the external reviews.
On the reflection paper:
As far as I know, this paper gives the first demonstration of a system that can support an arbitrarily deep tower of reflective reasoning within a general-purpose mechanized logic. […] It’s a new and intuitively appealing capability that is nontrivial to implement.
[…]
I see these results as an important milestone toward formal analysis of systems with some level of self-understanding.
On the “Logical Coherence” paper, one of two predecessors to the LI paper:
As I said, I don’t find the results of this paper particularly interesting. The first paragraph suggests that this problem is motivated by the concern of assigning probabilities to computations. This can be viewed as an instance of the more general problems of (a) modeling a resource-bounded decision maker computing probabilities and (b) finding techniques to help a resource-bounded decision maker compute probabilities. I find both of these problems very interesting. But I think that the model here is not that useful for either of these problems. Here are some reasons why […]
I see no obvious modification of uniformly coherent schemes that would address these concerns. Even worse, despite the initial motivation, the authors do not seem to be thinking about these motivational issues. […]
Additional comments: I’ve looked (not very carefully) at 2-3 other MIRI papers, and I had much the same reaction in terms of motivation. These are smart guys, but they have no real computer science sensibilities (although their steering committee certainly has terrific folks with great CS sensibility!).
More on the “Logical Coherence” paper, from a second external reviewer:
Whether these assurances, and the related algorithm, have important significance is a matter for debate. It is to a large extent a subjective question. This reviewer is not extremely impressed but others might feel differently.
What I would have liked to see are concrete natural examples where their algorithm assigns some natural probabilities and prior constructions do not.
Also, there is an inherent issue with algorithms that work by enumerating over all proofs. They run in exponential time and even practically it seems that this enumeration will quickly explode before we see any reasonable probabilities.
On the “online learning with unbounded delays” paper, the other predecessor to the LI paper:
The observation that under unbounded delays no algorithm can compete with the best expert in hindsight, albeit a trivial one, has not appeared in the literature before. The same is true for the particular positive result proven.
[…]
There are several problems in the proofs and the validity of the results cannot be established (though the reviewer suspects that the proof can be fixed with considerable effort). In particular, there are important problems in the proof of Lemma 7, which is a main ingredient of Theorem 5, the main result of the paper. For example: [reviewer goes on to describe 3 perceived errors they found]
[…]
The results are vaguely relevant for this problem [i.e. logical induction].
First, the requirement of asymptotic consistency (in the sense of matching the loss of a Bayes-optimal expert) is on one hand very weak (asymptotics is “easy”), while at the same time, the particular assumptions, being able to access a Bayes-optimal expert and the strong convexity of the “loss”, are very strong. In any remotely practical setting, we don’t expect these to hold and there is not much novelty in achieving asymptotic consistency by comparing losses. […]
Finally, even if this interpretation is correct, it is only made possible by a computationally expensive algorithm under the strong assumption of having access to a Bayes-optimal forecaster, and only for strongly convex losses. Note that while the authors are trying to provide an answer to this question “in principle”, computational concerns do matter for this specific question, as discussed next.
As usual, online learning of course offers a powerful set of tools for addressing prediction problems, but online learning can only do so much. In particular, one can push online learning towards philosophy (lacking any practical relevance), e.g., by using infinite expert sets and unbounded computational power, as done here. But it is rather intriguing if not self-defeating if this is done in the context of trying to answer a question that is derived from the lack of sufficient computational resources!
More on the “online learning with unbounded delays” paper, from a second external reviewer:
This paper’s conclusions add very little to what is already known. The problem is that the setup considered in this paper (of unbounded delays) is far too general to be analyzable theoretically or useful practically. […]
I do not think these results any significant light on standards for good reasoning under deductive limitations. The primary reason is that the setup is far too general and too unrealistic, and the algorithm completely impractical. It would be far better to model the problem of delays more realistically and come up with efficient algorithms to deal with delay.
@somervta helpfully linked my post about LIs on agentfoundations.org, MIRI’s forum for technical discussion, and it’s getting some comments over there – here’s the thread if you’re interested
(I didn’t link it myself because you can only register there via Facebook and I didn’t want to do that)
I clicked through with Facebook just to see what would happen, and instead of forcing me to go by my real name like I expected, it forced me to go by “240″ (because I’m user number 240). I was like, OK, fine, and I wrote a really long comment, only to find that it’s only visible when I’m logged in? Anyway, here’s confirmation that “240″ is really me in case anyone wanted it.
@somervta helpfully linked my post about LIs on agentfoundations.org, MIRI’s forum for technical discussion, and it’s getting some comments over there – here’s the thread if you’re interested
(I didn’t link it myself because you can only register there via Facebook and I didn’t want to do that)
(long OP snipped for space, but may be worth looking at for context)
I thought about this more, and concluded that Jaynes’ propositional formulation of probability is more different from Kolmogorov than I thought, and really does have an advantage in this case.
Both the Jaynes and Kolmogorov formulations have some some of Boolean algebra structure, which the probabilities are constrained to respect. In Kolmogorov, this arises because probabilities get assigned to sets, and you get a Boolean algebra from the unions/intersections of the sets. In Jaynes, probabilities are assigned to propositions and the Boolean algebra comes from logical and/or/not.
The difference is in the “basic atoms” of the algebra. In Kolmogorov, the sets contain things, called “outcomes,” and the “smallest” set you can make (besides the empty set) is a singleton with just one of the outcomes in it. All of these distinct singletons are mutually exclusive events, so they can’t be proper subsets of one another, which is the structure you need if you want to encode material conditionals (i.e. the kind of “A→B” that is equivalent to “¬A or B”). In Kolmogorov, material conditionals only arise from the subset relationships between bigger, non-atomic events.
But in Jaynes, the basic atoms are atomic propositions (i.e. propositions like “A” which are not aliases for compounds like “B or C,” but are undefined within the algebra itself). For two atoms A and B, the material conditional “¬A or B” is a perfectly good compound proposition, and we can (say) begin by being unsure of its truth value and later update after we prove it (by conditioning on it), as @eclairsandsins was suggesting upthread.
If we try to translate this back to the Kolmogorov picture, the compound propositions follow the same algebra as Kolmogorov events (sets), but the atomic propositions are weird “sets of unknown structure”: their unions, intersections, etc. exist in the algebra but we don’t know anything about their contents. This is exactly the sort of thing I needed in the OP to encode material conditionals, and generally seems preferable to the “you have to already know everything” feel of the Kolmogorov setup.
If we move from material conditionals to counterfactual conditionals, things get harder. (Counterfactual conditionals are the type I mentioned earlier that can be false even if antecedent and consequent are false: e.g. “if I were in Mexico, I’d be in Asia” is false even though I am in neither.) The Boolean algebra can tell us that certain things are logically possible even if they are contingently false (e.g. A and ¬A are both in the algebra, but we happen to assign P(A) = 0), but I don’t think this does the whole job, for which I think we need predicate calculus or modal logic rather than just propositional logic.
For instance, even if Linda is not a bankteller at all, I believe it is false (in the counterfactual conditional sense) that “(Linda is a bankteller) → (Linda is a feminist bankteller).” Not just because non-feminist banktellers are logically possible, but actually possible. For this I need the “there exists” of predicate calculus, or (better?) the “is possible” of modal logic. David Chapman has a post saying that Jaynes’ setup doesn’t generalize to predicate calculus; I linked it a while back and remember getting pushback from @raginrayguns about it, but I don’t remember the details.
Anyway, the motivation for all this was thinking about logical induction. If we want to reason sensibly about the probabilities of logical statements, we ought to be able to do it about (at least) statements of first-order predicate calculus, and possibly higher-order (?) as well. We’re talking about trying to assign probabilities to math conjectures here; we at least need to be able to deal with Peano arithmetic.
The MIRI formalism outsources this task to the e.c. traders, which doesn’t tell us how efficiently it can actually be done; if for instance we need a separate trader for each case of a “for all” sentence, that would still get the job done in MIRI’s asymptotic sense, but effectively means that we can’t do it in practice (one would like to be able to take in the sentence “all at once”). Quantifiers can be parcelled out into conjunctions/disjunctions of countably many propositions, but we’d like to avoid that if we can (one should be able to do mathematical induction without needing infinite storage space to hold P(n) for every integer.) IDK, it just seems like “can we do this sort of probability in practice” is the real question, and the MIRI work sidesteps that.
(via nostalgebraist)
I’ve been thinking a bit about the how to get a “uniform rather than pointwise” version of the logical induction stuff.
It seems like a lot of the challenge of the problem is generic to Bayesianism, and not particular to “logical” or “mathematical” outcomes. Anyone who reads my posts on this stuff knows I have an axe to grind about how, outside of specialized small domains, you don’t have a complete sigma-algebra to put probabilities on. (Because you aren’t logically omniscient, you don’t know all the logical relations between hypotheses, which means you don’t know all of the subset relationships between sets in your algebra.)
The case of “logical induction” forces Bayesians to think about this even if they wouldn’t otherwise, since the prototypical/motivating examples involve math, a world in which we are continually discovering facts of the form “A implies B.” So assuming logical omniscience would be assuming we know all the theorems at the outset, in which case we wouldn’t need LI to begin with.
But the problem that “A may imply B even though you don’t know it does” is generic and comes up for Bayesian inference about real-world events, too. A good solution to this problem would be very interesting and important (?) even if it didn’t, in itself, handle the “logical” aspects of “logical induction” (like “what counts as evidence for a logical sentence”).
I have to imagine there is work on this problem out there, but I have had a hard time finding it.
The basic mathematical setup would have to involve some “incomplete” version of a sigma-algebra (generically, a field of sets), where not all of the union/intersection information is “known.” This is a bit weird because when we talk about a collection of sets, we usually mean we know what is in the sets, and that information contains all the relations like “A is a subset of B” (i.e. B implies A), when we want to make some of them go away.
A Boolean algebra is like a field of sets where we forget what the sets contain, and just leave them as blank symbols that happen to have union/intersection (AKA “join/meet”) relations with one another. That seems closer to what we want, except that we need some of the join/meet operations to give undefined results. There are Boolean algebras where not everything has a join/meet (those that aren’t complete, in the complete lattice sense), but this seems like a thing having to do with inf/sup stuff in infinite spaces and isn’t really what we want. (Despite my username, I know very little about algebra and am just flying blind on Wikipedia here.)
An example of the sort of thing I want to do is the following. Say we are assigning probabilities in (0,1) to P(A), P(B), P(A=>B), and P(B=>A). Suppose P(A=>B) > P(B=>A), that is, we think it’s more likely that A implies B than the reverse (and in particular, more likely than A<=>B).
Now consider P(A) and P(B). The probabilities above say we’re most likely to be in a world where A=>B and not vice versa, in which case we should have P(A) > P(B), or we’ll be incoherent. So it seems like we should have P(A) > P(B) right now. Of course, this will make us incoherent if it turns out that we are in the B=>A or A<=>B worlds, but we think those are less likely. In betting terms, the losses we might incur from incoherence in a likely world should outweigh those we’d incur from incoherence in an unlikely world.
What we’re really doing here, I guess, is treating the implication (i.e. subset relation) as a random event, so implicitly there is a second, complete probability space whose events (or outcomes?) include the subset relations on the first, incomplete probability space (the one discussed above). Maybe you could just do the whole thing this way? I haven’t tried it, I’m curious what would happen
Anyway, I can’t help but think there must be the right math tools out there for doing this kind of thing, and I just don’t know about it. Anyone have pointers?
Um, if P(A → B) > P(B → A) then P(A) < P(B) not greater. Imagine if P(A → B) = 90% and P(B → A) = 30%. The only difference between the truth tables of A → B vs B → A is that the former is false only when A is true and B is false, and the latter is false only when B is true and A is false. So, P(A and ¬B) = 10% and P(B and ¬A) = 70%. The latter tells you that P(B) > 70% and P(¬A) > 70% aka P(A) < 30%. Therefore P(B) > P(A). To get a more general proof use variables instead of 90% and 30%.
By the way, “A → B” is just another way of saying “¬A or B,” and you just apply normal probability to the latter.
Ah, I think we are using two different meanings for the → sign.
In the Kolomogorov defn. of a probability space, we have to have a sigma-algebra (which specifies sets [“events”] and their union/intersection relations) before we assign any probabilities. If A, B are in the sigma-algebra and B is a subset of A, this is interpreted as “if event A happens, event B must also happen.” If we are taking A and B to be propositions, this means “A implies B.”
In the usual Bayesian framework, the events are propositions, but (our beliefs about) truth and falsehood are represented by probability assignments we give to the events, and we can only make these assignments if we have the sigma-algebra already. So the sigma-algebra encodes implication relationships which we are supposed to assent to before we take the step where we say certain propositions are true (P=1) or false (P=0).
To use the classic example, the sigma-algebra will have “Linda is a feminist bankteller” (A) as a subset of “Linda is a bankteller” (B). Then when we go and assign probabilities, the probability axioms tell us that we must respect this implication (A→B). Among other things this will mean that we assign probability 1 to “¬A or B,” for the trivial reason that “¬A or B” is the set of all outcomes. But this is not the sort of thing that the framework allows us to not know, and then figure out: it is fixed by the sigma-algebra at the outset.
So when I write things like P(A → B), I am talking about the sort of relation we normally get from the sigma-algebra. Such a relation goes beyond the truth tables: the sigma-algebra normally tells us things like “if Linda is a feminist bankteller, Linda is a bankteller” which are true (in the relevant sense) even if Linda is neither of those things in reality (in which case the truth tables are mute). There’s a connection to math progress here, in that often mathematicians are concerned about the consequences of assuming certain axioms but agnostic about the truth of the axioms; “the well-ordering theorem is equivalent to the axiom of choice” is interesting, even thought you will be hard pressed to find people who think they’re both true or both false (it is contested what that would even mean!).
It sounds like you’re coming from Jaynes’ approach to probability, while I’m used to Kolmogorov; the two are close to equivalent, but I’ll have to think more about whether Jaynes’ version makes this problem easier.
I’ve been thinking a bit about the how to get a “uniform rather than pointwise” version of the logical induction stuff.
It seems like a lot of the challenge of the problem is generic to Bayesianism, and not particular to “logical” or “mathematical” outcomes. Anyone who reads my posts on this stuff knows I have an axe to grind about how, outside of specialized small domains, you don’t have a complete sigma-algebra to put probabilities on. (Because you aren’t logically omniscient, you don’t know all the logical relations between hypotheses, which means you don’t know all of the subset relationships between sets in your algebra.)
The case of “logical induction” forces Bayesians to think about this even if they wouldn’t otherwise, since the prototypical/motivating examples involve math, a world in which we are continually discovering facts of the form “A implies B.” So assuming logical omniscience would be assuming we know all the theorems at the outset, in which case we wouldn’t need LI to begin with.
But the problem that “A may imply B even though you don’t know it does” is generic and comes up for Bayesian inference about real-world events, too. A good solution to this problem would be very interesting and important (?) even if it didn’t, in itself, handle the “logical” aspects of “logical induction” (like “what counts as evidence for a logical sentence”).
I have to imagine there is work on this problem out there, but I have had a hard time finding it.
The basic mathematical setup would have to involve some “incomplete” version of a sigma-algebra (generically, a field of sets), where not all of the union/intersection information is “known.” This is a bit weird because when we talk about a collection of sets, we usually mean we know what is in the sets, and that information contains all the relations like “A is a subset of B” (i.e. B implies A), when we want to make some of them go away.
A Boolean algebra is like a field of sets where we forget what the sets contain, and just leave them as blank symbols that happen to have union/intersection (AKA “join/meet”) relations with one another. That seems closer to what we want, except that we need some of the join/meet operations to give undefined results. There are Boolean algebras where not everything has a join/meet (those that aren’t complete, in the complete lattice sense), but this seems like a thing having to do with inf/sup stuff in infinite spaces and isn’t really what we want. (Despite my username, I know very little about algebra and am just flying blind on Wikipedia here.)
An example of the sort of thing I want to do is the following. Say we are assigning probabilities in (0,1) to P(A), P(B), P(A=>B), and P(B=>A). Suppose P(A=>B) > P(B=>A), that is, we think it’s more likely that A implies B than the reverse (and in particular, more likely than A<=>B).
Now consider P(A) and P(B). The probabilities above say we’re most likely to be in a world where A=>B and not vice versa, in which case we should have P(A) > P(B), or we’ll be incoherent. So it seems like we should have P(A) > P(B) right now. Of course, this will make us incoherent if it turns out that we are in the B=>A or A<=>B worlds, but we think those are less likely. In betting terms, the losses we might incur from incoherence in a likely world should outweigh those we’d incur from incoherence in an unlikely world.
What we’re really doing here, I guess, is treating the implication (i.e. subset relation) as a random event, so implicitly there is a second, complete probability space whose events (or outcomes?) include the subset relations on the first, incomplete probability space (the one discussed above). Maybe you could just do the whole thing this way? I haven’t tried it, I’m curious what would happen
Anyway, I can’t help but think there must be the right math tools out there for doing this kind of thing, and I just don’t know about it. Anyone have pointers?
(2/?) Because of this, I’m concerned only with asymptotic properties. But as you and jadagul note, there are multiple kinds of asymptotics. I think the asymptotic is stronger than you give it credit for. As you note, it only satisfies a finite number of conditions at a time, where the conditions are given by polynomial-time traders. But a polynomial-time trader can do a lot. One simple thing it can do is ensure logical consistency by looking for arbitrage opportunities based around simple proofs
(¾) Another is to ensure that, as more examples of a general statement are verified, the probability of the statement goes up. etc. etc. So I think you can write a long list of desirable properties as a finite set of traders, and guarantee your algorithm satisfies these properties after some finite time T. The only weakness has to do with the polynomial time nature of the traders e.g. if we look for arbitrage opportunities by brute force search, we can only find ones of logarithmic length.
(4/4) Any logical inductor, not just MIRI’s design, will solve problems exponentially slower than you might reasonable hope. We can reduce an arbitrary computational problem to logical induction by writing “What is the output of this computation?” as a mathematical statement. This means every clever algorithm in the universe can be used to speed up a logical inductor. Because we only know finitely many algorithms, and there are probably infinitely many, our inductors are very slow.
I talked to someone else yesterday who defended the paper for similar reasons – this is a hard problem, and “evade polynomial-time traders” may be a good way to philosophically think about what an answer ought to look like.
I guess the fundamental problem I have with the paper is not with this concept itself but with the way it’s formalized. Their non-intuitive definition of exploitation/arbitrage breaks a lot of the intuitions we might have about why this concept would work well. It’s not capturing what you describe in (3) – rather than talking about which desirable properties the agent is guaranteed to have simultaneously, it only talks about the ones which all hold for the limit. You are not guaranteed to ever get a state with all these properties, so intuitions about the desirability of such a state are not applicable.
(As @jadagul says, if a conjunction of e.c. traders is infinite, you may never resist it at any time; the limit is then like a discontinuous function which is the limit of a series of continuous ones. If you want discontinuity, you will literally never be satisfied.)
Formalizing a version of the concept that captures what we actually want out of it might be great, but that’s not what the paper does. And I’m not ready to get my socks blown off by this e.c.-traders-for-induction stuff until it is more than just a nebulous idea without specifics.
I just re-read this and realized I missed the word “finite” when you said “So I think you can write a long list of desirable properties as a finite set of traders … “ So yeah, if it’s a finite set of traders, you can avoid them all simultaneously by some N. I didn’t really get your argument, sorry.
But I’m not convinced this is true, or anyway it’s not intuitive to me and I’d need to see actual proofs. Informally speaking, I’m worried about cases where there is an infinity (or a finite but combinatorially exploding number) of distinct sentences (or whatever) which we have to handle to get a property, and one can get any one of them with an e.c. trader, but not the whole set. E.g. their timely learning property holds for “e.c. sequences” of theorems, and they prove it by writing an e.c. trader that tries to exploit a single arbitrary sequence. But there are many, probably infinitely many (?), ways to generate sequences of theorems in polytime (I think this is a similar claim to your point 4), and it’s not clear to me that you could objectively choose some finite subset which would correspond to “basically sensible behavior at time n.”
And even if you could, the LI criterion is indifferent between finite subsets that have this “make you sensible” property and those that don’t, so if this is the core of why we want to evade e.c. traders, the LI criterion is not capturing it.
Like, yeah, you do eventually get the conjunction you want. But you have to remember that there is no metric oomph to these convergence results – general convergence rate results for all LIs don’t exist, because you can get an LI just by counting traders in an arbitrary order. Even though these results are written with epsilons and Ns, we shouldn’t imagine any sort of steady trajectory “towards” any of the limits. LIA doesn’t move toward any property, it just suddenly gets each property when it lists the corresponding trader.
Even calling these results “asymptotic” seems kind of misleading to me. It’s asymptotic in the sense that brute force search for an NP problem will “asymptotically” find the solution (i.e. get nowhere and then suddenly solve the problem at some unknown magic time), not in the sense of gradient descent or something.
A more general comment: all of this stuff is interesting, perhaps more so than what is actually in the paper, but it isn’t in the paper. Given how much formal work the authors did and how many distinct results they proved, it’s not a defense of the paper (although it may be a defense of the concept) to cite some non-trivial statement they didn’t prove but which could be true. If it were good enough to just say “well you could probably do this,” then why do we care about all the rigorous stuff in the paper? If that stuff is orthogonal to the “actual” reason the concept is good, why did the authors prove it?