Graph Representations for Higher-Order Logic and Theorem Proving (2019)
1–10 of 16 posts
Re: Graph Representations for Higher-Order Logic and Theorem Proving (2019)
#2I wonder why they don't mention any work based on transformer architectures? The recent work on solving differential equations based on expressions in reverse polish notation seemed like a reasonable idea to apply to theorem proving as well.
Really cool work though!
Re: Graph Representations for Higher-Order Logic and Theorem Proving (2019)
#3I wonder why they don't mention any work based on transformer architectures? The recent work on solving differential equations based on expressions in reverse polish notation seemed like a reasonable idea to apply to theorem proving as well. Really cool work though!
A transformer is unable to really represent logic, let alone higher order logic and theorem proving.
Re: Graph Representations for Higher-Order Logic and Theorem Proving (2019)
#4I wonder why they don't mention any work based on transformer architectures? The recent work on solving differential equations based on expressions in reverse polish notation seemed like a reasonable idea to apply to theorem proving as well. Really cool work though!
A transformer is unable to really represent logic, let alone higher order logic and theorem proving.
Where can I read more about this?
Re: Graph Representations for Higher-Order Logic and Theorem Proving (2019)
#5I wonder why they don't mention any work based on transformer architectures? The recent work on solving differential equations based on expressions in reverse polish notation seemed like a reasonable idea to apply to theorem proving as well. Really cool work though!
This is the differential equations paper I was thinking about https://medium.com/analytics-vidhya/solving-differential-equ...
Re: Graph Representations for Higher-Order Logic and Theorem Proving (2019)
#6I wonder why they don't mention any work based on transformer architectures? The recent work on solving differential equations based on expressions in reverse polish notation seemed like a reasonable idea to apply to theorem proving as well. Really cool work though!
Solving differential equations symbolically[^1] is a classic pattern matching problem though. It takes a lot of practice recognising which equations can be solved with which method/heuristic, but in the end, the available heuristics are somewhat limited in number and so it's not unreasonable that an ML model would perform well here. Notice that you will still need to actually check your result in some way or the other, because ML models can generate false positives and you really don't want that in maths; so it's not that you're replacing rule-based systems, you're just augmenting them with other approaches (and of course, verifying the solution to a differential equation is basically a solved problem in symbolic analysis, since taking derivatives is a simple rule-based procedure[^2]).
I think theorem proving is much different. The space of possible heuristics you may apply to a proof is basically infinite. It can take a tremendous amount of creativity and intuition to come up with a complicated and novel proof. While I can see ML models being of use for simpler proofs or lemmas within bigger proofs (such as simple epsilon-delta proofs etc.), I have a hard time imagining that they will really be able to do real proofs anytime soon.
[^1]: I emphasise "symbolically" because it is my understanding that outside of simple situations and university lectures, most people don't bother with that, instead solving differential equations numerically.
[^2] There are some subtleties around the fact that, afaik, deciding whether two expressions are equal is undecidable in the general case because at some point you will have to compare e.g. coefficients and the equality of real numbers is undecidable. In practice, you will consider two numbers to be equal if their difference is below a certain threshold, which could in theory also yield false positives, but I find it unlikely that this would occur in practice in the situation of solving an equation.
Re: Graph Representations for Higher-Order Logic and Theorem Proving (2019)
#7I wonder why they don't mention any work based on transformer architectures? The recent work on solving differential equations based on expressions in reverse polish notation seemed like a reasonable idea to apply to theorem proving as well. Really cool work though!
Solving differential equations symbolically[^1] is a classic pattern matching problem though. It takes a lot of practice recognising which equations can be solved with which method/heuristic, but in the end, the available heuristics are somewhat limited in number and so it's not unreasonable that an ML model would perform well here. Notice that you will still need to actually check your result in some way or the othe…
I think they can use transformer in the same way for proof path generation: do pattern matching for complex logical statements to find those where specific rule can be applied, similarly as it has be done in differential equations paper.
Re: Graph Representations for Higher-Order Logic and Theorem Proving (2019)
#8It looks like Graph NNs are going places.
Re: Graph Representations for Higher-Order Logic and Theorem Proving (2019)
#9I wonder why they don't mention any work based on transformer architectures? The recent work on solving differential equations based on expressions in reverse polish notation seemed like a reasonable idea to apply to theorem proving as well. Really cool work though!
A transformer is unable to really represent logic, let alone higher order logic and theorem proving.
A transformer is a universal function approximator. The question is whether it can do so reasonably efficiently. Trained on natural language linear sequences, I’m with you. Trained on abstract logical graph representations? I don’t think that question’s answered yet, unless I’m missing something.
Re: Graph Representations for Higher-Order Logic and Theorem Proving (2019)
#10Earlier quoted context omitted.
A transformer is unable to really represent logic, let alone higher order logic and theorem proving.
A transformer is a universal function approximator. The question is whether it can do so reasonably efficiently. Trained on natural language linear sequences, I’m with you. Trained on abstract logical graph representations? I don’t think that question’s answered yet, unless I’m missing something.
How do transformers handle with truth tables, logical connectives, and propositional logic / rules of inference, and first-order logic?
Truth table: https://en.wikipedia.org/wiki/Truth_table
Logical connective: https://en.wikipedia.org/wiki/Logical_connective
Propositional logic: https://en.wikipedia.org/wiki/Propositional_calculus
Rules of inference: https://en.wikipedia.org/wiki/Rule_of_inference
DL: Description logic: https://en.wikipedia.org/wiki/Description_logic (... The OWL 2 profiles (EL, QR, RL; DL, Full) have established decideability and complexity: https://www.w3.org/TR/owl2-profiles/ )
FOL: First-order logic: https://en.wikipedia.org/wiki/First-order_logic
HOL: Higher-order logic: https://en.wikipedia.org/wiki/Higher-order_logic
In terms of regurgitating without critical reasoning?
Critical reasoning: https://en.wikipedia.org/wiki/Critical_thinking