Improving the Diproche CNL through Autoformalization via Large Language Models
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.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
Natural Language Proof Checking in Introduction to Proof Classes -- First Experiences with Diproche
We present and analyze the employment of the Diproche system, a natural language proof checker, within a one-semester mathematics beginners lecture with 228 participants. The system is used to check the students' solutio…
MASA: LLM-Driven Multi-Agent Systems for Autoformalization
Autoformalization serves a crucial role in connecting natural language and formal reasoning. This paper presents MASA, a novel framework for building multi-agent systems for autoformalization driven by Large Language Mod…
ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization
Autoformalization, which translates natural language mathematics into machine-verifiable formal statements, is critical for using formal mathematical reasoning to solve math problems stated in natural language. While Lar…
Mathematical ReasoningConsistent Autoformalization for Constructing Mathematical Libraries
Autoformalization is the task of automatically translating mathematical content written in natural language to a formal language expression. The growing language interpretation capabilities of Large Language Models (LLMs…
DenoisingRAGRetrieval-augmented GenerationProcess-Driven Autoformalization in Lean 4
Autoformalization, the conversion of natural language mathematics into formal languages, offers significant potential for advancing mathematical reasoning. However, existing efforts are limited to formal languages with s…
Mathematical Reasoning