用AI打造可验证的数学证明辅导系统，让学习更准确高效。
LeanTutor: Towards a Verified AI Mathematical Proof Tutor
- 结合大模型与定理证明器，实现自然语言与形式化证明的双向转换。
- 在371个皮亚诺算术证明上验证系统，能正确生成下一步推理。
- 适合数学教育、形式化验证研究者使用，提升教学可信度。
本文探讨开发一种基于人工智能的可验证数学证明辅导系统。尽管大型语言模型（LLMs）能实现自然语言的流畅交互，但容易出错；而定理证明器如Lean虽能保证正确性，却对学生难学。我们提出一个概念验证系统LeanTutor，融合两者优势，由三个模块组成：(i) 自动形式化/证明检查器，(ii) 下一步推理生成器，(iii) 自然语言反馈生成器。为评估系统，我们引入PeanoBench数据集，包含371个源自Natural Numbers Game的人类编写自然语言和形式语言的皮亚诺算术证明。
原文摘要 · Abstract (English)
This paper considers the development of an AI-based provably-correct mathematical proof tutor. While Large Language Models (LLMs) allow seamless communication in natural language, they are error prone. Theorem provers such as Lean allow for provable-correctness, but these are hard for students to learn. We present a proof-of-concept system (LeanTutor) by combining the complementary strengths of LLMs and theorem provers. LeanTutor is composed of three modules: (i) an autoformalizer/proof-checker, (ii) a next-step generator, and (iii) a natural language feedback generator. To evaluate the system, we introduce PeanoBench, a dataset of 371 Peano Arithmetic proofs in human-written natural language and formal language, derived from the Natural Numbers Game.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。