Target-Based Automated Conjecturing for Neural Theorem Proving

Neural theorem proving models often struggle with hard problems, in part due to the lack of training examples. We introduce a novel approach to automated conjecturing that increases the amount of training examples by generating conjectures specifically tailored to a target set of difficult problems.Our method is an evolutionary algorithm in which a conjecturer iteratively proposes new conjectures, guided by feedback on how much they help a prover make progress on the target set. Conjectures that most effectively enhance the prover's performance become seeds for the next iteration.We demonstrate that this approach significantly enhances the prover's performance on hard problems, with preliminary results showing an increase in proof success rate from 4% to 18% on a target set of complex number problems after only two iterations.