AI for mathematics | 谷歌Minerva & Autoformalization项目原作解读

自动证明数学定理是人工智能的一个初衷，也是一直以来的难题（a long-standing problem of AI）。近年来人工智能的发展让我们渐渐意识到自动证明变成一种可能。尤其是近几年的大语言模型，更加让我们对现有智能的推理能力抱有很大的期望。

到目前为止，人类数学家使用了两种不同的方式来书写数学。第一种是大家都熟悉的方式，即用自然语言来描述数学证明。大部分的数学都是以这种方式书写的，这包括我们的数学课本，数学论文，等等。这个形式的数学虽然非常灵活，但它的问题是证明的正确性一般很难检验。

第二种称之为形式化数学（formal mathematics）。这是近半个世纪计算机科学家创造的，用来检验数学证明的一种工具。数学家可以在这样的一个程序里写数学证明，而证明的正确性可以被形式化证明系统来检验。但这个方式来证明数学定理并不常用，因为在形式化证明系统里要书写的数学证明要比在一般情况下的证明复杂的多。

两种不同形式的数学各有千秋，而真正的有意思的研究问题便在于如何结合两种数学的优点去创造一个伟大的数学智能。

机器之心最新一期线上分享邀请到了谷歌研究科学家吴宇怀（Yuhuai Tony Wu），介绍他们在 AI for mathematics 领域取得数学智能 SOTA 的探索。

分享主题：AI for mathematics ｜ 数学智能 SOTA：Minerva & Autoformalization

分享嘉宾：吴宇怀 (Yuhuai Tony Wu)，谷歌研究科学家，斯坦福博士后，多伦多大学博士。立志于创造一个善于推理的人工智能，用于解决所有数学难题。

分享摘要：我们从 Minerva开始说起。Minerva 是一个大语言模型。当训练在足够多的数学相关的数据之后，我们发现它的数学能力非常强，可以在波兰、英国高中数学测试中拿到高于平均分的分数。然而这样的语言模型也有不足，它只能模仿，而不能自主训练而提高数学水平。形式化证明系统(formal proving systems)提供了一个训练环境，但形式化数学的数据非常少。因此我们需要自动形式化（autoformalization）来作为一个桥梁连接自然语言数学。接下来的讨论也就会关于如何用大语言模型来帮助我们做这个桥梁，从而享用两种方式的优点（enjoy the best of both worlds）。

相关链接：

1.Solving Quantitative Reasoning Problems with Language Models, NeurIPS, 2022.

论文地址：

https://arxiv.org/abs/2206.14858

Google blog: 

https://ai.googleblog.com/2022/06/minerva-solving-quantitative-reasoning.html 

2.Autoformalization with LLMs, NeurIPS, 2022

论文地址：

https://arxiv.org/abs/2205.12615 

Media coverage: 

https://www.newscientist.com/article/2322999-ai-translates-maths-problems-into-code-to-make-them-easier-to-solve/ 

https://trustmyscience.com/ia-permet-automatiser-traduction-enonce-probleme-code-informatique/ 

3.Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs

论文地址：

https://openreview.net/forum?id=SMa9EAovKMC 

加群看直播

直播间 ： 关注机器之心机动组视频号，北京时间 10 月 26 日 10:00 开播。

交流群： 本次直播设有 QA 环节，欢迎加入本次直播交流群探讨交流。

如群已超出人数限制，请添加机器之心小助手：syncedai2、syncedai3、syncedai4 或 syncedai5，备注「Minerva」即可加入。

如果你也有最新工作希望分享或提交你感兴趣的内容方向，随时告诉我们吧： https://jiqizhixin.mikecrm.com/fFruVd3

机器之心 · 机动组

机动组是机器之心发起的人工智能技术社区，聚焦于学术研究与技术实践主题内容，为社区用户带来技术线上公开课、学术分享、技术实践、走近顶尖实验室等系列内容。 机动组也将不定期举办线下学术交流会与组织人才服务、产业技术对接等活动，欢迎所有 AI 领域技术从业者加入。