Re:Deep learning is hitting a wall?
by sirwhinesalot on Thursday March 10, 2022 @01:32PM
(#30630567)
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
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.
Re:Deep learning is hitting a wall?
by YeGoblynQueenne on Thursday March 10, 2022 @02:31PM
(#30631346)
Thanks for the clarifications! Happy reading :)
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
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
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.