Generative Language Modeling for Automated Theorem Proving

looking for the LLM's that have been big recently, there's GPT-f (https://arxiv.org/abs/2009.03393), Baldur (https://arxiv.org/abs/2303.04910), and COPRA (https://arxiv.org/abs/2310.04353), though currently these models don't seem as effective as the specialized non-LLM tools. In terms of using reinforcement learning to learn beyond human written proofs, there's TacticZero (https://openreview.net/forum?id=edmYVRkYZv), this paper from OpenAI (https://arxiv.org/pdf/2202.01344.pdf), rlCoP (https://arxiv.org/abs/1805.07563), the HOList line of work (https://arxiv.org/pdf/1905.10006.pdf), and HyperTree Proof Search (https://arxiv.org/abs/2205.11491), as well as some in progress work I'm working on with a team at the University of Massachusetts.

important to solve; GOFAI can push the boulders around perfectly, even though it would be unable to recognize a photograph of 'a boulder' or use the word 'boulder' in a story. Then you have the extensive hand-engineering of expert knowledge which goes into ascension agents and the symbolic winners, above and beyond merely plugging in a Sokoban solver. There are increasing experiments in making DRL agents exploit or initialize from pretrained language models (https://arxiv.org/abs/2005.07648#google https://arxiv.org/abs/2201.12122 https://arxiv.org/abs/2204.01691#google https://ai.stanford.edu/blog/DrRepair/ https://arxiv.org/abs/2005.07648#google https://arxiv.org/abs/2009.03393 https://arxiv.org/abs/2204.00598 come to mind) or reading manuals (https://arxiv.org/abs/1401.5390 all the way back in 2012!), and of course, a DRL agent can learn a tremendous amount without actually doing any playing by offline and off-policy and imitation learning, but while it is exciting and things like Gato look like the future, there is a long way to go from feeding in a dump of the Nethack wiki which mentions offhandedly "you can do X" to an agent recognizing an opportunity for X in the wild and executing it. (Which is something that symbolic approaches also don't come anywhere close to doing, because they just cheat by the capability being given to them by hand-engineering rather than having to autonomously read, understand, and apply.)

multiplication if you had to use BPEs, were never told how BPEs worked or corresponded to sane encodings, were basically never shown how to do multiplication, and were forced to do it without any working out. Quick, what's 542983 * 39486? No writing anything down, you have to output the numbers in order, and a single wrong digit is a fail. (That's easy mode, I won't even bother asking you to do BPEs.) ML models can learn multiplication, obviously they can learn multiplication, they just can't do it in this absurd adversarial context. GPT-f[1] was doing Metamath proofs on 9-digit division (again, a vastly harder context, they involve ~10k proof steps) with 50-50 accuracy, and we have a toy proof of concept[2] for straight multiplication. [1] https://arxiv.org/abs/2009.03393 [2] https://github.com/Thopliterce/transformer-arithmetic

you claim to be solving is not the one I was talking about, and not meaningfully more interesting. > The reason is that the space of all programs that can be computed by a Universal Turing Machine ("arbitrary") is infinite and any learner trying to find one of them blindly, without some kind of hint to guide it, would be lost for ever inside it. I'm not looking to solve arbitrary programs. I'm looking, at least at this first hurdle, to solve a few largely trivial ones. If you saw 100 examples, you would be able to solve this problem, or at least get very close. Therefore this sort of theoretical argument cannot hold. > By way of comparison, neural nets, with their hand-crafted architectures, minutely fine-tuned to specific domains or even particular datasets, cannot do that (e.g. a trained model can't be used as a feature to another neural net, in the way that ILP hypotheses can be used as BK). I assume you've seen GPT-f? (https://arxiv.org/abs/2009.03393) Section 4.7.1 shows this is entirely feasible for neural networks, though the technique is very different. Though I prefer even more the elegance (and general absurdity) of learning the bias by pretraining on WebMath (GitHub, arXiv Math, Math StackExchange). > The bottom line is that learning arbitrary programs from examples is a hard problem I agree it's hard, but in my mind this sentence completes to “and therefore our only hope is to use most powerful tool we have available, neural networks.”