Adding some comments on top of Mario's: >> Trying to find such a chain of substitution rules is essentially a tree >> search problem. If there are N theorems in the database then to answer the >> latter question comes down to searching a tree of size N^L. Is that somewhat >> right? > > This is a slightly overly restricted setting. You probably want to be able to > add new theorems to the database and then use them to compress future proofs. > That means that the branching factor can grow over time, roughly (N+L)^L if > we say that adding a theorem counts as a step. This is actually how > DreamCoder works (https://arxiv.org/abs/2006.08381), you should take a look.
There are also the substitutions. Not all substitutions are bound by the requirement to unify to the conclusion, eg modus ponens. Then either you discard these proof steps (and I presume we have theoretical results on this that show that it's possible to prove things that way but your proof size explodes?) or you keep them and your search space becomes enumerable at each step (assuming no restriction on the length of the proof step which in practice you would have, but it's still prohibitively huge even for one step). Hence the motivation to use a language model such that we can sample possible next steps from it and use that list as the branching for each step in our search tree. I call these unbound substitutions or terms required in proofs, "exogenous terms" (haven't found a standard name for them?); Being capable of generating those is again a core motivation of GPT-f. The consequence is that the search tree is not "complete" and you can't just get to a proof by searching forever. But the hope is that as the language model gets better it is powerful enough to cover the search space properly yet keeping it small enough to be practical. >> Is it true that any AI system built on metamath will need these same >> foundations? For instance it will need a parser for the database, a verifier >> and also it will need a function which: for any statement returns the >> possible substitutions/theorems which could be applied. Generally speaking you definitely need an "interactive" verifier (which includes, for Metamath, a parser for the grammar defined by the database). I don't think you necessarily need a system that mechanically proposes possible substitutions, as an example with GPT-f we let the model do that work. For other approaches based on ranking possible actions, having something that proposes actions is definitely useful. Hope it's useful. Happy to answer any specific questions about GPT-f and how we interface to Metamath. -stan On Wed, Jun 9, 2021 at 10:45 PM Mario Carneiro <[email protected]> wrote: > > > > On Wed, Jun 9, 2021 at 11:21 AM Jon P <[email protected]> wrote: >> >> There have been a couple of AI systems, gpt-f and Holophrasm, built on >> metamath whose aim is to generate proofs. Are there more I’m not aware of? > > > Not that I know of, at least for metamath. There are other systems in other > languages: GPT-f also has a lean version, HOList works for HOL light, > Tactician is a Coq-based ML architecture, and there are several others that > don't immediately come to mind. > >> The question “Is there a proof of any length which proves this proposition” >> is in the same complexity class as the halting problem I think. Whereas “Is >> there a proof of length less than L steps which proves the proposition” is >> NP-complete, so is easier to tackle I think. > > > Technically, L has to be written in unary for it to be NP-complete. If you > write it normally then it is NEXPTIME. > . >> >> Trying to find such a chain of substitution rules is essentially a tree >> search problem. If there are N theorems in the database then to answer the >> latter question comes down to searching a tree of size N^L. Is that somewhat >> right? > > > This is a slightly overly restricted setting. You probably want to be able to > add new theorems to the database and then use them to compress future proofs. > That means that the branching factor can grow over time, roughly (N+L)^L if > we say that adding a theorem counts as a step. This is actually how > DreamCoder works (https://arxiv.org/abs/2006.08381), you should take a look. > >> >> So does this mean, in the abstract, given enough hardware and time you could >> find all proofs of length less than L just by brute force search? > > > Yes. A proof of length L is a string, and there are only finitely many > strings of that length. Just verify them all and see if one checks. > >> I am also interested in what the true branching factor is. For instance not >> all N theorems in the database can be applied to all hypotheses, only a >> subset can be. How much is the reduction? Can most theorems be applied to >> most statements or is it that only a very small subset can? Moreover I guess >> there is a reduction because it is sufficient to find only one proof whereas >> there will be many for any provable statement. > > > There are quite a few theorems, like ax-mp, that apply on any goal state, so > the branching factor is always at least as many as the number of theorems > that conclude with |- ph. But it's true that most lemmas are not like this. > Worse, one of ax-mp's hypotheses is |- ps where ps is unrelated to ph, which > means that you can apply literally any theorem T in set.mm to the current > goal in two steps, by using ax-mp and then T in the minor premise. So the > average branching factor is at least sqrt(N) where N is the number of > theorems in the database. > >> Is it true that any AI system built on metamath will need these same >> foundations? For instance it will need a parser for the database, a verifier >> and also it will need a function which: for any statement returns the >> possible substitutions/theorems which could be applied. > > > No. The brute force search method just described is not practical above about > 15 steps or so. It has been used for parts of > http://us.metamath.org/mmsolitaire/pmproofs.txt but it runs out of steam even > before the end of that list. > > Most theorem provers are ultimately doing tree search, but the tree being > searched may not literally be the tree of substitutions mentioned. For > example they might instead use tactics (proof producing programs) as building > blocks and tree search a way to fit them together. This method may not be > complete, and may not produce the shortest proof, but it can eliminate a lot > of the excess branching factor in the naive method. > >> >> Is there any value in us (I don’t know if anyone would be interested in >> working on this) gathering some programs which already do this or writing >> some new code in a nice optimised way? For example in MineRL, a minecraft AI >> challenge, they provide an environment which offers the agent the state of >> the game and a list of options available to it. Maybe some sort of >> environment like this for metamath would help encourage people to tackle the >> AI side of these problems? > > > set.mm is already a fairly good source for hand-optimized proofs, since this > has been a running goal for a while. You should talk to the gpt-f folks about > a metamath-based gym environment; I think they already have something like > that. > >> Another question I have is how much can be done with optimised code, or >> multithreading, or gpu parallelisation? For instance the unify command in >> MMJ2 presumably is searching for all possible proofs of length 1 to fill in >> a gap? Could something like this be optimised to run in the background on >> other threads on the cpu so it could fill in 2, 3, or more steps for you? >> Would this be a powerful thing to add to a proof assistant, a brute force >> solver which is always trying to help? If a gpu optimised parallel search >> could be performed on a large amount of hardware might it be able to >> actually generate some reasonable length proofs? > > > Certainly bigger small-scale brute force search is useful for proof authors. > Smarter search is also useful. Unfortunately, most proof activities are not > well-suited to GPU parallelism because it is a very discrete and nonlinear > problem (as you already mentioned, not unlike the halting problem) and it's > hard to find a piece of it that looks like "do the same thing to these 1000 > data elements". Multithreading is fine though, you can have this stuff > running in the background on other CPUs. > >> Finally for the general AI problem presumably if any kind of mild heuristic >> could be found then it might be possible to generate proofs much more >> efficiently? I think that’s what the above systems are doing, if I have >> understood correctly, is given a list of possible substitutions to prefer >> some other overs as more likely to lead in the right direction? Their hope >> is that the Neural Networks can develop some sort of intuition. > > > Yes, neural network based tree search builds heuristics for how promising the > goal state looks like, so that silly things like applying ax-mp many times in > a row are rejected for generating too many goals. You can still improve on > this by giving the neural network human level steps to be able to work with: > for example not requiring that the NN fills in substitutions and just give > theorem names with the substitutions being handled by unification. > >> In terms of finding a heuristic there is some interesting work here which >> might apply. The basic idea, as applied to metamath, would be to use some >> variant of word2vec to embed all the statements in the database into a high >> dimensional (say 100) vector space. Then when searching the tree of possible >> proofs statements could be evaluated based on whether they were leading >> closer to the hypotheses or not. Might this approach have any value here? Is >> anyone interested in it? Are there other ways of generating a heuristic to >> help with search? > > > GPT-f is a transformer, but previous methods like Holophrasm and HOList are > based on a tree embedding of the formulas. You kind of have to do this > because NNs work on a finite dimensional latent space. > > Mario > > -- > You received this message because you are subscribed to the Google Groups > "Metamath" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to [email protected]. > To view this discussion on the web visit > https://groups.google.com/d/msgid/metamath/CAFXXJSuy4Cm%2BXwo%2Bn%3DiziRJ0hVJH34kgmBvrReJd2RK4KSWLHw%40mail.gmail.com. -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CACZd_0x7P_i%2B%2B%2B9xU_%2B9i6U0nJ2U7NW6oczemMQb0Ng0hwt7_w%40mail.gmail.com.
