导语


为了探索数学与人工智能深度融合的可能性，集智俱乐部联合同济大学特聘研究员陈小杨、清华大学交叉信息学院助理教授袁洋、南洋理工大学副教授夏克林三位老师，共同发起“人工智能与数学”读书会，希望从 AI for Math，Math for AI 两个方面深入探讨人工智能与数学的密切联系。本读书会是“AI+Science”主题读书会的第三季。读书会自9月15日开始，每周五晚20:00-22:00，预计持续时间8～10周。欢迎感兴趣的朋友报名参与！




分享内容简介



 

数学常被认为是最能体现人类智慧的领域，数学家常被看作是最聪明的人类，而AI科学家则希望挑战这些顶级人类的智能。让AI自己做数学，尤其是让AI自主证明数学定理，可能是最古老的AI领域之一，但因为组合爆炸的严峻阻碍而长期停滞。当下LLM方法高歌猛进，也给自动定理证明注入了新活力，目前的最好成果已经能够完成一些高中级别的竞赛题。本期分享将对近两三年主要使用LLM方法向数学证明发起挑战的前沿进展做一综述，畅想“AI数学家”的可能性。分享首先会介绍自动定理证明的“基础设施”——形式语言和交互式证明助手，随后介绍两种研究路线：以GPT-f为代表的形式证明搜索路线和以DSP为代表的自然证明翻译路线，最后是为了最终创造“AI数学家”所需未来工作的设想。





分享内容大纲



  • 数学环境：形式语言和证明助手

  • 路线之一：大语言模型辅助形式证明搜索

  • 路线之二：大语言模型生成自然语言证明启发形式证明

  • 番外篇：增强大语言模型推理能力的其它尝试

  • 幻想时间：如何创造“AI数学家”




主要涉及到的知识概念



 

  • 自动定理证明 Automated Theorem Proving

  • 自动形式化 Autoformalization





主讲人介绍




周子喻，捷克理工大学在读硕士，主要研究方向是利用深度学习实现自动定理证明DL4ATP。




参考文献



  • Stanislas P., & Ilya . (2020). Generative Language Modeling for Automated Theorem Proving. arXiv preprint arXiv:2009.03393.https://arxiv.org/abs/2009.03393

  • Guillaume L., Marie-Anne L., Thibaut L., Xavier M., Amaury H., Gabriel E., Aurélien R., & Timothée L. (2022). Hypertree proof search for neural theorem proving. arXiv preprint. https://arxiv.org/abs/2205.11491

  • Haiming Wang, Ye Yuan, Zhengying Liu, Jianhao Shen, Yichun Yin, Jing Xiong, Enze Xie, Han Shi, Yujun Li, Lin Li, Jian Yin, Zhenguo Li, and Xiaodan Liang. 2023. DT-Solver: Automated Theorem Proving with Dynamic-Tree Sampling Guided by Proof-level Value Function. Association for Computational Linguistics.https://aclanthology.org/2023.acl-long.706/

  • Albert Q., Jiang., Sean W., Jin Peng Z., Wenda L., Jiacheng L., Mateja J., Timothée L., Yuhuai W., & Guillaume L. (2023) Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal  Proofs. arxiv preprint.https://arxiv.org/abs/2210.12283

  • Xueliang Z., Wenda L., Lingpeng K. Decomposing the Enigma: Subgoal-based Demonstration Learning for Formal Theorem Proving.arXiv preprint .https://arxiv.org/abs/2305.16366




本次分享与读书会主题之间的关系




 • 与读书会之间的关系：
与读书会之间的关系：本次主讲内容重点介绍了AI+Math的背景以及已取得的理论和实践成果，揭示了AI与Math的紧密联系以及未来可能的研究发展方向。

 • 与复杂系统之间的关系：
数学结构本身可以看作一个复杂系统，数学对象构成了相互关联的复杂系统。另一方面，复杂科学的研究也离不开数学工具。混沌、非线性等既是重要的数学概念，也是复杂科学的基础概念。人工智能技术的深入发展，将进一步加强数学与复杂科学的深刻联系，同时，数学与复杂科学的方法正逐步在人工智能的发展研究中发挥重要作用，并为构建神经网络与大模型的可解释性提供坚实的理论基础，通过人工智能与数学研究结合可以为复杂系统与人工智能的结合带来更多可能性。




直播信息




时间：

2023年11月3日（本周五）晚上20:00-22:00


参与方式：
扫码参与人工智能与数学读书会，加入群聊，获取系列读书会回看权限，成为AI+Science社区的种子用户，与社区的一线科研工作者与企业实践者沟通交流，共同推动AI+Science社区的发展。


人工智能与数学读书会启动


人工智能与数学读书会主要围绕AI　for　math，math　for　AI两个方面深入探讨人工智能与数学的密切联系。首先，我们将概述人工智能在数学的应用，并深入探讨大模型与数学推理，定理自动证明， AI发现数学规律，符号计算等方向的研究工作。随后，我们将转向大模型与神经网络的数学基础。最后，我们将深入探讨几何与拓扑在机器学习的应用。人工智能与数学读书会自2023年9月15日开始，每周五晚上20:00-22:00举办，持续时间预计 8 周。欢迎对本话题感兴趣的朋友报名参加！



详情请见：

人工智能与数学读书会启动：AI for Math，Math for AI



点击“阅读原文”，报名读书会