# Using Large Language Models for (De-)Formalization and Natural Argumentation Exercises for Beginner's Students

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 7 of its 21 references that are in the map.
- First posted on arXiv 12 Apr 2023.

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

- [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)
- [Using Automated Theorem Provers for Mistake Diagnosis in the Didactics of Mathematics](https://mlsanity.com/paper/2002.05083/) (2020)
- [Automatized Evaluation of Formalization Exercises in Mathematics](https://mlsanity.com/paper/2006.01800/) (2020)
- [Improving the Diproche CNL through Autoformalization via Large Language Models](https://mlsanity.com/paper/2303.17513/) (2023)

## Abstract (arXiv)

We describe two systems currently being developed that use large language models for the automatized correction of (i) exercises in translating back and forth between natural language and the languages of propositional logic and first-order predicate logic and (ii) exercises in writing simple arguments in natural language in non-mathematical scenarios.