Logical Induction
intelligence.org
Logical Induction
1–10 of 66 posts
Re: Logical Induction
#2So 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.
Re: Logical Induction
#3Let it prove something first then we have something
Re: Logical Induction
#4Let it prove something first then we have something
I think the purpose of this is to predict proofs ahead of time. Which could be useful in the management of people. As they say in the intro, given a group of specialists, this algorithm can guess, on a daily basis, which of the things they are working on are more likely to be true, and which are more likely to be false. Before the proof is finished.
Re: Logical Induction
#5So 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.
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 mathematicians don't like things that are probably true but not proven.
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.
Re: Logical Induction
#6So 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.
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…
This algorithm is not practical to implement using any computer that would fit on Earth. It's primarily of theoretical interest.
Re: Logical Induction
#7Let 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.)
Re: Logical Induction
#8Didn't the CIA have some experiment where they pooled a bunch of folks that were really good at guessing world events? Their constructions sounds awfully familiar to that experiment.
Re: Logical Induction
#9Didn't the CIA have some experiment where they pooled a bunch of folks that were really good at guessing world events? Their constructions sounds awfully familiar to that experiment.
IARPA ran something like that: https://en.wikipedia.org/wiki/Aggregative_Contingent_Estimat...
Re: Logical Induction
#10Let 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 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.)