6 ms·

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.

tnecniv 10y ago
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.
- jey 10y ago
  This algorithm is not practical to implement using any computer that would fit on Earth. It's primarily of theoretical interest.
- catnaroek 10y ago
  > 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 https://en.wikipedia.org/wiki/Almost_surely
  - joshcohen 10y ago
    In this setting we're using discrete probabilities so we don't have to worry:)
  - tnecniv 10y ago
    Good catch. The nuances of the continuum are many and subtle.
JohnStrange 10y ago
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.
- tom_mellior 10y ago
  > 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?
  - JohnStrange 10y ago
    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.
    - tom_mellior 10y ago
      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.
joshcohen 10y ago
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.
- eli_gottlieb 10y ago
  How do you manage to claim that your computable logical inductor dominates the incomputable universal semimeasure?
  - joshcohen 10y ago
    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.
    - tbt 10y ago
      This is right, but perhaps misleading; most of the properties are "asymptotic", meaning that they may take an extremely long time to hold, but they hold at finite times. For example, "provability induction" says that if you have a (polytime computable) sequence of sentences phi_n, all of which happen to be provable (possibly with fast-growing proof lengths), then P_n(phi_n) limits to 1. This means that on day n the logical inductor P is confident of phi_n, even though phi_n may take much longer than n steps to prove.
      - joshcohen 10y ago
        Although P_n can't be computed in anything like n steps.
        tbt 10y ago
        Yeah. It's still surprising to me, though; P_n can predict extremely long-running computations, even ones with a much longer runtime than P_n, at least as well as any quickly computable "pattern". (The algorithm in the paper uses a (roughly) double-exponential-time algorithm to predict arbitrarily long-running programs, in a way that can't be improved upon by any polytime computable method.)
bbctol 10y ago
This is MIRI; they do really interesting theoretical philosophy and worryingly small amounts of practical research.
- jey 10y ago
  What is your definition of practical?
  - bonoboTP 10y ago
    My concept of practical is stuff like: implementing things, doing experiments with prototypes, producing stuff that is imperfect but does something and can be improved upon. 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.
  - jpt4 10y ago
    MIRI is entirely Blue Team - they work to create theoretical [0] safeguards on AI agents yet to be developed. I've long envisioned a counterpart Red Team that does nothing but build AIs that attempt to subvert these safety features, since the rest of the world of non Friendly AI [1] research is only unco-ordinated para-red behavior. [0] In the sense of "valid under these known precepts", not "speculative". [1] Non "Friendly AI", not "non-Friendly" AI.
    - gallabytes 10y ago
      I find that perception fairly surprising, as for a very long time it felt like we did more red team than blue team. I do acknowledge that this has been changing recently, but only significantly in the context of building on the results in this paper.
      - jpt4 10y ago
        Would you please direct me to an example of MIRI's Red Team efforts that isn't the recent "Malevolent AI" paper [0]? Adherence to the belief that UFAI is a threshold-grade existential risk seems to compel a "define first, delay implementation" strategy, lest any step forward be the irrevocable wrong one. [0] http://arxiv.org/abs/1605.02817 http://arxiv.org/abs/1605.02817
chriswarbo 10y ago
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 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 ;)

tnecniv 10y ago

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.

jey 10y ago
This algorithm is not practical to implement using any computer that would fit on Earth. It's primarily of theoretical interest.
catnaroek 10y ago
> 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 https://en.wikipedia.org/wiki/Almost_surely
- joshcohen 10y ago
  In this setting we're using discrete probabilities so we don't have to worry:)
- tnecniv 10y ago
  Good catch. The nuances of the continuum are many and subtle.

JohnStrange 10y ago

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.

tom_mellior 10y ago
> 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?
- JohnStrange 10y ago
  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.
  - tom_mellior 10y ago
    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.

joshcohen 10y ago

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.

eli_gottlieb 10y ago
How do you manage to claim that your computable logical inductor dominates the incomputable universal semimeasure?
- joshcohen 10y ago
  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.
  - tbt 10y ago
    This is right, but perhaps misleading; most of the properties are "asymptotic", meaning that they may take an extremely long time to hold, but they hold at finite times. For example, "provability induction" says that if you have a (polytime computable) sequence of sentences phi_n, all of which happen to be provable (possibly with fast-growing proof lengths), then P_n(phi_n) limits to 1. This means that on day n the logical inductor P is confident of phi_n, even though phi_n may take much longer than n steps to prove.
    - joshcohen 10y ago
      Although P_n can't be computed in anything like n steps.
      - tbt 10y ago
        Yeah. It's still surprising to me, though; P_n can predict extremely long-running computations, even ones with a much longer runtime than P_n, at least as well as any quickly computable "pattern". (The algorithm in the paper uses a (roughly) double-exponential-time algorithm to predict arbitrarily long-running programs, in a way that can't be improved upon by any polytime computable method.)

bbctol 10y ago

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

jey 10y ago
What is your definition of practical?
- bonoboTP 10y ago
  My concept of practical is stuff like: implementing things, doing experiments with prototypes, producing stuff that is imperfect but does something and can be improved upon. 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.
- jpt4 10y ago
  MIRI is entirely Blue Team - they work to create theoretical [0] safeguards on AI agents yet to be developed. I've long envisioned a counterpart Red Team that does nothing but build AIs that attempt to subvert these safety features, since the rest of the world of non Friendly AI [1] research is only unco-ordinated para-red behavior. [0] In the sense of "valid under these known precepts", not "speculative". [1] Non "Friendly AI", not "non-Friendly" AI.
  - gallabytes 10y ago
    I find that perception fairly surprising, as for a very long time it felt like we did more red team than blue team. I do acknowledge that this has been changing recently, but only significantly in the context of building on the results in this paper.
    - jpt4 10y ago
      Would you please direct me to an example of MIRI's Red Team efforts that isn't the recent "Malevolent AI" paper [0]? Adherence to the belief that UFAI is a threshold-grade existential risk seems to compel a "define first, delay implementation" strategy, lest any step forward be the irrevocable wrong one. [0] http://arxiv.org/abs/1605.02817 http://arxiv.org/abs/1605.02817

chriswarbo 10y ago

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