将数学形式化证明转化为自然语言，让机器可验证内容更易读。
Symbolic Informalization: Fluent, Productive, Multilingual
- 用跨系统中间语言连接不同证明工具，实现多语言自然语言转换。
- 在多语言环境下生成流畅、语法正确且保持精确性的数学描述文本。
- 适合想提升形式化内容可读性的研究人员和教育工作者。
符号非正式化使形式化数学能够可靠地转换为自然语言，有望在不损失精度的前提下，让机器可验证的内容对人类更易读。在传统证明系统中，符号非正式化将有限的语法糖机制扩展为数学的常规语言表达；在由人工智能构建并自动形式化的场景下，它能精准解释所构造的内容。本文介绍了名为Informath的项目，旨在展示符号非正式化如何以合理开发成本生成流畅文本，并支持多种形式化与自然语言。Informath采用一种跨语言架构，其中Dedukti作为枢纽连接Agda、Lean、Rocq等不同证明系统，而Grammatical Framework（GF）则负责确保多种自然语言下的语法正确性与语言多样性。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。