数学知识库与抽象能力的建立

数学知识库与抽象能力的建立Aidam是学霸君自主研发的智能教育机器人，它是以深度学习、专家系统和自然语言理解为核心技术的复杂系统。这个系统的核心在于通过学习人类的解题逻辑，熟悉人类思考和学习方式，进而掌握各种解题方法。据他们统计，高考数学大概有3529个考点，为了解决这些问题，截止2017年5月，学霸君累计解决近80万套试卷、100亿道试题，答疑命中率93%。目前，学霸君已经拥有7000万道数学题目的题库系统，以及大量的学生手写和上传题目图片、各种教辅书籍中的题目库，这些构成了学霸君的智能机器人的训练数据。目前，依靠学霸君的产品端的日申请量，每天可以产生1800万张左右的题目图片上传。而其中，无论是拍照，还是学生手写题目，均可以被Aidam的图像识别系统正确识别，并记录、收集、标记。在学霸君的题库中，每一道题目均记录了其答案、解析和不同的解题方法。在此基础上，Aidam不断进行自动解题训练。“系统每天大概做40-50万道题目。”在超链路神经网络使用的时候发现，它对于记忆题目使用的步骤跟逻辑是有价值与效果的，所以开始大规模地在代数体系跟解析体系解决这个问题。“棋有棋谱、题有题路”，依靠机器学习技术，在系统层面开始有机会，像人一样将数学题目一步步推理做出来。无论这道题目是否在系统中录入过，无论它的难度系数有多高，只要在它的知识范围内，都是可以完成的。通过运用包括题库，概念实体库，定理库，可以形成一个完整且高效的知识数据库，同时整合Maple等四大数学软件，运用自动推理机进行运算，综合运用有监督学习和无监督学习来训练机器，就会形成一个更高正确率的概率分布输出。毛主席说集体的力量是无穷的，目前在研发高考机器人的过程中，最大的挑战其实来自于如何把各种异构的数据、各种形态的数据、各种解题API和解题策略套路整合到一套代码里面。希尔伯特计划与高考数学题的语言形式化三大数学流派包括逻辑主义、形式主义和直觉主义，形式主义的奠基人是希尔伯特，他区分了三种数学理论。一是直观的非形式化的数学理论；二是将第一种数学理论形式化，构成一个形式系统；三是描述和研究第二种数学理论的，称为元数学、证明论或元理论。他的的主要思想就是要奠定一门数学的基础，应该先用严格的数学来证明它的协调性。希尔伯特计划的数学内容就是数理逻辑中的证明论，其主要目标是为全部的数学提供一个安全的理论基础。这个基础应该包括所有数学的形式化。意思是，所有数学应该用一种统一的严格形式化的语言，并且按照一套严格的规则来使用。元数学是以形式系统为研究对象的一门新数学，它包括对形式系统的描述、定义，也包括对形式系统性质的研究。形式主义者认为数学的公理系统或逻辑的公理系统，其中基本概念都是没有意义的，其公理也只是一行行的符号，无所谓真假，只要能够证明该公理系统是相容的，不互相矛盾的，该公理系统便得承认，它便代表某一方面的真理。另外逻辑公理系统也被认为是没有内容的，不能由内容方面保证其真理性，于是便只留下“相容性”作为真理所在了。目前理论上可以运用NLP中的多项工具，把所有的高考数学题都写成计算机理解的形式化符号。最后高考题目都是有解的，所以我们就不用考虑该死的哥德尔不完备性啦。直接把数学题目中的基本概念转换为形式系统中的初始符号，命题转换为符号公式，推演规则转换为符号公式之间的变形映射关系，证明转换为符号公式的有穷序列，再利用机器学习或神经网络中训练好的各种专家系统或推理特征值编出解题步骤，然后就可以交给mathmatica等四大数学软件了。当然，如果不是要考150的话那么，这个智能系统就基本开发完毕了。怎么样？有点小激动吧！

理解题目的意思和意图把用自然语言表述的数学试题转化为的数学形式化语言是关键一步。实践中可以运用encode-decode模型作为编程框架，完成编译与反编译（高考卷的输入输出）。由于机器学习问题是一个与问题域紧密相关的问题,所以不能简单照搬现有的NLP应用API,而是应该针对数学试题的语言特点生成有针对性的问题模板并在日常的学习中加以泛化与正则化。学术的说法就是把开放无限域的自然语言表达转化为有限域的特定问题。目前自然语言处理主要包括三种技术。第一种是基于规则的专家系统，第二种是基于统计的贝叶斯方法。第三种是基于神经网络的深度学习方法。这三种方法各有利弊，如果能够把这三种方法的优点结合起来，那么对于高考题目的理解就可以达到一个非常高的水平。当前不管是美国的谷歌、亚马逊、脸书还是中国的科大讯飞、百度语音，都已经在自然语言理解方面做出了非常突出的工作。高考机器人之所以在题目理解环节常常失败，个人认为主要是因为他们没有能够完成与这些最优秀人工智能公司API的赋能连接。因此，如果我们国家的学霸君还有成都准星云学公司的高考机器人能够运用上最优秀的自然语言力理解，并且对这些工具进行专业化的二次训练与开发，那么对数学题目的理解与形式化转换就应该不成问题。一个有说服力的事实是，目前中英文、中俄，中韩，中日文的机器翻译已经取得了98%的正确率，这个正确率是超过人类的翻译能力的。而不同语言之间的翻译与把自然语言翻译成形式化数学语言，在某种意义上来说是有很多相通之处的。因此借鉴以上的技术，把自然语言的高考题翻译为形式化的数学符号序列理论上来说应该是没有问题的。如果再能够运用逻辑反推或者反向传播的机器学习技术，准确率应该会更高。机器人的解题过程与核心技术简介智能机器人的解题过程大致可以分为三个步骤。首先是识别并理解人类语言，即通过图片信息识别模块和自然语言处理模块将人类语言转换为逻辑形式语言。其次是逻辑推理与计算，利用计算机的知识库（知识图谱、知识语义网络）、推理机模拟人类处理信息的方式和策略，找出最佳解题路径。最后是用人类的语言回答问题，并给出详细的解题步骤，即将形式语言转化为自然语言。其中NLP中的场景语义分析是系统的核心问题之一。高考机器人首先需要运用图像识别模块把由图像扫描输入的图片信息转化为文字符号信息。目前市场上有众多成熟的OCR技术产品可供使用，即使是针对特别潦草的手写图片，也可以通过生物信息学技术解决。具体的解决方法是首先收集、标注大量图片，同时搭建GPU集群平台来训练深度神经网络，然后对生成模型来做进一步优化。第二步就是对每一道考题进行自然语言处理，首先是正确理解题目的意思和意图，然后把它转化成形式化的数学语言。简单来说就是已知什么求什么。第三步同时运用多功能推理机，调用系统的数学知识库和maple等计算引擎的API来解题。最后就是输出答案了，这一部分所需的技术与第一步基本相同，但可能需要借鉴一些问答系统中的对话管理方面的技巧，确保不出现答非所问的情况。另外运用作业帮、学霸君等公司的搜索题库解题，或者用经过训练的深度学习神经网络解题也都是有希望的技术路径。自动答