Skip to yearly menu bar Skip to main content


Poster
in
Workshop: 2nd AI for Math Workshop @ ICML 2025

Target-Based Automated Conjecturing for Neural Theorem Proving

Marco Dos Santos · Albert Jiang · Wenda Li · Mateja Jamnik


Abstract:

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.

Chat is not available.