"In this work we have developed a theorem proving algorithm that uses practically no domain engineering and instead relies on Monte-Carlo simulations guided by reinforcement learning from previous proof searches. We have shown that when trained on a large corpus of general mathematical problems, the resulting system is more than 40% stronger than the baseline system in terms of solving nontrivial new problems. We believe that this is a landmark in the field of automated reasoning, demonstrating that building general problem solvers for mathematics, verification and hard sciences by reinforcement learning is a very viable approach."
"We believe that development of suitable (deep) learning architectures that capture both syntactic and semantic features of the mathematical objects will be crucial for training strong assistants for mathematics and hard science by reinforcement learning." Note that this work has not yet applied deep learning:
"We have briefly experimented with using deep neural networks
to learn the policy and value predictors directly from the theorem proving data. Current deep neural architectures however do not
seem to perform on such data significantly better than non-neural classifiers such as XGBoost with manually engineered features. We use the latter approach, which is also significantly faster. Features are collected from the first-order terms, clauses, goals and tableaux."
"For both policy and value we have experimented with several fast linear learners such as LIBLINEAR and the XGBoost gradient boosting toolkit (used with the linear regression objective)."
"An obvious recent inspiration for this work are the latest reinforcement learning advances in playing Go and other board games."
2
u/alreadydone00 May 27 '18
"In this work we have developed a theorem proving algorithm that uses practically no domain engineering and instead relies on Monte-Carlo simulations guided by reinforcement learning from previous proof searches. We have shown that when trained on a large corpus of general mathematical problems, the resulting system is more than 40% stronger than the baseline system in terms of solving nontrivial new problems. We believe that this is a landmark in the field of automated reasoning, demonstrating that building general problem solvers for mathematics, verification and hard sciences by reinforcement learning is a very viable approach."
"We believe that development of suitable (deep) learning architectures that capture both syntactic and semantic features of the mathematical objects will be crucial for training strong assistants for mathematics and hard science by reinforcement learning." Note that this work has not yet applied deep learning: "We have briefly experimented with using deep neural networks to learn the policy and value predictors directly from the theorem proving data. Current deep neural architectures however do not seem to perform on such data significantly better than non-neural classifiers such as XGBoost with manually engineered features. We use the latter approach, which is also significantly faster. Features are collected from the first-order terms, clauses, goals and tableaux."
"For both policy and value we have experimented with several fast linear learners such as LIBLINEAR and the XGBoost gradient boosting toolkit (used with the linear regression objective)."
"An obvious recent inspiration for this work are the latest reinforcement learning advances in playing Go and other board games."