Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency

• URL: http://arxiv.org/abs/2410.20936v1
• Date: Mon, 28 Oct 2024 11:37:39 GMT
• Title: Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency
• Authors: Zenan Li, Yifan Wu, Zhaoyu Li, Xinming Wei, Xian Zhang, Fan Yang, Xiaoxing Ma,
• Abstract summary: 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.
• Score: 22.86318578119266
• License:
• Abstract: Autoformalization, the task of automatically translating natural language descriptions into a formal language, poses a significant challenge across various domains, especially in mathematics. Recent advancements in large language models (LLMs) have unveiled their promising capabilities to formalize even competition-level math problems. However, we observe a considerable discrepancy between pass@1 and pass@k accuracies in LLM-generated formalizations. To address this gap, we introduce a novel framework that scores and selects the best result from k autoformalization candidates based on two complementary self-consistency methods: symbolic equivalence and semantic consistency. Elaborately, symbolic equivalence identifies the logical homogeneity among autoformalization candidates using automated theorem provers, and semantic consistency evaluates the preservation of the original meaning by informalizing the candidates and computing the similarity between the embeddings of the original and informalized texts. Our extensive experiments on the MATH and miniF2F datasets demonstrate that our approach significantly enhances autoformalization accuracy, achieving up to 0.22-1.35x relative improvements across various LLMs and baseline methods.

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)
• Localizing Factual Inconsistencies in Attributable Text Generation [91.981439746404]
  We introduce QASemConsistency, a new formalism for localizing factual inconsistencies in attributable text generation. We first demonstrate the effectiveness of the QASemConsistency methodology for human annotation. We then implement several methods for automatically detecting localized factual inconsistencies.
  arXiv  Detail & Related papers  (2024-10-09T22:53:48Z)
• Consistent Autoformalization for Constructing Mathematical Libraries [4.559523879294721]
  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.
  arXiv  Detail & Related papers  (2024-10-05T15:13:22Z)
• Factual Dialogue Summarization via Learning from Large Language Models [35.63037083806503]
  Large language model (LLM)-based automatic text summarization models generate more factually consistent summaries. We employ zero-shot learning to extract symbolic knowledge from LLMs, generating factually consistent (positive) and inconsistent (negative) summaries. Our approach achieves better factual consistency while maintaining coherence, fluency, and relevance, as confirmed by various automatic evaluation metrics.
  arXiv  Detail & Related papers  (2024-06-20T20:03:37Z)
• LLM Critics Help Catch Bugs in Mathematics: Towards a Better Mathematical Verifier with Natural Language Feedback [71.95402654982095]
  We propose Math-Minos, a natural language feedback-enhanced verifier. Our experiments reveal that a small set of natural language feedback can significantly boost the performance of the verifier.
  arXiv  Detail & Related papers  (2024-06-20T06:42:27Z)
• Semantic Consistency for Assuring Reliability of Large Language Models [9.876355290198639]
  Large Language Models (LLMs) exhibit remarkable fluency and competence across various natural language tasks. We introduce a general measure of semantic consistency, and formulate multiple versions of this metric to evaluate the performance of various LLMs. We propose a novel prompting strategy, called Ask-to-Choose (A2C), to enhance semantic consistency.
  arXiv  Detail & Related papers  (2023-08-17T18:11:33Z)
• Enriching Disentanglement: From Logical Definitions to Quantitative Metrics [59.12308034729482]
  Disentangling the explanatory factors in complex data is a promising approach for data-efficient representation learning. We establish relationships between logical definitions and quantitative metrics to derive theoretically grounded disentanglement metrics. We empirically demonstrate the effectiveness of the proposed metrics by isolating different aspects of disentangled representations.
  arXiv  Detail & Related papers  (2023-05-19T08:22:23Z)
• Co-Driven Recognition of Semantic Consistency via the Fusion of Transformer and HowNet Sememes Knowledge [6.184249194474601]
  This paper proposes a co-driven semantic consistency recognition method based on the fusion of Transformer and HowNet sememes knowledge. BiLSTM is exploited to encode the conceptual semantic information and infer the semantic consistency.
  arXiv  Detail & Related papers  (2023-02-21T09:53:19Z)
• A Latent-Variable Model for Intrinsic Probing [93.62808331764072]
  We propose a novel latent-variable formulation for constructing intrinsic probes. We find empirical evidence that pre-trained representations develop a cross-lingually entangled notion of morphosyntax.
  arXiv  Detail & Related papers  (2022-01-20T15:01:12Z)
• Joint Contextual Modeling for ASR Correction and Language Understanding [60.230013453699975]
  We propose multi-task neural approaches to perform contextual language correction on ASR outputs jointly with language understanding (LU) We show that the error rates of off the shelf ASR and following LU systems can be reduced significantly by 14% relative with joint models trained using small amounts of in-domain data.
  arXiv  Detail & Related papers  (2020-01-28T22:09:25Z)

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.