Improving the Diproche CNL through Autoformalization via Large Language Models

• URL: http://arxiv.org/abs/2303.17513v3
• Date: Wed, 10 Apr 2024 14:19:42 GMT
• Title: Improving the Diproche CNL through Autoformalization via Large Language Models
• Authors: Merlin Carl,
• Abstract summary: The Diproche system is an automated proof checker for texts written in a controlled fragment of German. In this paper, we explore the possibility of prompting large language models for autoformalization in the context of Diproche.
• Score: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: 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.

Related papers

• Using Large Language Models for (De-)Formalization and Natural Argumentation Exercises for Beginner's Students [0.0]
  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.
  arXiv  Detail & Related papers  (2023-04-12T23:05:02Z)
• nl2spec: Interactively Translating Unstructured Natural Language to Temporal Logics with Large Language Models [3.1143846686797314]
  We present nl2spec, a framework for applying Large Language Models (LLMs) derive formal specifications from unstructured natural language. We introduce a new methodology to detect and resolve the inherent ambiguity of system requirements in natural language. Users iteratively add, delete, and edit these sub-translations to amend erroneous formalizations, which is easier than manually redrafting the entire formalization.
  arXiv  Detail & Related papers  (2023-03-08T20:08:53Z)
• Bidirectional Language Models Are Also Few-shot Learners [54.37445173284831]
  We present SAP (Sequential Autoregressive Prompting), a technique that enables the prompting of bidirectional models. We show SAP is effective on question answering and summarization. For the first time, our results demonstrate prompt-based learning is an emergent property of a broader class of language models.
  arXiv  Detail & Related papers  (2022-09-29T01:35:57Z)
• Autoformalization with Large Language Models [22.86710743804944]
  A successful autoformalization system could advance the fields of formal verification, program synthesis, and artificial intelligence. We show large language models provide new prospects towards this goal. Our methodology results in a new state-of-the-art result on the MiniF2F theorem proving benchmark, improving the proof rate from $29.6%$ to $35.2%$.
  arXiv  Detail & Related papers  (2022-05-25T09:53:30Z)
• Controlling Translation Formality Using Pre-trained Multilingual Language Models [19.465727478912072]
  This paper describes the University of Maryland's submission to the Special Task on Formality Control for Spoken Language Translation at iwslt. We investigate to what extent this problem can be addressed with a textitsingle multilingual model. Results show that this strategy can approach the translation quality and formality control achieved by dedicated translation models.
  arXiv  Detail & Related papers  (2022-05-13T13:47:28Z)
• Detecting Text Formality: A Study of Text Classification Approaches [78.11745751651708]
  This work proposes the first to our knowledge systematic study of formality detection methods based on statistical, neural-based, and Transformer-based machine learning methods. We conducted three types of experiments -- monolingual, multilingual, and cross-lingual. The study shows the overcome of Char BiLSTM model over Transformer-based ones for the monolingual and multilingual formality classification task.
  arXiv  Detail & Related papers  (2022-04-19T16:23:07Z)
• Multilingual Generative Language Models for Zero-Shot Cross-Lingual Event Argument Extraction [80.61458287741131]
  We present a study on leveraging multilingual pre-trained generative language models for zero-shot cross-lingual event argument extraction (EAE) By formulating EAE as a language generation task, our method effectively encodes event structures and captures the dependencies between arguments. Our proposed model finetunes multilingual pre-trained generative language models to generate sentences that fill in the language-agnostic template with arguments extracted from the input passage.
  arXiv  Detail & Related papers  (2022-03-15T23:00:32Z)
• Differentiable Prompt Makes Pre-trained Language Models Better Few-shot Learners [23.150999852147283]
  This study proposes a novel pluggable, and efficient approach named DifferentiAble pRompT (DART) It can convert small language models into better few-shot learners without any prompt engineering. A comprehensive evaluation of standard NLP tasks demonstrates that the proposed approach achieves a better few-shot performance.
  arXiv  Detail & Related papers  (2021-08-30T12:29:25Z)
• Improving the Lexical Ability of Pretrained Language Models for Unsupervised Neural Machine Translation [127.81351683335143]
  Cross-lingual pretraining requires models to align the lexical- and high-level representations of the two languages. Previous research has shown that this is because the representations are not sufficiently aligned. In this paper, we enhance the bilingual masked language model pretraining with lexical-level information by using type-level cross-lingual subword embeddings.
  arXiv  Detail & Related papers  (2021-03-18T21:17:58Z)
• SLM: Learning a Discourse Language Representation with Sentence Unshuffling [53.42814722621715]
  We introduce Sentence-level Language Modeling, a new pre-training objective for learning a discourse language representation. We show that this feature of our model improves the performance of the original BERT by large margins.
  arXiv  Detail & Related papers  (2020-10-30T13:33:41Z)
• Generative Language Modeling for Automated Theorem Proving [94.01137612934842]
  This work is motivated by the possibility that a major limitation of automated theorem provers compared to humans might be addressable via generation from language models. We present an automated prover and proof assistant, GPT-f, for the Metamath formalization language, and analyze its performance.
  arXiv  Detail & Related papers  (2020-09-07T19:50:10Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.