4 ms·

> exceptional guesser Considering neural networks are inherently maximizing probabilities and statistical descriptions of data, this should come as no surprise

by uoaei 6y ago

> exceptional guesser Considering neural networks are inherently maximizing probabilities and statistical descriptions of data, this should come as no surprise. This work has not dissolved the dichotomy between rules-based and statistical methods, but rather transmuted the syntax of rules-based expressions into a representation that can be exploited by statistical machines in a way that makes "guessing" more fruitful. There are some examples near the end of the paper showing how the authors take an initially intractable expression and are able to simplify it with their approach so that Mathematica can actually perform the integral for them. It seems much more appropriate to market this method as a preprocessor for massive expressions to a more chewable size.

sdenton4 6y ago
> exceptional guesser This IMO describes how mathematics itself moves forward... A matematician is an extremely well-trained 'guesser' who is also able to sink a lot of time into formal verification. The process is essentially: a) Find an interesting conjecture that you've got a strong guess to be true. b) Check for obvious (or less obvious) counterexamples, or conflicting theorems. c) Prove the thing is true. A large part of the art of being a working mathematician is in part (a): you need to make a really good guess. An ideal conjecture is correct AND proveable AND leads to other interesting results, or says interesting things about bigger problems. So what happens when we apply really good versions of current AI to this area? Picking out an 'interesting' conjecture is still Strong-AI-Complete: it requires lots of domain knowledge, and an understanding of what this particular conjecture would 'unlock.' But we could perhaps come up with good 'guessers' which quickly tell us whether a given idea might work out, perhaps saving a bunch of effort. Perhaps we could even get to the point of generating a proposed proof which can be fed to an automated proof checking system, allowing for inspection and modification by the human in the loop.

by uoaei 6y ago

sdenton4 6y ago

> exceptional guesser This IMO describes how mathematics itself moves forward... A matematician is an extremely well-trained 'guesser' who is also able to sink a lot of time into formal verification. The process is essentially: a) Find an interesting conjecture that you've got a strong guess to be true. b) Check for obvious (or less obvious) counterexamples, or conflicting theorems. c) Prove the thing is true. A large part of the art of being a working mathematician is in part (a): you need to make a really good guess. An ideal conjecture is correct AND proveable AND leads to other interesting results, or says interesting things about bigger problems. So what happens when we apply really good versions of current AI to this area? Picking out an 'interesting' conjecture is still Strong-AI-Complete: it requires lots of domain knowledge, and an understanding of what this particular conjecture would 'unlock.' But we could perhaps come up with good 'guessers' which quickly tell us whether a given idea might work out, perhaps saving a bunch of effort. Perhaps we could even get to the point of generating a proposed proof which can be fed to an automated proof checking system, allowing for inspection and modification by the human in the loop.