Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency

• URL: http://arxiv.org/abs/2410.20936v2
• Date: Fri, 06 Dec 2024 09:06:20 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

• Instantiation-based Formalization of Logical Reasoning Tasks using Language Models and Logical Solvers [4.897782942277061]
  We introduce Semantic Self-Verification (SSV), a novel approach to accurately formulate the reasoning problem from natural language to the formal language of the solver. SSV uses a consistency-based approach to produce strong abstract formalizations of problems using concrete instantiations that are generated by the model and verified by the solver. We propose such *near-certain reasoning* as a new approach to reduce the need for manual verification in many cases, taking us closer to more dependable and autonomous AI reasoning systems.
  arXiv  Detail & Related papers  (2025-01-28T14:04:49Z)
• Emergence of Self-Identity in AI: A Mathematical Framework and Empirical Study with Generative Large Language Models [4.036530158875673]
  This paper introduces a mathematical framework for defining and quantifying self-identity in AI systems. Our framework posits that self-identity emerges from two mathematically quantifiable conditions. The implications of our study are immediately relevant to the fields of humanoid robotics and autonomous systems.
  arXiv  Detail & Related papers  (2024-11-27T17:23:47Z)
• 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)
• 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)
• Improving Autoformalization using Type Checking [15.58948808529849]
  We analyze both current autoformalization methods and the processes used to evaluate them, focusing specifically on the Lean 4 theorem proving language. We demonstrate that scaling type-check filtering with self-consistency techniques on top of existing methods significantly improves performance, achieving absolute accuracy gains of up to +18.4% on ProofNet. We also release new benchmarks: a new research-level mathematics dataset RLM25, a corrected ProofNet, and ProofNetVerif with labeled correct and incorrect autoformalization pairs for evaluating metrics.
  arXiv  Detail & Related papers  (2024-06-11T13:01:50Z)
• 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)
• 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.