Proposal: Expert Iteration for Machine Learning Based Theorem Provers via Complexity Minimization

We present a research proposal for employing position evaluators to improve tactic prediction in theorem proving. We propose to train a position evaluator to predict proof length, using this to effectively train a tactic predictor to select tactics that result in shorter proofs, and thus, enhance the tactic selection process.
Additionally, we conjecture that position evaluators can be utilized to guide proof search. We will evaluate our models using the CoqGym dataset.
We plan to do this with continual learning as via expert iteration, refining the model's performance over time and data set.
In this context, we propose to view Expert Iteration as alternating maximization and a meta-learning algorithm.