17 ms·

Notice that 2018 winner in LTB category is MaLARea 0.6, NN-based theorem prover. History repeats itself. Programs, which use hand-crafted heuristics, compete w

Notice that 2018 winner in LTB category is MaLARea 0.6, NN-based theorem prover. History repeats itself. Programs, which use hand-crafted heuristics, compete with NN-based programs for a time and then they are left behind. Like Stockfish and Leela Zero.

YeGoblynQueenne 6y ago
MaLARea won a single category in two years, out of 11 categories in a competition running since 1996 (though not all categories were used each year). Furthermore, there were five other winners in the same category since the first entry of MaLARea. I think your enthusiasm is a little premature.
- red75prime 6y ago
  It's just an observation that handcrafted heuristics, which are required to mitigate combinatorial explosion, time after time give way to heuristics produced by machine learning. Haar cascades, various OCR techniques, rule-based translation, chess heuristics for alpha-beta search, pre NN speech recognition techniques etc.
  - YeGoblynQueenne 6y ago
    I'm not sure I like the "heuristics" terminology with respect to machine learning, but let's agree to it, for simplicity. Now, in automated theorem proving (ATP hence) there aren't only heuristics. For example, the resolution rule (used by the Vampire theorem prover) is not a heuristic, but an inference rule that comes with soundness and completeness results. It's what I would call a principled choice, i.e. one fully justified by theory. As to combinatorial explosion, in resolution that is not mitigated by heuristics, but by restricting the problem, e.g. to definite logic programs, etc. See, the problem with ATP is not that we don't know good ways to perform ATP tasks- we do. We have very good algorithms that do that kind of thing. Algorithms that come with theoretical guarantees of optimality. Complexity results. Soundness and completenes results. Decidability results. All that jazz. So there is no real reason to look for approximations of the same algorithms, as might be learned by a neural network- because, why approximate something for which you already have a precise definition? The real problem with ATP is the huge, unmanageable size of the hypothesis spaces - and the many negative rersults, e.g. of the undecidability of arbitrary first order logic languages, etc. These are not even efficiency problems that can really be addressed by better algorithms, or heuristics- they're fundamental problems associated with having finite resources, in a universe with finite time and having to explore an infinite domain. These are not the kinds of problems one solves by throwing a lot of data at an optimisation procedure. Contrast this with chess. The search space for chess moves is finite, though large. We don't have a principled "solution" for chess, like a closed-form solution, or an inference rule- just some search procedures guided by heuristics (minimax and its ilk, including MCTS). Here, an approximation is a good alternative, because really that's all we've been able to do so far. In ATP on the other hand, there are principled solutions and we don't have to rely on heuristics and approximations. So, one has no reason to expect that neural nets can do well in ATP just because they've done well in chess. As to the observation that neural nets have done well in diverse domains, here there's a bit of a survivorship bias at play I think, because for example, neither you nor me really are in a position to know in how many domains neural nets have been applied and didn't do so well, because that kind of work never sees the light of day- unlike the success stories, like chess or Go. So again you can't make very good predictions by looking at what has gone before. In any case, who knows. I might have to eat my words at some point. Never say never and all that. EDIT: Sorry about this part of my earlier comment: "I think your enthusiasm is a little premature." Re-reading it, it comes across as snarky and dismissive. That was not my intention, or if it was at the time of writing, I regret it.

YeGoblynQueenne 6y ago

MaLARea won a single category in two years, out of 11 categories in a competition running since 1996 (though not all categories were used each year). Furthermore, there were five other winners in the same category since the first entry of MaLARea. I think your enthusiasm is a little premature.

red75prime 6y ago
It's just an observation that handcrafted heuristics, which are required to mitigate combinatorial explosion, time after time give way to heuristics produced by machine learning. Haar cascades, various OCR techniques, rule-based translation, chess heuristics for alpha-beta search, pre NN speech recognition techniques etc.
- YeGoblynQueenne 6y ago
  I'm not sure I like the "heuristics" terminology with respect to machine learning, but let's agree to it, for simplicity. Now, in automated theorem proving (ATP hence) there aren't only heuristics. For example, the resolution rule (used by the Vampire theorem prover) is not a heuristic, but an inference rule that comes with soundness and completeness results. It's what I would call a principled choice, i.e. one fully justified by theory. As to combinatorial explosion, in resolution that is not mitigated by heuristics, but by restricting the problem, e.g. to definite logic programs, etc. See, the problem with ATP is not that we don't know good ways to perform ATP tasks- we do. We have very good algorithms that do that kind of thing. Algorithms that come with theoretical guarantees of optimality. Complexity results. Soundness and completenes results. Decidability results. All that jazz. So there is no real reason to look for approximations of the same algorithms, as might be learned by a neural network- because, why approximate something for which you already have a precise definition? The real problem with ATP is the huge, unmanageable size of the hypothesis spaces - and the many negative rersults, e.g. of the undecidability of arbitrary first order logic languages, etc. These are not even efficiency problems that can really be addressed by better algorithms, or heuristics- they're fundamental problems associated with having finite resources, in a universe with finite time and having to explore an infinite domain. These are not the kinds of problems one solves by throwing a lot of data at an optimisation procedure. Contrast this with chess. The search space for chess moves is finite, though large. We don't have a principled "solution" for chess, like a closed-form solution, or an inference rule- just some search procedures guided by heuristics (minimax and its ilk, including MCTS). Here, an approximation is a good alternative, because really that's all we've been able to do so far. In ATP on the other hand, there are principled solutions and we don't have to rely on heuristics and approximations. So, one has no reason to expect that neural nets can do well in ATP just because they've done well in chess. As to the observation that neural nets have done well in diverse domains, here there's a bit of a survivorship bias at play I think, because for example, neither you nor me really are in a position to know in how many domains neural nets have been applied and didn't do so well, because that kind of work never sees the light of day- unlike the success stories, like chess or Go. So again you can't make very good predictions by looking at what has gone before. In any case, who knows. I might have to eat my words at some point. Never say never and all that. EDIT: Sorry about this part of my earlier comment: "I think your enthusiasm is a little premature." Re-reading it, it comes across as snarky and dismissive. That was not my intention, or if it was at the time of writing, I regret it.