Autogenerating Natural Language Proofs for Proof Education

EasyChair Preprint 8600

Abstract

Understanding mathematical proofs is critical for students learning the foundations of computing. Having students construct mathematical proofs with the help of a computer is appealing as it makes it easier to autograde student work and autogenerate practice problems for students. Most existing tools for students to construct proofs with a computer are restricted systems that only permit simple logics, or there is a large overhead involved in students learning how to use them Proof Blocks (proofblocks.org), a tool that allows students to drag-and-drop prewritten lines of a proof into the correct order is a nice compromise because the tool is easy for students to use to construct proofs on any topic~\cite{poulsen2022proof}. However, a downside is that the process of writing questions can be time consuming and error-prone. An instructor must write the proof, break it into lines, and then specify a directed acyclic graph giving the logical dependence between lines of the proof. In this paper, we document the first step toward building a system to automatically generate Proof Blocks problems from Coq proofs: a Coq plugin which generates a natural language proof from a Coq proof. Our natural language generator differs from similar tools in that we deliberately restrict which definitions and tactics are allowed in the interest of improving readability of the output.

Keyphrases: CS education, Coq plugin, Natural Language Generation

@booklet{EasyChair:8600,
  author    = {Seth Poulsen and Matthew West and Talia Ringer},
  title     = {Autogenerating Natural Language Proofs for Proof Education},
  howpublished = {EasyChair Preprint 8600},
  year      = {EasyChair, 2022}}