3 ms·
> Machine learning may help in guiding theorem provers Interesting idea. There would be real upside where the machine learning system gets it right and guides
by MaxBarraclough 2y ago
> Machine learning may help in guiding theorem provers
Interesting idea. There would be real upside where the machine learning system gets it right and guides the prover to a valid proof, and little downside if it gets it wrong. (The prover won't derive an invalid proof, it will just fail to derive a valid one.) I don't think there are many applications of machine learning that have this property.
- eru 2y ago> (The prover won't derive an invalid proof, it will just fail to derive a valid one.) I don't think there are many applications of machine learning that have this property. Don't basically all applications of any heuristic solver to NP problems have this property? (Including problems that are only in NP, because they are also already in P.)
- MaxBarraclough 2y agoYes, sure, I could have phrased that better. There are no doubt many possible applications of the idea. The recent headline-grabbing applications of machine learning tend not to be like this.
- eru 2y agoYes, agreed. Though even amongst the recent-headline-grabbing stuff there are some areas that you can improve at by the equivalent of AlphaGo's self-play. Basically, when you have a slow and expensive option to use a weaker version of your system to produce better decisions / smarter data, and then use those to train the system.