Lemmanaid: Neuro-Symbolic Lemma Conjecturing
This work addresses the challenge of lemma conjecturing for automated reasoning tools and formal mathematics, facilitating computer-assisted theory development, though it is incremental as it builds on existing neural and symbolic approaches.
The authors tackled the problem of automatically generating useful lemmas for automated reasoning and formal mathematics by developing Lemmanaid, a neuro-symbolic tool combining LLMs and symbolic methods, which discovered 29-39.5% of human-written lemmas in Isabelle proof libraries, outperforming neural-only methods by 8-15%.
Automatically conjecturing useful, interesting and novel lemmas would greatly improve automated reasoning tools and lower the bar for formalizing mathematics in proof assistants. It is however a very challenging task for both neural and symbolic approaches. We present the first steps towards a practical neuro-symbolic lemma conjecturing tool, Lemmanaid, that combines Large Language Models (LLMs) and symbolic methods, and evaluate it on proof libraries for the Isabelle proof assistant. We train an LLM to generate lemma templates that describe the shape of a lemma, and use symbolic methods to fill in the details. We compare Lemmanaid against an LLM trained to generate complete lemma statements as well as previous fully symbolic conjecturing methods. Lemmanaid outperforms both neural and symbolic methods on test sets from Isabelle's HOL library and from its Archive of Formal Proofs, discovering between 29-39.5% of the gold standard human written lemmas. This is 8-15% more lemmas than the neural-only method. By leveraging the best of both symbolic and neural methods we can generate useful lemmas for a wide range of input domains, facilitating computer-assisted theory development and formalization.