谷歌 Minerva & Autoformalization 项目原作解读-静雅生活网

导读：以下文章来源于机器之心 SOTA 模型，作者 SOTA 模型　　自动证明数学定理是人工智能的一个初衷，也是一直以来的难题（a long-standing problem

　　以下文章来源于机器之心 SOTA 模型，作者 SOTA 模型

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

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

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

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

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

谷歌 Minerva & Autoformalization 项目原作解读

　　分享主题：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/