4 ms·

it's interesting that he says that proving a mathematical theorem would be a bigger milestone. from my limited perspective, that seems less surprising than get

it's interesting that he says that proving a mathematical theorem would be a bigger milestone. from my limited perspective, that seems less surprising than getting language models of GPT-3 quality. There are already theorem proving environments like Lean, HOL, and Coq. Proving theorems in these systems is essentially just a kind of guided tree search - you're trying to reach a goal state by choosing from a finite menu of "tactics", and might have to backtrack. There is nascent research in this area already; it works but hasn't proved any significant theorems. But from what I've read this might be partly because most "interesting" mathematics can't yet be formally expressed in a theorem prover. Eventually mathematicians will build out the libraries of mathematical objects in those languages such that it's possible to state an interesting theorem; then it seems like people are already very good at combining neural nets with tree search to surpass human capabilities.

xiphias2 6y ago
Effective automatic theorem proving would make software much safer as well. Right now it's too much time to bother verifying so much code, even if somebody would be capable of doing it.
oggy 6y ago
AI can be very useful in practice for theorem proving WITHOUT proving "big new theorems" or inventing new mathematics. Right now, what makes theorem proving an extremely expensive undertaking is making proof search work. AI could help immensely by improving the search. The process of proving things in provers like Lean, HOL or Coq is interactive; roughly, the theorem you want to prove is your starting goal, and you apply tactics to transform the proof goal until the goal becomes the boolean value true. The Platonic ideal of this process is that you provide the main, "creative" steps of the goal transformation, and the tactics discharge the rest automatically. In practice, however, for the process to work, you need to carefully state your theorems in a certain way, and you need an enormous amount of tacit knowledge about how the internals of the tactics, as well as of the libraries of already proved facts that you can use. These things take years of practice to build up. I think it unlikely that theorem provers will see a significant uptake until the tactics (i.e., proof search) improve massively. This is where I hope AI could step in. There are many challenges, obviously. The training data sets are relatively modest; when I looked a few years ago, the publicly available Isabelle theories, for example, amounted to a few hundred thousand proved theorems, which is a minuscule corpus compared to what something like GPT-3 uses. Then, how do you represent the input, just characters, or do you need more structure? Can you can leverage something like reinforcement learning? How do you could set the training process up? On the other hand, compared to chat bots, the quality of the resulting AI system would be much easier to quantify (success rate on a benchmark of new theorems). There's already work in this area, but I'm not aware of any grand successes yet. I hope to see much more work on this in the near future. I've been dabbling in it myself a while ago while I was still in academia, but other priorities have taken precedence in the past couple of years.

xiphias2 6y ago

Effective automatic theorem proving would make software much safer as well. Right now it's too much time to bother verifying so much code, even if somebody would be capable of doing it.

oggy 6y ago

AI can be very useful in practice for theorem proving WITHOUT proving "big new theorems" or inventing new mathematics. Right now, what makes theorem proving an extremely expensive undertaking is making proof search work. AI could help immensely by improving the search. The process of proving things in provers like Lean, HOL or Coq is interactive; roughly, the theorem you want to prove is your starting goal, and you apply tactics to transform the proof goal until the goal becomes the boolean value true. The Platonic ideal of this process is that you provide the main, "creative" steps of the goal transformation, and the tactics discharge the rest automatically. In practice, however, for the process to work, you need to carefully state your theorems in a certain way, and you need an enormous amount of tacit knowledge about how the internals of the tactics, as well as of the libraries of already proved facts that you can use. These things take years of practice to build up. I think it unlikely that theorem provers will see a significant uptake until the tactics (i.e., proof search) improve massively. This is where I hope AI could step in. There are many challenges, obviously. The training data sets are relatively modest; when I looked a few years ago, the publicly available Isabelle theories, for example, amounted to a few hundred thousand proved theorems, which is a minuscule corpus compared to what something like GPT-3 uses. Then, how do you represent the input, just characters, or do you need more structure? Can you can leverage something like reinforcement learning? How do you could set the training process up? On the other hand, compared to chat bots, the quality of the resulting AI system would be much easier to quantify (success rate on a benchmark of new theorems). There's already work in this area, but I'm not aware of any grand successes yet. I hope to see much more work on this in the near future. I've been dabbling in it myself a while ago while I was still in academia, but other priorities have taken precedence in the past couple of years.