Symbolic Informalization: Fluent, Productive, Multi... | AI Research

Symbolic Informalization: Fluent, Productive, Multilingual
The paper introduces "Informath," a project designed to bridge the gap between formal mathematical logic and the natural language used in textbooks and research. While modern artificial intelligence can help formalize mathematics, it often struggles to explain its work in a way that humans can easily verify. Informath uses "symbolic informalization" to reliably convert machine-checked proofs into fluent, human-readable text across multiple languages, ensuring that the precision of formal logic is preserved without requiring the user to read complex code.

The Architecture of Informath

Informath functions as a translation hub that connects different formal proof systems—such as Agda, Lean, and Rocq—with natural languages. It uses two primary components to achieve this: Dedukti and the Grammatical Framework (GF). Dedukti acts as a central "interlingua," a formal hub that standardizes the logic from various proof systems. Meanwhile, the Grammatical Framework manages the linguistic side, ensuring that the output is grammatically correct and capable of being translated into different natural languages, such as English, French, German, and Swedish.

Achieving Fluency and Multilinguality

A major challenge in translating formal logic is making the output sound natural rather than rigid or robotic. Informath addresses this by utilizing the Resource Grammar Library (RGL), which contains the linguistic structures for approximately 40 languages. By using the RGL, the system can generate diverse and flexible expressions that mirror how mathematicians actually write. Because the system separates the formal logic (Dedukti) from the linguistic rules (GF), adding a new language is a modular process that does not require rebuilding the entire system.

Improving Productivity

To make the system practical for researchers, Informath aims to be "productive," meaning it is feasible to design and implement without requiring users to be experts in linguistics or grammar coding. The project seeks to allow users to interact with the system without needing to see the underlying GF code. By providing tools to map formal concepts to a pre-existing lexicon, Informath allows users to define how their specific mathematical concepts should be verbalized, making the system accessible to those who are primarily interested in using proof systems for mathematics rather than software engineering.

Key Considerations

While symbolic informalization offers a reliable alternative to the "hallucinations" sometimes produced by large language models, it faces inherent challenges. The paper notes that informal language is often vague and lacks the strict rules of formal systems, making the translation process complex. Furthermore, because the system relies on compositional rules, it must be carefully designed to handle the nuances of mathematical syntax. Ultimately, Informath serves as a tool to make formal mathematics more transparent, allowing users to verify that a computer-generated proof matches their intended mathematical statement.