新智元报道
编辑:好困 桃子文档地址:
https://docs.google.com/document/d/1kD7H4E28656ua8jOGZ934nbH2HcBLyxcRgFDduH5iQ0/edit正如文档所介绍,「这是为那些希望涉足数学AI领域的人士准备的初步资源列表」。去年,美国国家科学院「AI辅助数学推理」研讨会期间发起了这份清单行动。它是由UIUC的助理教授Talia Ringer进行了整理。据介绍,这份清单还不是最终版。每个人都可以针对文档内容进行编辑和评论。从修改批注中可以看出,陶哲轩本人贡献了自己的一份力量。有网友表示,「不仅我需要这个,我的学生们也会失去理智」。目录
- 形式化证明
- 机器学习维基和词汇表- 编程语言
- 数学教程- 形式化证明
- 形式化证明的机器学习
- 机器学习课程资料- 「自动化证明」,Talia Ringer
- 「形式化数学」,Kevin Buzzard
- 「机器学习」,吴恩达
- 面相职业数学家的机器学习
- 宾夕法尼亚大学软件基础课程
- Lean教学和课程网页
- 「实分析」,Patrick Massot
- 「逻辑验证指南」,Anne Baanen
合作- PyTorch
- Tensorflow
- JAX证明助手AI在数学领域的一个研究方向是结合AI自动化技术和机器可验证的证明。以下是一些可以用于编写的工具列表:- Lean
- Coq
- Isabelle
- HOL4
- HOL Light
- Agda
- Cubical Agda约束求解器计算数学工具数学数据库集成AI数学工具数据集和基准测试下述资源可以作为训练数据或用于评估性能。部分资源提供了标准的训练/测试划分,而部分则没有。在构建任何工具时,务必注意避免让测试数据污染训练集,以保证结果的有效性。另外,HuggingFace提供了众多公共数据集和基准测试套件,是一个值得查看的好资源。语言模型和聊天机器人AI工具若能被托管机构之外的人下载,通常会被标为「开源」。然而,这些工具往往伴随着严格的使用和分发限制。以下内容将会按照OSI的定义,使用「自由和开源」这个术语。对于那些标为「公开可用」的模型,使用前务必仔细阅读其许可协议,以避免对使用权限的误解。通用模型数学模型形式化证明模型聊天机器人