Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Logical Induction

intelligence.org

Post reply on HN
Print view View original

31–40 of 66 posts

Re: Logical Induction

#31

Post by joshcohen »

eli_gottlieb wrote: post #30
joshcohen wrote: post #24

Earlier quoted context omitted.

It's not clear if there are any practical applications to automated theorem proving (and that's not the goal of the work). This is primarily motivated by very "theoretical" decision theory.

How do you manage to claim that your computable logical inductor dominates the incomputable universal semimeasure?

I'm not an author but this property with respect to a universal 'semimeasure' holds in the limit as time goes to infinity, as do most stated properties of logical inductors. The fact that they're computable is academic.

Re: Logical Induction

#32

Post by tom_mellior »

JohnStrange wrote: post #27
tom_mellior wrote: post #20

Earlier quoted context omitted.

I didn't say that the proof assistants were first order! I'm well aware that that's not the case. But AFAIK all the automation they use is first order. Higher order proof steps like "do this by induction on n " are always introduced by hand (at least in Coq and Isabelle), even if the rest of the proof is automatic.

I don't understand what you mean by "all the automation they do is first order". They are based on higher order proof theories, e.g. higher order tablaux, and they implement higher order unification. Otherwise they would be first-order provers and thus much more limited. 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…

> I don't understand what you mean by "all the automation they do is first order".

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.

Re: Logical Induction

#33

Post by bbctol »

gjdjcjdnxnvjd wrote: post #2

So does this mean that the era of automated theorem proving and AI-driven mathematics is finally upon us? I'm no expert, but this seems pretty groundbreaking.

This is MIRI; they do really interesting theoretical philosophy and worryingly small amounts of practical research.

Re: Logical Induction

#34

Post by chriswarbo »

gjdjcjdnxnvjd wrote: post #2

So does this mean that the era of automated theorem proving and AI-driven mathematics is finally upon us? I'm no expert, but this seems pretty groundbreaking.

Keep in mind that theorem proving was one of the very first applications of AI (e.g. Newell and Simon's "Logic Theorist" in the 1950s), so I would take any excitement with as much salt as any other AI claim ;)

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 ;)

Re: Logical Induction

#35

Post by tnecniv »

catnaroek wrote: post #23
tnecniv wrote: post #5

Earlier quoted context omitted.

My understanding from the article (while I would like to read the paper, I don't have time at the moment) is that it assigns probabilities that a conjecture is correct and improves these estimates over time. As such, something will only really be proven true when the probability hits 1. The summary says that this will occur in the limit, but that might take as long as proving things the traditional way and mathematic…

> something will only really be proven true when the probability hits 1 Careful. An event can have probability 1 even if its complement isn't empty: https://en.wikipedia.org/wiki/Almost_surely

Good catch. The nuances of the continuum are many and subtle.

Re: Logical Induction

#36

Post by Natanael_L »

posterboy wrote: post #21
josh_fyi wrote: post #13

The article is basic mathematical research and is not intended to be implemented, but rather to guide further applied research. 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 can…

> A formal system cannot in general prove that it is reliable, i.e. that if it proves statement P then P is true 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…

The inability to be certain comes from the fact that we always can ask arbitrarily complex questions about the subject matter. To prevent the halting problem, you must prevent complex questions.

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).

Re: Logical Induction

#37

Post by fmap »

josh_fyi wrote: post #13

The article is basic mathematical research and is not intended to be implemented, but rather to guide further applied research. 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 can…

> A formal system cannot in general prove that it is reliable, i.e. that if it proves statement P then P is 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.

Re: Logical Induction

#38

Post by AlexMennen »

posterboy wrote: post #21
josh_fyi wrote: post #13

The article is basic mathematical research and is not intended to be implemented, but rather to guide further applied research. 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 can…

> A formal system cannot in general prove that it is reliable, i.e. that if it proves statement P then P is true 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…

> This implies second order logic.

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.

Re: Logical Induction

#39

Post by jey »

bbctol wrote: post #33
gjdjcjdnxnvjd wrote: post #2

So does this mean that the era of automated theorem proving and AI-driven mathematics is finally upon us? I'm no expert, but this seems pretty groundbreaking.

This is MIRI; they do really interesting theoretical philosophy and worryingly small amounts of practical research.

What is your definition of practical?

Re: Logical Induction

#40

Post by tbt »

eli_gottlieb wrote: post #30
joshcohen wrote: post #24

Earlier quoted context omitted.

It's not clear if there are any practical applications to automated theorem proving (and that's not the goal of the work). This is primarily motivated by very "theoretical" decision theory.

How do you manage to claim that your computable logical inductor dominates the incomputable universal semimeasure?

The universal semimeasure is "computably approximable from below", aka (lower) semicomputable, meaning that you can computably list out all the rational numbers below a given value assigned by the measure. The probabilities assigned by a logical inductor are computably approximable reals, which (confusingly) is weaker than lower semicomputable; it just means that you can compute a sequence of rationals that converges to the real, with a possibly uncomputable convergence rate.
Post reply on HN