4 ms·

SAT solvers, by far the greatest achievement of the Machine Reasoning / Symbolic camp (IMO), have an internal learning mechanism (CDCL) that is responsible for

SAT solvers, by far the greatest achievement of the Machine Reasoning / Symbolic camp (IMO), have an internal learning mechanism (CDCL) that is responsible for the incredible performance of SAT solvers on real-world use-cases. They somehow learn the structure of the problem. I've seen a SAT solver used to explore complex hardware designs and not only find all good alternatives but prove there were no others. Commercial Mixed Integer Programming solvers can optimize massive problems to provably global optimality very very quickly, and they too have an internal learning mechanism (cutting-planes). They excel at reasoning but they can only learn from the outcomes of the rules they are provided and how they interact, they cannot learn from data. With the advent of soft-constraints (which have an associated weight) I wonder if such systems could be adapted to learn probabilistic rules as well. Some existing systems (like AlphaGo) already combine symbolic approaches (Monte-Carlo Tree Search) with Deep Learning, but what I'm thinking about here goes beyond that.

YeGoblynQueenne 5y ago
I disagree. "By far the greatest achivement" of the symbolic camp is automated theorem proving, particularly the work on Resolution theorem-proving, that is also used in SAT solving as far as I know. But that's subjective, I suppose. Anyway I'm not an expert on SAT solving. Thank you for the perspective you provide with which I was unfamiliar. Edit: I don't think the OP meant SAT solvers when they said "symbolic learning"?
- sirwhinesalot 5y ago
  Indeed OP is not talking about SAT solvers, since SAT solvers don't "learn" from examples, at least not in the way OP is thinking (symbolic learning is an entirely separate field). SAT solvers, however, learn from their "mistakes", at least internally, which is really interesting and I think opens some very, very interesting research questions that as far as I know don't have that much money going into. For example, human brains can reason internally and learn in a similar manner, learning from "mistakes" of rule application in the same way (i.e. if I try to do this, then that fails, but if I do this other thing, then it works but not fully...). Just some food for thought. Automated Theorem Proving is also a very important success of the Symbolic camp but I would argue a less interesting one, since SAT solvers can do much more than prove theorems (and ATPs that can do more than prove theorems invariably use a SAT/SMT solver internally, like Vampire does for example). SAT solvers (and extensions) are used in model checkers, software and hardware verification tools, software and hardware synthesis tools, operations research, etc.
  - YeGoblynQueenne 5y ago
    I thought Vampire is resolution-based? Maybe the SAT/SMT-based one is more recent? One reason I think that theorem provers are more important than SAT solvers is that SLD-Resolution at least can be efficiently implemented. Also, Resolution can be used for induction, from examples and a background theory. That's a relatively recent result and you won't find a very clear account of it in the literature, but for instance, see here some early work: Meta-Interpretive Learning of Higher-Order Dyadic Datalog: Predicate Invention Revisited https://www.ijcai.org/Proceedings/13/Papers/231.pdf https://www.ijcai.org/Proceedings/13/Papers/231.pdf You have to unpick it from the language used but "meta-interpretive learning" means that it's based on a Prolog meta-interpreter, so an implementation of SLD(NF)-Resolution. And those "metarules" are really second-order definite clauses. The approach is really higher-order SLD-Resolution that turns out to be inductive, rather than deductive. But what you say about learning from "mistakes" reminded me of a rival approach, "Learning from Failures": Learning programs by learning from failures http://andrewcropper.com/pubs/popper.pdf http://andrewcropper.com/pubs/popper.pdf Which is, incidentally, implemented by means of SAT solvers (via ASP, ultimately). I'm more of a fan of the meta-interpretive approach (I study it), but I think the Popper paper might interest you, judging from your comment.
    - sirwhinesalot 5y ago
      Wonderful links, thank you so much. Vampire uses a portfolio of strategies, including the application of an SMT solver (Z3). This link goes into some detail: http://smt2019.galois.com/papers/tool_paper_20.pdf http://smt2019.galois.com/papers/tool_paper_20.pdf This is the most relevant bit for our conversation: > There are only two cases where Vampire can return sat: Firstly in UF and secondly, if Vampire produces a ground problem after preprocessing it may pass this problem to Z3 and report its result (possibly sat) directly. Essentially this refers to model building, i.e. solving existential problems. That's where SAT solvers excel. This includes producing counter-examples which are extremely useful in industry.
      - YeGoblynQueenne 5y ago
        Thanks for the clarifications! Happy reading :)

