GFLean: 基于 GF 的 Lean 自动形式化框架
基本信息
- 标题：GFLean: An Autoformalisation Framework for Lean via GF
- 作者：Shashank Pathak
- 提交日期：2024 年 4 月 1 日
- arXiv 编号：arXiv:2404.01234 [cs.CL]
- 学科分类：
- 主要分类：Computation and Language (cs.CL)
- 交叉分类：Logic (math.LO)
- ACM 分类：I.2.7
- 备注：19 页，3 幅图
- DOI：https://doi.org/10.48550/arXiv.2404.01234
摘要
本文提出了一个面向 Lean 定理证明器的自动形式化（autoformalisation）框架，称为 GFLean。GFLean 使用一种名为 Grammatical Framework（GF） 的高层语法编写工具来进行解析（parsing）和线性化（linearisation），并以 Haskell 语言实现。
论文介绍了 GFLean 的功能、内部工作机制，并讨论了其局限性。此外，作者还探讨了如何将基于神经网络的翻译程序与基于规则的翻译程序结合使用、相互补充，从而构建更加稳健的自动形式化框架。
主题关键词
- 自动形式化（Autoformalisation）
- Lean 定理证明器
- Grammatical Framework (GF)
- 语法解析与线性化
- 神经网络翻译 vs. 规则翻译