Consistent Autoformalization for Constructing Mathematical Libraries

• URL: http://arxiv.org/abs/2410.04194v1
• Date: Sat, 5 Oct 2024 15:13:22 GMT
• Title: Consistent Autoformalization for Constructing Mathematical Libraries
• Authors: Lan Zhang, Xin Quan, Andre Freitas,
• Abstract summary: Autoformalization is the task of automatically translating mathematical content written in natural language to a formal language expression. This paper proposes the coordinated use of three mechanisms, most-similar retrieval augmented generation (MS-RAG), denoising steps, and auto-correction with syntax error feedback (Auto-SEF) to improve autoformalization quality.
• Score: 4.559523879294721
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: 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), including in formal languages, are lowering the barriers for autoformalization. However, LLMs alone are not capable of consistently and reliably delivering autoformalization, in particular as the complexity and specialization of the target domain grows. As the field evolves into the direction of systematically applying autoformalization towards large mathematical libraries, the need to improve syntactic, terminological and semantic control increases. This paper proposes the coordinated use of three mechanisms, most-similar retrieval augmented generation (MS-RAG), denoising steps, and auto-correction with syntax error feedback (Auto-SEF) to improve autoformalization quality. The empirical analysis, across different models, demonstrates that these mechanisms can deliver autoformalizaton results which are syntactically, terminologically and semantically more consistent. These mechanisms can be applied across different LLMs and have shown to deliver improve results across different model types.

Related papers

• Unified Generative and Discriminative Training for Multi-modal Large Language Models [88.84491005030316]
  Generative training has enabled Vision-Language Models (VLMs) to tackle various complex tasks. Discriminative training, exemplified by models like CLIP, excels in zero-shot image-text classification and retrieval. This paper proposes a unified approach that integrates the strengths of both paradigms.
  arXiv  Detail & Related papers  (2024-11-01T01:51:31Z)
• Self-Healing Machine Learning: A Framework for Autonomous Adaptation in Real-World Environments [50.310636905746975]
  Real-world machine learning systems often encounter model performance degradation due to distributional shifts in the underlying data generating process. Existing approaches to addressing shifts, such as concept drift adaptation, are limited by their reason-agnostic nature. We propose self-healing machine learning (SHML) to overcome these limitations.
  arXiv  Detail & Related papers  (2024-10-31T20:05:51Z)
• Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency [22.86318578119266]
  We introduce a novel framework that scores and selects the best result from k autoformalization candidates based on symbolic equivalence and semantic consistency. Our experiments on the MATH and miniF2F datasets demonstrate that our approach significantly enhances autoformalization accuracy.
  arXiv  Detail & Related papers  (2024-10-28T11:37:39Z)
• Boosting the Capabilities of Compact Models in Low-Data Contexts with Large Language Models and Retrieval-Augmented Generation [2.9921619703037274]
  We propose a retrieval augmented generation (RAG) framework backed by a large language model (LLM) to correct the output of a smaller model for the linguistic task of morphological glossing. We leverage linguistic information to make up for the lack of data and trainable parameters, while allowing for inputs from written descriptive grammars interpreted and distilled through an LLM. We show that a compact, RAG-supported model is highly effective in data-scarce settings, achieving a new state-of-the-art for this task and our target languages.
  arXiv  Detail & Related papers  (2024-10-01T04:20:14Z)
• Explaining Text Similarity in Transformer Models [52.571158418102584]
  Recent advances in explainable AI have made it possible to mitigate limitations by leveraging improved explanations for Transformers. We use BiLRP, an extension developed for computing second-order explanations in bilinear similarity models, to investigate which feature interactions drive similarity in NLP models. Our findings contribute to a deeper understanding of different semantic similarity tasks and models, highlighting how novel explainable AI methods enable in-depth analyses and corpus-level insights.
  arXiv  Detail & Related papers  (2024-05-10T17:11:31Z)
• Emergent Linguistic Structures in Neural Networks are Fragile [20.692540987792732]
  Large Language Models (LLMs) have been reported to have strong performance on natural language processing tasks. We propose a framework to assess the consistency and robustness of linguistic representations.
  arXiv  Detail & Related papers  (2022-10-31T15:43:57Z)
• Autoregressive Structured Prediction with Language Models [73.11519625765301]
  We describe an approach to model structures as sequences of actions in an autoregressive manner with PLMs. Our approach achieves the new state-of-the-art on all the structured prediction tasks we looked at.
  arXiv  Detail & Related papers  (2022-10-26T13:27:26Z)
• Unifying Framework for Optimizations in non-boolean Formalisms [0.6853165736531939]
  Many popular automated reasoning paradigms provide languages supporting optimization statements. Here we propose a unifying framework that eliminates syntactic distinctions between paradigms. We study formal properties of the proposed systems that translate into formal properties of paradigms that can be captured within our framework.
  arXiv  Detail & Related papers  (2022-06-16T00:38:19Z)
• Incorporating Linguistic Knowledge for Abstractive Multi-document Summarization [20.572283625521784]
  We develop a neural network based abstractive multi-document summarization (MDS) model. We process the dependency information into the linguistic-guided attention mechanism. With the help of linguistic signals, sentence-level relations can be correctly captured.
  arXiv  Detail & Related papers  (2021-09-23T08:13:35Z)
• Contextualized Perturbation for Textual Adversarial Attack [56.370304308573274]
  Adversarial examples expose the vulnerabilities of natural language processing (NLP) models. This paper presents CLARE, a ContextuaLized AdversaRial Example generation model that produces fluent and grammatical outputs.
  arXiv  Detail & Related papers  (2020-09-16T06:53:15Z)
• Improve Variational Autoencoder for Text Generationwith Discrete Latent Bottleneck [52.08901549360262]
  Variational autoencoders (VAEs) are essential tools in end-to-end representation learning. VAEs tend to ignore latent variables with a strong auto-regressive decoder. We propose a principled approach to enforce an implicit latent feature matching in a more compact latent space.
  arXiv  Detail & Related papers  (2020-04-22T14:41:37Z)

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.