YeGoblynQueenne 5y ago

I disagree. "By far the greatest achivement" of the symbolic camp is automated theorem proving, particularly the work on Resolution theorem-proving, that is also used in SAT solving as far as I know. But that's subjective, I suppose. Anyway I'm not an expert on SAT solving. Thank you for the perspective you provide with which I was unfamiliar. Edit: I don't think the OP meant SAT solvers when they said "symbolic learning"?

sirwhinesalot 5y ago
Indeed OP is not talking about SAT solvers, since SAT solvers don't "learn" from examples, at least not in the way OP is thinking (symbolic learning is an entirely separate field). SAT solvers, however, learn from their "mistakes", at least internally, which is really interesting and I think opens some very, very interesting research questions that as far as I know don't have that much money going into. For example, human brains can reason internally and learn in a similar manner, learning from "mistakes" of rule application in the same way (i.e. if I try to do this, then that fails, but if I do this other thing, then it works but not fully...). Just some food for thought. Automated Theorem Proving is also a very important success of the Symbolic camp but I would argue a less interesting one, since SAT solvers can do much more than prove theorems (and ATPs that can do more than prove theorems invariably use a SAT/SMT solver internally, like Vampire does for example). SAT solvers (and extensions) are used in model checkers, software and hardware verification tools, software and hardware synthesis tools, operations research, etc.
- YeGoblynQueenne 5y ago
  I thought Vampire is resolution-based? Maybe the SAT/SMT-based one is more recent? One reason I think that theorem provers are more important than SAT solvers is that SLD-Resolution at least can be efficiently implemented. Also, Resolution can be used for induction, from examples and a background theory. That's a relatively recent result and you won't find a very clear account of it in the literature, but for instance, see here some early work: Meta-Interpretive Learning of Higher-Order Dyadic Datalog: Predicate Invention Revisited https://www.ijcai.org/Proceedings/13/Papers/231.pdf https://www.ijcai.org/Proceedings/13/Papers/231.pdf You have to unpick it from the language used but "meta-interpretive learning" means that it's based on a Prolog meta-interpreter, so an implementation of SLD(NF)-Resolution. And those "metarules" are really second-order definite clauses. The approach is really higher-order SLD-Resolution that turns out to be inductive, rather than deductive. But what you say about learning from "mistakes" reminded me of a rival approach, "Learning from Failures": Learning programs by learning from failures http://andrewcropper.com/pubs/popper.pdf http://andrewcropper.com/pubs/popper.pdf Which is, incidentally, implemented by means of SAT solvers (via ASP, ultimately). I'm more of a fan of the meta-interpretive approach (I study it), but I think the Popper paper might interest you, judging from your comment.
  - sirwhinesalot 5y ago
    Wonderful links, thank you so much. Vampire uses a portfolio of strategies, including the application of an SMT solver (Z3). This link goes into some detail: http://smt2019.galois.com/papers/tool_paper_20.pdf http://smt2019.galois.com/papers/tool_paper_20.pdf This is the most relevant bit for our conversation: > There are only two cases where Vampire can return sat: Firstly in UF and secondly, if Vampire produces a ground problem after preprocessing it may pass this problem to Z3 and report its result (possibly sat) directly. Essentially this refers to model building, i.e. solving existential problems. That's where SAT solvers excel. This includes producing counter-examples which are extremely useful in industry.
    - YeGoblynQueenne 5y ago
      Thanks for the clarifications! Happy reading :)