Symbolic Informalization: Fluent, Productive, Multilingual

• URL: http://arxiv.org/abs/2606.16893v1
• Date: Mon, 15 Jun 2026 16:06:21 GMT
• Title: Symbolic Informalization: Fluent, Productive, Multilingual
• Abstract summary: Symbolic informalization enables a reliable conversion of formal mathematics to natural language.<n>This paper outlines the project Informath, which aims to show how symbolic informalization can produce fluent text.
• Score: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Symbolic informalization enables a reliable conversion of formal mathematics to natural language. It has the potential to make machine-checked content human-readable without loss of precision. In a traditional proof system usage, symbolic informalization generalizes the limited mechanisms of syntactic sugar into the ordinary language of mathematics. In a setting where proofs are constructed by artificial intelligence and autoformalization, symbolic informalization can explain what precisely has been constructed. This paper outlines the project Informath, which aims to show how symbolic informalization can produce fluent text with a reasonable development effort and address multiple formal and natural languages. Informath is based on an interlingual architecture, where Dedukti works as a hub between different proof systems (Agda, Lean, Rocq) and Grammatical Framework (GF) takes care of linguistic correctness and variation in different natural languages.

Related papers

• Coherency through formalisations of Structured Natural Language, A case study on FRETish [0.0]
  Formalisation is the process of writing system requirements in a formal language.<n>In this paper we propose a new guideline: Coherency through Formalisations.<n>We analyze NASA's Formal Requirement Elicitation Tool FRET and propose an alternative automated translation of the Controlled Natural Language FRETish to the formal language of MTL.
  arXiv  Detail & Related papers  (2026-05-11T12:30:53Z)
• Position: Natural Language Should Not Fully Replace Formal Languages [11.90605417129287]
  We argue that natural language is optimized for underspecification in open-ended contexts.<n>We show that natural language excels at low specificity tasks, while formal languages are advantageous on tasks with stricter requirements.
  arXiv  Detail & Related papers  (2026-05-10T15:01:16Z)
• Cognitive Mismatch in Multimodal Large Language Models for Discrete Symbol Understanding [96.81411333150213]
  This paper introduces a benchmark to evaluate how top-tier MLLMs navigate discrete semantic spaces.<n>Our investigation uncovers a counterintuitive phenomenon: models often fail at basic symbol recognition yet succeed in complex reasoning tasks.<n>This work offers a roadmap for developing more rigorous, human-aligned intelligent systems.
  arXiv  Detail & Related papers  (2026-03-19T04:08:20Z)
• Data2Concept2Text: An Explainable Multilingual Framework for Data Analysis Narration [42.95840730800478]
  This paper presents a complete explainable system that interprets a set of data, abstracts the underlying features and describes them in a natural language of choice.<n>The system relies on two crucial stages: (i) identifying emerging properties from data and transforming them into abstract concepts, and (ii) converting these concepts into natural language.
  arXiv  Detail & Related papers  (2025-02-13T11:49:48Z)
• From Word Models to World Models: Translating from Natural Language to the Probabilistic Language of Thought [124.40905824051079]
  We propose rational meaning construction, a computational framework for language-informed thinking. We frame linguistic meaning as a context-sensitive mapping from natural language into a probabilistic language of thought. We show that LLMs can generate context-sensitive translations that capture pragmatically-appropriate linguistic meanings. We extend our framework to integrate cognitively-motivated symbolic modules.
  arXiv  Detail & Related papers  (2023-06-22T05:14:00Z)
• Lexinvariant Language Models [84.2829117441298]
  Token embeddings, a mapping from discrete lexical symbols to continuous vectors, are at the heart of any language model (LM) We study textitlexinvariantlanguage models that are invariant to lexical symbols and therefore do not need fixed token embeddings in practice. We show that a lexinvariant LM can attain perplexity comparable to that of a standard language model, given a sufficiently long context.
  arXiv  Detail & Related papers  (2023-05-24T19:10:46Z)
• Geometry of Language [0.0]
  We present a fresh perspective on language, combining ideas from various sources, but mixed in a new synthesis. The question is whether we can formulate an elegant formalism, a universal grammar or a mechanism which explains significant aspects of the human faculty of language. We describe such a mechanism, which differs from existing logical and grammatical approaches by its geometric nature.
  arXiv  Detail & Related papers  (2023-03-09T12:22:28Z)
• Towards Autoformalization of Mathematics and Code Correctness: Experiments with Elementary Proofs [5.045988012508899]
  Autoformalization seeks to address this by translating proofs written in natural language into a formal representation that is computer-verifiable via interactive theorem provers. We introduce a semantic parsing approach, based on the Universal Transformer architecture, that translates elementary mathematical proofs into an equivalent formalization in the language of the Coq interactive theorem prover.
  arXiv  Detail & Related papers  (2023-01-05T17:56:00Z)
• Language Models as Inductive Reasoners [125.99461874008703]
  We propose a new paradigm (task) for inductive reasoning, which is to induce natural language rules from natural language facts. We create a dataset termed DEER containing 1.2k rule-fact pairs for the task, where rules and facts are written in natural language. We provide the first and comprehensive analysis of how well pretrained language models can induce natural language rules from natural language facts.
  arXiv  Detail & Related papers  (2022-12-21T11:12:14Z)
• Transparency Helps Reveal When Language Models Learn Meaning [71.96920839263457]
  Our systematic experiments with synthetic data reveal that, with languages where all expressions have context-independent denotations, both autoregressive and masked language models learn to emulate semantic relations between expressions. Turning to natural language, our experiments with a specific phenomenon -- referential opacity -- add to the growing body of evidence that current language models do not well-represent natural language semantics.
  arXiv  Detail & Related papers  (2022-10-14T02:35:19Z)
• A Latent-Variable Model for Intrinsic Probing [93.62808331764072]
  We propose a novel latent-variable formulation for constructing intrinsic probes.<n>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)
• Probing Linguistic Information For Logical Inference In Pre-trained Language Models [2.4366811507669124]
  We propose a methodology for probing linguistic information for logical inference in pre-trained language model representations. We find that (i) pre-trained language models do encode several types of linguistic information for inference, but there are also some types of information that are weakly encoded. We have demonstrated language models' potential as semantic and background knowledge bases for supporting symbolic inference methods.
  arXiv  Detail & Related papers  (2021-12-03T07:19:42Z)
• Learning Symbolic Rules for Reasoning in Quasi-Natural Language [74.96601852906328]
  We build a rule-based system that can reason with natural language input but without the manual construction of rules. We propose MetaQNL, a "Quasi-Natural" language that can express both formal logic and natural language sentences. Our approach achieves state-of-the-art accuracy on multiple reasoning benchmarks.
  arXiv  Detail & Related papers  (2021-11-23T17:49:00Z)

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.