#挑战30天在头条写日记#

#数学#​#数学证明##让AI触手可及#​#人工智能#​#chatGTP人工智能#​

AI的发展，出现了一些专门擅长数学定理自动证明输出证明过程的AI。这些AI未来与数学物理发展和AI进化相互促进

目前一个比较有代表性和影响力的AI模型是GPT-f，它是由OpenAI研究者Stanislas Polu和Ilya Sutskever在2020年发布的一个基于Transformer的自动定理证明模型 。

GPT-f可以用来解决Metamath库中的数学问题，并生成形式化的证明过程 。

Metamath论坛总共有约23,000个基础的需证明的定理 。这些定理涵盖了从ZFC集合论公理开始，到各种数学分支和结构的内容。每个定理都有完整的证明过程，可以用一个简单的替换规则来验证 。GPT-f是一个人工智能模型，它可以自动证明Metamath当中的一些定理。目前，GPT-f只能证明Metamath当中23个定理并被收录到Metamath数据库中 。这只占总数0.01%。GPT-f还需要不断地学习和改进。

GPT-f利用了大语言模型，如ChatGPT，来进行数学和科学问题的定量推理，并借助交互式定理工具如COQ来辅助大模型进行精确数学推理 。

GPT-f最佳模型实现Metamath56.22%的保留测试集，而目前最先进的MetaGen-IL只有21.16%的证明能力 。

除了GPT-f之外，还有一些其他的AI模型也在尝试实现数学定理自动证明输出证明过程，目前主要有Metamath和miniF2F两个测试数据集进行数学证明AI评测。

• Metamath：一个包含了基于ZFC集合论的约38000个证明的形式数学社区 。Metamath提供了一个统一的形式化语言和一个自动验证器来检查证明的正确性。Metamath可以用来测试数学证明AI从非形式化语言到形式化语言的自动翻译能力。

• miniF2F：一个包含了1000个基于F2F（Freek Wiedijk's Formalizing 100 Theorems）项目选出的定理及其非形式化证明 的数据集。miniF2F提供了一个基于Isabelle/HOL形式化系统 的自动定理证明器来验证证明草图中缺失细节。miniF2F可以用来测试数学证明AI从非形式化语言到形式化草图到完整形式化证明的自动生成能力。

目前在Metamath和miniF2F上取得最好成绩的数学证明AI是GPT-f ，它是由OpenAI研究者Stanislas Polu和Ilya Sutskever在2020年发布的一个基于Transformer 的自动定理证明模型。

GPT-f利用了大语言模型ChatGPT 来进行数学和科学问题的定量推理，并借助交互式定理工具如COQ 来辅助大模型进行精确数学推理。GPT-f在Metamath上可以自动证明23个定理，并被收录到Metamath数据库中 ；在miniF2F上可以完成测试集中56.5%的证明 。

除了GPT-f之外，还有一些其他的数学证明AI也在进行测评和比较，例如：

• MetaGen-IL：一个基于元学习和强化学习的自动定理证明模型，它可以从少量的形式化数据中学习，并在不同的形式化系统中迁移。MetaGen-IL在Metamath上可以自动证明21个定理 ；在miniF2F上可以完成测试集中21.2%的证明 。

• HTPS：一个基于Transformer和自监督学习的自动定理证明模型 ，它可以从大量的非形式化数学数据中学习，并生成形式化证明草图。HTPS在Metamath上可以自动证明16个定理 ；在miniF2F上可以完成测试集中32.8%的证明 。

• Meta Blog：一个基于Transformer和元学习的自动定理证明模型，它可以从少量的形式化数据中学习，并生成形式化证明草图。Meta Blog在Metamath上可以自动证明15个定理；在miniF2F上可以完成测试集中30.7%的证明。