Using Large Language Models for (De-)Formalization and Natural Argumentation Exercises for Beginner's Students
Not on the map. Why?
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.
Key facts. No citing papers in the map yet (data through 7 Oct 2026). Builds on 7 of its 21 references that are in the map. First posted on arXiv 12 Apr 2023.
Builds on
7 of 21 references.
References · 7
- 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
- 2020Using Automated Theorem Provers for Mistake Diagnosis in the Didactics of Mathematicscited by 1
- 2020Automatized Evaluation of Formalization Exercises in Mathematicscited by 1
- 2023Improving the Diproche CNL through Autoformalization via Large Language Modelscited by 1
Built on by
Not cited yet.