非形式化到形式化数学的神经翻译初步实验
计算与语言
2018-06-12 v2 人工智能
机器学习
计算机科学中的逻辑
摘要
我们报告了训练深度神经网络以自动将非形式化的 LaTeX 编写的 Mizar 文本翻译为形式化 Mizar 语言的实验。据我们所知，这是神经网络首次被用于数学形式化。使用 Luong 等人的神经机器翻译模型（NMT），我们针对各种超参数测试了对齐的非形式化-形式化语料库并评估了它们的结果。我们的实验表明，性能最佳的模型配置能够在 65.73% 的推理数据上生成正确的 Mizar 语句，所有模型的并集覆盖了 79.17%。这些结果表明，通过人工神经网络进行形式化是数学自动形式化的一种有前景的方法。我们给出了若干案例研究以说明我们的结果。
引用
@article{arxiv.1805.06502,
title = {First Experiments with Neural Translation of Informal to Formal Mathematics},
author = {Qingxiang Wang and Cezary Kaliszyk and Josef Urban},
journal= {arXiv preprint arXiv:1805.06502},
year = {2018}
}
备注
Submission to CICM'2018