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

11–20 of 66 posts

Re: Logical Induction

#11

Post by JohnStrange »

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.

It's a pretty cool idea but nothing groundbreaking. There is plenty of AI-driven mathematics already, e.g. the Mizar theorem prover. Pollock used to advocate the idea of continuously trying to prove theorems that might be useful later. It's an underrated idea, in my opinion, and his system of defeasible reasoning based on graph theory is still one of the best.

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.

Re: Logical Induction

#12

Post by tom_mellior »

JohnStrange wrote: post #11
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.

It's a pretty cool idea but nothing groundbreaking. There is plenty of AI-driven mathematics already, e.g. the Mizar theorem prover. Pollock used to advocate the idea of continuously trying to prove theorems that might be useful later. It's an underrated idea, in my opinion, and his system of defeasible reasoning based on graph theory is still one of the best. What's new in this paper is the probabilistic component,…

> AI-driven mathematics already, e.g. the Mizar theorem prover

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?

Re: Logical Induction

#13

Post by josh_fyi »

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

Re: Logical Induction

#14

Post by dharma1 »

Slightly OT but it's well worth watching the recent film about Ramanujan, "The Man Who Knew Infinity".

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.

Re: Logical Induction

#15

Post by adrianratnapala »

ajkjk wrote: post #10
m3kw9 wrote: post #3

Let it prove something first then we have something

This paper is a theoretical contribution, not a practical one, similar to Solomonoff Induction. Solomonoff Induction's contribution is essentially "there exists a formal mathematical process that inductive reasoning on evidence corresponds to" which, among other things, pretty much solves epistemological puzzles like the https://en.wikipedia.org/wiki/Raven_paradox from philosophy. Yeah, the actual performance of Solo…

That's interesting I had never heard of Solomonoff Induction until I read your comment. But how important, philosophically, is the existence of such a system, given that the brain already does exist as the "low fidelity analogue".

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.

Re: Logical Induction

#16

Post by bonoboTP »

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…

But can it show that it's actually running this correct algorithm to determine whether the statement about itself is probably true?

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.

Re: Logical Induction

#17

Post by nsomaru »

dharma1 wrote: post #14

Slightly OT but it's well worth watching the recent film about Ramanujan, "The Man Who Knew Infinity". 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.

If you're interested in that line of thought and would like perspective on the way perhaps Ramanujan might have perceived it, perhaps you may enjoy this transcript of a great lecture from an Indian holy man, mathematician and poet (Swami Rama Thirtha) in SF in 1903: http://www.ramatirtha.org/vol1/inspiration.htm

Re: Logical Induction

#18

Post by the8472 »

szemet wrote: post #7
m3kw9 wrote: post #3

Let it prove something first then we have something

Its too late, we already risk fortunes (and even lives) trusting in similar methods ;): 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.)

That's not quite correct, most prime proving algorithms are non-deterministic in their computation, but they don't necessarily produce false positives (like miller-rabin does), algorithms that only produce false negatives also exist (e.g. ECPP)

Re: Logical Induction

#19

Post by JohnStrange »

tom_mellior wrote: post #12
JohnStrange wrote: post #11

Earlier quoted context omitted.

It's a pretty cool idea but nothing groundbreaking. There is plenty of AI-driven mathematics already, e.g. the Mizar theorem prover. Pollock used to advocate the idea of continuously trying to prove theorems that might be useful later. It's an underrated idea, in my opinion, and his system of defeasible reasoning based on graph theory is still one of the best. What's new in this paper is the probabilistic component,…

> AI-driven mathematics already, e.g. the Mizar theorem prover 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…

Not really, I know people who work on Mizar but I'm not myself involved. Anyway it's also subjective what you call AI-driven and what not.

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.

Re: Logical Induction

#20

Post by tom_mellior »

JohnStrange wrote: post #19
tom_mellior wrote: post #12

Earlier quoted context omitted.

> AI-driven mathematics already, e.g. the Mizar theorem prover 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…

Not really, I know people who work on Mizar but I'm not myself involved. Anyway it's also subjective what you call AI-driven and what not. 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.

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.
Post reply on HN