On March 25, 2023, I posted some speculations on how recent AI/ML improvements might be applied to create Metamath proofs. Like any hypothesis, experiments are necessary to see whether or not they're true. That said, I think good hypotheses are a helpful first step.
I have a few other notes & speculations. My hope is that these posts will inspire some of those experiments. See below for more. --- David A. Wheeler ======== First, there is a *lot* going on to make AI/ML technologies more widely available. For example, we have "OpenLLaMA: An Open Reproduction of LLaMA": https://github.com/openlm-research/open_llama That also includes efforts to make it easier to run these kinds of tools locally and/or on servers controlled by others. For example, WebGPU has been recently implemented by Chrome & Firefox is expected to release that soon. I expect that will make it easier to run machine learning algorithms, including on client-side JavaScript (where it might be possible to run an ML algorithm without having to install anything, just use your browser). I can' summarize it all, there's too much going on. If someone can point us to sites which are keeping track of this, or to key new results, that'd be awesome. Second, I think we should keep thinking about ways we could output Metamath proofs to make it easier for machine learning systems to learn how to create new proofs. I discussed a lot of that in my March 2023 post, such as presenting proofs "backwards" (start from the goal). One challenge is that most outputs include step numbers and step references. Those are challenging for an ML tool to figure out what the underlying relationship is, because it has to convert those numbers into "spatial" relationships that aren't obvious. For training purposes it might be best to do something else, thought it's not clear what. One option would be to omit step numbers, and for references use relative steps (+1). Or instead of step numbers, use reference names based on the label of the statement that uses. We could also add {...} to surround groups, to help the ML system learn groupings. Other ideas welcome. -- 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/F31053C1-966F-459B-9CC4-5945D8B81FFC%40dwheeler.com.
