Improving the Diproche CNL through Autoformalization via Large Language Models

TL;DR

This paper investigates enhancing the Diproche proof checker by leveraging large language models for autoformalization, aiming to improve proof verification in educational settings involving controlled natural language.

Contribution

It introduces a novel approach of using large language models to autoformalize controlled natural language proofs in Diproche, improving the system's flexibility and potential accuracy.

Findings

Encouraging initial results in autoformalization accuracy

Potential for improved proof checking in didactical contexts

Demonstrates feasibility of LLM-based formalization for proof systems

Abstract

The Diproche system is an automated proof checker for texts written in a controlled fragment of German, designed for didactical applications in classes introducing students to proofs for the first time. The first version of the system used a controlled natural language for which a Prolog formalization routine was written. In this paper, we explore the possibility of prompting large language models for autoformalization in the context of Diproche, with encouraging first results.