Hi Savas! > 1. Is your algorithm able to eventually prove any provable result given > enough time? In other words, is the proof search exhaustive?
Theoretically yes but with very low probability. > 2. Does it work for any metamath database or only for set.mm? We're not tied to set.mm in any way. I think we may have a few assumptions here and there (eg. we treat |- as a special symbol in some of our internal formats) but they can easily be removed. > I would also like to suggest some theorems for a test: if the answer to > question 2 is positive, you could try your algorithm on quantum logic (see > http://us2.metamath.org:88/qleuni/mmql.html) and intuitionistic logic (see > http://us2.metamath.org:88/ileuni/mmil.html). How large are the quantum logic and intuitionistic logic databases? What would be the main value of applying our proves on them out of curiosity? > 3. Does your prover use facts it learned from the training set or it uses > theorems from the database? I.e. if you were to change all theorem names in > the database so they are different from ones used in the training set, would > the model still work well? What if you "jumble" theorems (say, change order > in conjunctions of clauses), will the model work better than a usual search > or it will be ineffective? We don't rely on theorem names but statements. The statistical models do memoize specific formulations of theorems and we rely on set.mm at proof search to check that the theorem we apply are indeed part of the database, proven, and not appearing after the statement we're trying to prove. > 4. Related to previous questions, can you transfer skills the model learned > from one database to another? For instance, can it learn to prove > intuitionistic theorems faster if it was first trained on classical logic? Yes. > 5. Do you get (or hope to get) some sort of discriminative/generative model > as a byproduct? For example, given a trained model, can you evaluate the > probability that some proposition is true? Can you autosuggest possible > theorems/steps to use based on your model? Clearly this question has proof > assistants in mind :-) Yes. Not only theorems but also terms for unification as well (otherwise we wouldn't make much progress in Metamath/set.mm). Do you believe the community would be interested in an online tool to discharge goals? > As for set.mm, it would be interesting to see how it behaves on calculational > proofs like, for example, proofs that certain numbers are prime (see > http://us2.metamath.org:88/mpeuni/mmtheorems145.html#mm14463s). Another > interesting topic is proofs in the Tarskian geometry section (see > http://us2.metamath.org:88/mpeuni/mmtheorems237.html#mm23691h). Those mostly > use propositional calculus and Tarski axioms, which reduces the search space. > Geometric proofs also have some sort of "geometric intuition" behind them > which may (or may not) be helpful for finding proofs. The model is capable to prove some of the prime number theorems, but proofs sizes do grow very fast. I believe we already proved 17 as an example. Out of curiosity, why are you specifically interested in these two classes of theorems? Thanks! -stan On Mon, Mar 30, 2020 at 2:12 PM savask <[email protected]> wrote: > > Very interesting work, Stanislas! Great to see the cooperation between > classical AI (in the form of theorem provers) and modern machine learning. > > I have several questions which I hope you could comment on. > > 1. Is your algorithm able to eventually prove any provable result given > enough time? In other words, is the proof search exhaustive? > > 2. Does it work for any metamath database or only for set.mm? > > 3. Does your prover use facts it learned from the training set or it uses > theorems from the database? I.e. if you were to change all theorem names in > the database so they are different from ones used in the training set, would > the model still work well? What if you "jumble" theorems (say, change order > in conjunctions of clauses), will the model work better than a usual search > or it will be ineffective? > > 4. Related to previous questions, can you transfer skills the model learned > from one database to another? For instance, can it learn to prove > intuitionistic theorems faster if it was first trained on classical logic? > > 5. Do you get (or hope to get) some sort of discriminative/generative model > as a byproduct? For example, given a trained model, can you evaluate the > probability that some proposition is true? Can you autosuggest possible > theorems/steps to use based on your model? Clearly this question has proof > assistants in mind :-) > > I would also like to suggest some theorems for a test: if the answer to > question 2 is positive, you could try your algorithm on quantum logic (see > http://us2.metamath.org:88/qleuni/mmql.html) and intuitionistic logic (see > http://us2.metamath.org:88/ileuni/mmil.html). > > As for set.mm, it would be interesting to see how it behaves on calculational > proofs like, for example, proofs that certain numbers are prime (see > http://us2.metamath.org:88/mpeuni/mmtheorems145.html#mm14463s). Another > interesting topic is proofs in the Tarskian geometry section (see > http://us2.metamath.org:88/mpeuni/mmtheorems237.html#mm23691h). Those mostly > use propositional calculus and Tarski axioms, which reduces the search space. > Geometric proofs also have some sort of "geometric intuition" behind them > which may (or may not) be helpful for finding proofs. > > -- > 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/353a6707-14fd-4c08-a6e6-611972c84916%40googlegroups.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_0wjOyMFjW0%3DakrO_vcxsEAGVj007QmX6KRCYtgycR3vBA%40mail.gmail.com.
