# Roosterize: Suggesting Lemma Names for Coq Verification Projects Using Deep Learning

arXiv: https://arxiv.org/abs/2103.01346 · HTML: https://mlsanity.com/paper/2103.01346/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 6 of its 20 references that are in the map.
- First posted on arXiv 1 Mar 2021.

## Builds on (most cited first, 6 of 6)

- [Sequence to Sequence Learning with Neural Networks](https://mlsanity.com/paper/1409.3215/) (2014)
- [Get To The Point: Summarization with Pointer-Generator Networks](https://mlsanity.com/paper/1704.04368/) (2017)
- [Effective Approaches to Attention-based Neural Machine Translation](https://mlsanity.com/paper/1508.04025/) (2015)
- [OpenNMT: Open-source Toolkit for Neural Machine Translation](https://mlsanity.com/paper/1709.03815/) (2017)
- [Learning Natural Coding Conventions](https://mlsanity.com/paper/1402.4182/) (2014)
- [Deep Generation of Coq Lemma Names Using Elaborated Terms](https://mlsanity.com/paper/2004.07761/) (2020)

## Built on by (most cited first, 1 of 1)

- [Baldur: Whole-Proof Generation and Repair with Large Language Models](https://mlsanity.com/paper/2303.04910/) (2023)

## Abstract (arXiv)

Naming conventions are an important concern in large verification projects using proof assistants, such as Coq. In particular, lemma names are used by proof engineers to effectively understand and modify Coq code. However, providing accurate and informative lemma names is a complex task, which is currently often carried out manually. Even when lemma naming is automated using rule-based tools, generated names may fail to adhere to important conventions not specified explicitly. We demonstrate a toolchain, dubbed Roosterize, which automatically suggests lemma names in Coq projects. Roosterize leverages a neural network model trained on existing Coq code, thus avoiding manual specification of naming conventions. To allow proof engineers to conveniently access suggestions from Roosterize during Coq project development, we integrated the toolchain into the popular Visual Studio Code editor. Our evaluation shows that Roosterize substantially outperforms strong baselines for suggesting lemma names and is useful in practice. The demo video for Roosterize can be viewed at: https://youtu.be/HZ5ac7Q14rc.