Improving the Diproche CNL through Autoformalization via Large Language Models
Not on the map. Why?
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.
Key facts. Cited by 1 paper in the map (data through 7 Oct 2026). Builds on 4 of its 16 references that are in the map. First posted on arXiv 12 Mar 2023.
Builds on
4 of 16 references.
References · 4
- 2022Autoformalization with Large Language Modelscited by 252
- 2023ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematicscited by 180
- 2019Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizarcited by 40
- 2022Natural Language Proof Checking in Introduction to Proof Classes -- First Experiences with Diprochecited by 2
Built on by
Citing papers per year: 2023: 1.
1 paper.