KELPS: A Framework for Verified Multi-Language Autoformalization via Semantic-Syntactic Alignment

• URL: http://arxiv.org/abs/2507.08665v1
• Date: Fri, 11 Jul 2025 15:05:06 GMT
• Title: KELPS: A Framework for Verified Multi-Language Autoformalization via Semantic-Syntactic Alignment
• Authors: Jiyao Zhang, Chengli Zhong, Hui Xu, Qige Li, Yi Zhou,
• Abstract summary: KELPS is an iterative framework for translating, synthesizing, and filtering informal data into formal languages.<n>First, we translate natural language into Knowledge Equations (KEs), a novel language that we designed, theoretically grounded in assertional logic.<n>Next, we convert them to target languages through rigorously defined rules that preserve both syntactic structure and semantic meaning.<n>This process yielded a parallel corpus of over 60,000 problems.
• Score: 5.295540405828356
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Modern large language models (LLMs) show promising progress in formalizing informal mathematics into machine-verifiable theorems. However, these methods still face bottlenecks due to the limited quantity and quality of multilingual parallel corpora. In this paper, we propose a novel neuro-symbolic framework KELPS (Knowledge-Equation based Logical Processing System) to address these problems. KELPS is an iterative framework for translating, synthesizing, and filtering informal data into multiple formal languages (Lean, Coq, and Isabelle). First, we translate natural language into Knowledge Equations (KEs), a novel language that we designed, theoretically grounded in assertional logic. Next, we convert them to target languages through rigorously defined rules that preserve both syntactic structure and semantic meaning. This process yielded a parallel corpus of over 60,000 problems. Our framework achieves 88.9% syntactic accuracy (pass@1) on MiniF2F, outperforming SOTA models such as Deepseek-V3 (81%) and Herald (81.3%) across multiple datasets. All datasets and codes are available in the supplementary materials.

Related papers

• The Unreasonable Effectiveness of Model Merging for Cross-Lingual Transfer in LLMs [54.59207567677249]
  Large language models (LLMs) still struggle across tasks outside of high-resource languages.<n>In this work, we investigate cross-lingual transfer to lower-resource languages where task-specific post-training data is scarce.
  arXiv  Detail & Related papers  (2025-05-23T20:28:31Z)
• Towards Typologically Aware Rescoring to Mitigate Unfaithfulness in Lower-Resource Languages [9.426642998924724]
  Multilingual large language models generate non-faithful output in resource-constrained languages.<n>To mitigate unfaithfulness in such settings, we propose using computationally light auxiliary models to rescore the outputs of larger architectures.<n>We show that monolingual 4-layer BERT models pretrained from scratch on less than 700 MB of data without fine-tuning are able to identify faithful summaries with a mean accuracy of 88.33%.
  arXiv  Detail & Related papers  (2025-02-24T21:22:19Z)
• Training Neural Networks as Recognizers of Formal Languages [87.06906286950438]
  We train and evaluate neural networks directly as binary classifiers of strings.<n>We provide results on a variety of languages across the Chomsky hierarchy for three neural architectures.<n>Our contributions will facilitate theoretically sound empirical testing of language recognition claims in future work.
  arXiv  Detail & Related papers  (2024-11-11T16:33:25Z)
• In-Context Language Learning: Architectures and Algorithms [73.93205821154605]
  We study ICL through the lens of a new family of model problems we term in context language learning (ICLL) We evaluate a diverse set of neural sequence models on regular ICLL tasks.
  arXiv  Detail & Related papers  (2024-01-23T18:59:21Z)
• Automatic Model Selection with Large Language Models for Reasoning [33.93807127935167]
  Chain-of-Thought (CoT) and Program-Aided Language Models (PAL) represent two distinct reasoning methods. We introduce a model selection method to combine the best of both worlds by employing a large language model. Our proposed method demonstrates significant performance improvements across eight reasoning datasets.
  arXiv  Detail & Related papers  (2023-05-23T17:57:59Z)
• Learning Disentangled Semantic Representations for Zero-Shot Cross-Lingual Transfer in Multilingual Machine Reading Comprehension [40.38719019711233]
  Multilingual pre-trained models are able to zero-shot transfer knowledge from rich-resource languages to low-resource languages in machine reading comprehension (MRC) In this paper, we propose a novel multilingual MRC framework equipped with a Siamese Semantic Disentanglement Model (SSDM) to disassociate semantics from syntax in representations learned by multilingual pre-trained models.
  arXiv  Detail & Related papers  (2022-04-03T05:26:42Z)
• Zero-Shot Cross-lingual Semantic Parsing [56.95036511882921]
  We study cross-lingual semantic parsing as a zero-shot problem without parallel data for 7 test languages. We propose a multi-task encoder-decoder model to transfer parsing knowledge to additional languages using only English-Logical form paired data. Our system frames zero-shot parsing as a latent-space alignment problem and finds that pre-trained models can be improved to generate logical forms with minimal cross-lingual transfer penalty.
  arXiv  Detail & Related papers  (2021-04-15T16:08:43Z)
• SML: a new Semantic Embedding Alignment Transformer for efficient cross-lingual Natural Language Inference [71.57324258813674]
  The ability of Transformers to perform with precision a variety of tasks such as question answering, Natural Language Inference (NLI) or summarising, have enable them to be ranked as one of the best paradigms to address this kind of tasks at present. NLI is one of the best scenarios to test these architectures, due to the knowledge required to understand complex sentences and established a relation between a hypothesis and a premise. In this paper, we propose a new architecture, siamese multilingual transformer, to efficiently align multilingual embeddings for Natural Language Inference.
  arXiv  Detail & Related papers  (2021-03-17T13:23:53Z)
• XCOPA: A Multilingual Dataset for Causal Commonsense Reasoning [68.57658225995966]
  Cross-lingual Choice of Plausible Alternatives (XCOPA) is a typologically diverse multilingual dataset for causal commonsense reasoning in 11 languages. We evaluate a range of state-of-the-art models on this novel dataset, revealing that the performance of current methods falls short compared to translation-based transfer.
  arXiv  Detail & Related papers  (2020-05-01T12:22:33Z)

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.