Logical Induction
intelligence.org
intelligence.org
The deeper motivation for this article is to allow future Artificial General Intelligences to prove facts about themselves; specifically, the fact that the AGI, or a next-gen that it developers, has the same (safe) utility function that the designers originally specified.
A formal system cannot achieve this by simulating itself.
A formal system cannot in general prove that it is reliable, i.e. that if it proves statement P then P is true. http://intelligence.org/files/lob-notes-IAFF.pdf
But with this article, the hope is that a formal system can show that the statement about itself is probably true.
I'm not entirely sure what you mean by this (I haven't read the article yet, and I'm already familiar with Loeb's theorem). It's true that you cannot show that, say, second order arithmetic is consistent in the same system. In fact, every soundness proof (for a sufficiently strong logic) will have to be carried out in a stronger system.
There is a standard way around this, which has existed for a long time. You stratify the system by introducing universes. E.g. in type theory, a universe is a type of (codes for) small types. This allows you to state and show meta theorems "for all (small) types", by quantifying over a universe.
In the concrete example of Martin-Loef type theory (MLTT) you can show that MLTT with n+1 universes contains a model of MLTT with n universes. On the other hand, adding more universes seems to be harmless as far as anyone knows.
Under the assumption that MLTT with a countably infinite number of universes is consistent and you restrict your formal system to only use a bounded number of universes, it is still possible to show that it is "reliable". It is "at least as reliable" as MLTT with countably many universes.
I will read the article later and update this post if there is something compelling in the paper. At the moment I'm just confused what the problem is, and would really appreciate it if you could expand on this.
As you say, this isn't quite self-trust. Another natural move is to relax the criterion of self-trust away from "it proves itself consistent" (impossible by incompleteness) towards "it assigns high probability that it has good beliefs". (Formalizations of this are in the paper.)
> At the moment I'm just confused what the problem is
In short, it would be nice to have a model of "good reasoning under deductive limitation", where "good reasoning" means something like "has accurate beliefs about all questions of interest" (for example, facts about the outputs of long-running computations), and where "deductive limitation" rules out the reasoning process "just wait for your theorem prover to decide the question".
Examples of long-running computations that are hard to compute exactly, but that we can sometimes still have reasonable beliefs about: optimal moves in chess, go, etc.; the accuracy of some ML system after a given training regimen; a weather-forecasting program that runs a gigantic series of simulations; and so on.
Self-trust seems like a problem on paper, but the reality is that normal mathematics uses very few universes. Concretely, the proof of the Feit-Thompson theorem in Coq, with all the related theories, uses 4 universes. If you have a system certified in type theory, then you can still reason about it. Possibly one universe higher, but that is not a problem (as far as anybody knows).
Self-trust (broadly construed) is interesting to me because it seems relevant to designing goal-based agents that are "stable", in the sense that they trust that future versions of themselves will have accurate beliefs (and therefore don't have an incentive to mess around with their systems for forming beliefs). If we try to formalize this intuition with "beliefs" as theorems proven by a formal system, we run into reflection problems; having your theorem prover assert that it will keep outputting only true statements feels awfully close to asserting its own soundness. So even if your agent can perform all the usual mathematical reasoning it needs, it still can't do all the useful reasoning about itself (it would need another large cardinal... and then another...).
The self-trust property in the paper says that it's possible to "learn from experience" that your future self is probably going to have pretty good beliefs. Specifically, a logical inductor P_n learns (roughly speaking) that "if P_f(n) thinks Phi is likely, then Phi is likely", where f(n) can be a fast-growing computable function. That is, on day n, P_n believes a sort of "probabilistic soundness" condition for its future self P_f(n). This is weaker than full soundness in at least two ways, but it is fully "reflective" in the sense that P believes this of itself.
On a separate matter, are there any principled meta-universal rules for incrementing the universe index? That is, if one suspects that one's current universe lacks proving power, is it possible to generate the axioms for a more powerful universe?
There are type theories with universe variables, which essentially allow you to add an arbitrary (but finite) number of additional universes. The rules for this are straightforward, even though a consistency proof is of course only possible relative to type theory or set theory with more universes...
In set theory, one typically adds an axiom scheme that states something like "There is a Grothendieck universe containing this set". Iterating this gives you a similar tower of universes.
There are a lot more constructions that go beyond this and the funny thing is that as far as anyone knows they are all consistent. For instance, type theories with induction-recursion allow you to generate internal universes closed under certain operations while staying in the same universe. So one universe with induction-recursion allows you to show MLTT with an arbitrary finite number of universes consistent.
There is always an external context that runs the computation. A computation never exists in "abstract space", it always happens on a physical level. Any computation is only good if it runs in the context that it was designed for.
What I mean is that the AI can never "know" if it's still following the "righteous goals", because a new environment may have grown around it, that "transforms" its inputs and outputs so that to the core machine it seems like nothing has changed, but actually its real-world effects have become very different. And at this point you could actually also say that this part of the environment has grown onto the AI machine and it now effectively has new goals that are incompatible with the ones designed into the core part of the machine.
My point is, there is no isolated system, reasoning by itself in an isolated fashion. Subject and environment are not clearly divided.
> at this point you could actually also say that this part of the environment has grown onto the AI machine
No, you cannot, if the environment is part of the definition of the machine, as you put it, A computation never exists in "abstract space", because if the environment changed, you'd have a new machine and all bets are off. You had that right at first.
Of course, that definition is unwieldy and we define interfaces as abstract and general as possible, to separate concerns. With involved machinery, that separation is not that clear cut, as their always two sides of the coin, to put it trivially.
This implies second order logic. It is not clear to me, whether the loss of consistency is warranted. Type Theories are tried to avoid inconsistence. However high the order of the processing logic is, its only reason to exist is to output first order theorems, those we can prove decidable.
> But with this article, the hope is that a formal system can show that the statement about itself is probably true.
Probabilty is not good enough. The Bayesian Conspiracy sure is strong, but I'd prefer to stay with first order logic and finite state machines that are provably correct.
> > The short answer is that this theorem illustrates the basic kind of self-reference involved when an algorithm considers its own output as part of the universe
Isn't that what differential equations are for? I'm tired of the liars paradoxon. Intuitively, I've settled on the presumption that paradoxa always rest on wrong assumptions.
I'm no mathematician, but I refuse the notion that I am inherently unable to be certain. That's why algorithms are by my preferred definition bound to be deterministic. I'd like to be able to tie this in with the Chomsky Hierarchy, albeit I am not that advanced. I'm no mathematician and I'm impressed by quines. I guess, the halting problem implies that quines cannot always be predicted. Heuristics help there and that's what stochastic is all about.
Let me be clear. The paradoxon "this sentence is a lie" is neither a sentence, nor a lie. That's a question of definition. Of course I'm in no position to say a similar thing about Goedels incompleteness theorem, and I even referred to it's result in higher order logics, but I still doubt the relevance, as many seem to be ignorant of his former completeness theorem.
The higher order logic and self reference is related to recursively enumerable grammars low in the Chomsky Hierarchy. Though, if ordered by magnitude, I'd call it higher. I hope, if the goal is natural language, we don't need to aim that high. If you want a computer that computes computers, though, go for it.
> A formal system cannot achieve this by simulating itself.
The type of self similarity used in quines or the liars paradox seems to play an important role in what we perceive as intelligent. Although, I stipulate, the intelligence involved is the ability to tell the difference between a misleading liars paradox and constructively provable quines. Of course, a machine that doesn't need verification from the supervising developer would be akin to a perpetuum mobile.
It is easy to supervise the AGI's output by the less intelligent machines that have to do the output. The focus is on optimizing the processes, not the inability to assert safety guidelines.
Edit: mixed up the order of the Chomsky Hierarchy.
No, it does not. The second incompleteness theorem is provable in first-order Peano Arithmetic.
> Of course I'm in no position to say a similar thing about Goedels incompleteness theorem, and I even referred to it's result in higher order logics, but I still doubt the relevance, as many seem to be ignorant of his former completeness theorem.
I have no idea what you're trying to say, but I assure you that people who do this kind of research are aware of the completeness theorem.
> A formal system cannot in general prove that it is reliable
I hadn't noticed when I wrote that, formal system is an idiom - even more specific in this specific context. How confusing.
Because there will always be statements that are true which the original system is oblivious to, and thus the corresponding questions will be outside its scope (incompleteness theorem).
It has kept me thinking what "intuition" really is, how it develops and happens in the brain, and what would be needed to build AI that has intuition.
http://danroy.org/papers/FreRoyTen-Turing.pdf -- TOWARDS COMMON-SENSE REASONING VIA CONDITIONAL SIMULATION: LEGACIES OF TURING IN ARTIFICIAL INTELLIGENCE
http://www.mit.edu/~tomeru/thesis/tomerThesis.pdf -- On the Nature and Origin of Intuitive Theories: Learning, Physics and Psychology
It is enjoyable reading and very thorough. Pending revolutionary new insights I might even regard it as conclusive.
That said, I can think of a number of uses for such an algorithm. If you load it full of conjectures in your field that are known to be true, it will might help you hone what problems are worth exploring by providing guess at how likely it is you can prove a statement you are pondering.
Careful. An event can have probability 1 even if its complement isn't empty: https://en.wikipedia.org/wiki/Almost_surely
What's new in this paper is the probabilistic component, trying to guess the outcome of complicated proofs. That's a neat idea, but nothing revolutionary. It may give rise to nice shortcuts for better efficiency.
The real problem is making the machine get a good hunch what to prove, so it doesn't find useful theorems just randomly. I'm not working in this field, so correct me if I'm wrong, but that seems to be rather hard. In any case, as far as I know most automated theorem provers are only semi-automatic, you have to give them an idea about which direction to go and which proof strategy to use.
I'm working in exactly this area, and it's very nice to see it mentioned occasionally as a useful direction!
There's a bunch of nice work being done on this problem; I'm mostly familiar with (roughly chronologically) IsaScheme, IsaCoSy, QuickSpec, Hipspec and Hipster. These take in a bunch of function definitions and output equations about them; they work by enumerating (type-correct) terms and using random testing (QuickCheck) to quickly separate unequal terms from each other, then they apply automated theorem provers to the remainder.
There are also more first-order, less computationally-focused systems for generating theorems out there, like HR and Graffiti.
Can you tell us more about how Mizar is AI-driven? I have never worked with it, but my understanding was that it was a fairly normal proof assistant. That is, proofs are written by humans, and some smallish boring intermediate steps are done using a regular first-order prover. Like with Coq or Isabelle.
Does Mizar do something else as well? Does it use AI to make conjectures?
I can comment on another thing, though. Even very simple concepts like well-foundedness conditions go beyond first-order logic and these provers are based on pretty expressive higher-order type systems. AFAIK, they can prove fairly substantial theorems.
But Yes, most common higher-order provers are semi-automatic, you need to give them a hint about which proof strategy to use. That's mainly because they are used that way, not any principal limitation. You won't find many mathematicians who are interested in a theorem prover to spit out some (alleged) theorem by itself, and then let the mathematician check whether it's useful.
The only fully automatic higher-order theorem prover that I know of is ETPS, it will select proof strategies by itself if you don't indicate them. But it's also one of the oldest and slowest and mainly just used for teaching logic.
I meant that the tactics of Coq that do reasoning for you, and the internal/external provers of Isabelle, are first order. I was probably partly wrong: you are right that some of them do use higher-order unification. But when in Coq I use "auto" or "omega" or whatever tactic to solve a goal, no higher-order tableaux are in use as far as I know. I have to massage the goal until I get it into a form that is palatable to the first-order automatic provers. Similarly, when I write an Isabelle proof like "from A have B by X; from this have C by Y; hence D by Z", the proof methods X, Y, Z are first order, often off-the-shelf SMT provers. Alternatively, there are also some built-in methods that use simple equational reasoning with higher-order unification, yes.
Let me know if I'm wrong about the details of this! Anyway, none of this means that you cannot prove complex higher-order stuff in these systems. You just can't do it automatically.
And, coming back to the start of this subthread, I don't think Mizar is really different in this regard.
There are a few hurdles to overcome before computer/AI-assisted mathematics really 'takes off', for example:
Almost all mathematics is aimed at a human reader; arguments are written in prose, and formula markup only exists to guide the appearance when rendered, i.e. LaTeX; just like HTML, it's technically all marked up and machine readable, but the semantic information we can extract is very low.
Whilst OCR, etc. will keep progressing, I think the real solution is to have people (or their tools) place semantics first and rendering second, e.g. with formats like OpenMath; to do this, we need to provide compelling reasons, e.g. automated assistance, inclusion in repositories, automated citations for those who use your results, etc.
Another problem is that there are many incompatible systems; if some result is formalised in a different system to the one you're using, your best option is to either switch system or attempt to re-prove it yourself. There are ongoing efforts to provide a more abstract overlay, so that results from one system can be re-used in another (providing their logics are somehow compatible), e.g. https://kwarc.info/projects
Another is how low-level automated reasoning currently is; even something which looks like a pretty clear instruction, like a step which says "by induction", involves such a huge search space that existing algorithms blow up. Working mathematicians, quite rightly, get fed up of the tedium of spelling out each individual step in such excruciating detail. It's just like with software, but imagine that you've spent your career working with a super fast Prolog system with a well-organised standard library built up over a thousand years, and you're then asked to program machine code by flipping switches on a slow machine with no existing software ;)
This is in the vein of "prediction using ensembles of experts" methods such as SI, with a twist that the experts are traders, not forecasters; they don't have to have opinions on everything the logical inductor has to predict, the traders just have to point out particular ways that the logical inductor is being silly (and then the logical inductor corrects those problems).
[0] In the sense of "valid under these known precepts", not "speculative".
[1] Non "Friendly AI", not "non-Friendly" AI.
When I say it feels like we spend a lot of time red teaming, that means I think we spend somewhere between 30 and 60% of research time trying to break things and see how they fail. This is fully compatible with not immediately implementing things - it's much less expensive to break something /before/ you build it.
Theoretical stuff is like: proving theorems, conceptualizing the task at hand, philosophical inquiry into the nature of agents/intelligence/reasoning/goals/human values
I'm not trying to argue which is more important, but surely MIRI focuses more on the theoretical.
Yeah, the actual performance of Solomonoff Induction is uncomputable, but to me the useful point is that "induction can be done mathematically", and then what we do heuristically in our brains can be thought of as a low-fidelity analog of that. If I'm understanding the page correctly, this is the same idea but for statements based on proofs and logical theorems. Which seems to expand the scope somewhat.
(I'm really excited about this, actually, just as a person who enjoys learning about this stuff from Wikipedia. I feel like I've vaguely thought about how Solomonoff induction would work on statements that are derived from each other (or when combined with type-checking, since type-checking is closely related to theorem-proving), but had no idea how to even ask a precise question much less make anything of it.)
The limits on what computers can do are related to logical no-go theorems such as Gödel's which are about proofs -- examples of certain knowledge. But once you have accepted the fallibility or "low fidelity" of human reasoning, then all those no-go theorems are no longer relevant in the first place.
Also, "simply prove/disprove the propositions" requires infinite computational resources (we don't know how long the proofs will be or if there are any). Logical induction does not.
https://en.wikipedia.org/wiki/Primality_test#Probabilistic_t...
(Primality is also a logical (analytic) truth and we are satisfied with probabilistic proofs - of course only because the risk is known and controllable.)
Some proof methods:
- BPSW. Deterministic, completely correct for all 64-bit values. Purely a compositeness test above, though no counterexamples known. This matches the false-positive idea -- above 64-bit it returns one of "definitely composite" or "probably prime."
- BLS 1975 methods. Relies on partial factoring N-1 and/or N+1 so unless the input is a special form, only practical to ~100 digits. No false results if the partial factoring can be done, and even gives a certificate of primality.
- APR-CL. Deterministic. No false results. Fast and practical up to ~5000 digits (one can debate where the impractical size line is). No certificate.
- AKS. Deterministic. No certificate. No false results. Very slow, so not generally used.
- ECPP. Non-deterministic (randomness is used internally), but no false results. Generates a certificate. Primo is practical up to ~30k digits (depends on your hardware and patience, but 10k digits on modern computers is quite practical). Open source implementations aren't as efficient, but still 1k+ digits is very reasonable. It is possible an implementation might be unable to proceed for various reasons and could return "gave up - no primality decision made" in addition to the choices "definitely composite" or "definitely prime (certificate included)". That's really a limitation of the implementation or the caller's patience.