# Improving the Diproche CNL through Autoformalization via Large Language Models

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

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 4 of its 16 references that are in the map.
- First posted on arXiv 12 Mar 2023.

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

- [Autoformalization with Large Language Models](https://mlsanity.com/paper/2205.12615/) (2022)
- [ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics](https://mlsanity.com/paper/2302.12433/) (2023)
- [Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar](https://mlsanity.com/paper/1912.02636/) (2019)
- [Natural Language Proof Checking in Introduction to Proof Classes -- First Experiences with Diproche](https://mlsanity.com/paper/2202.08131/) (2022)

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

- [Using Large Language Models for (De-)Formalization and Natural Argumentation Exercises for Beginner's Students](https://mlsanity.com/paper/2304.06186/) (2023)

## Abstract (arXiv)

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.