机器证明主要需要解决三个问题。首先是知识表示,即用何种语言描述问题和定理;其次是知识更新,即给定由旧知识到新知识的规则;最后是如何通过对规则进行控制来找到证明。本文以初等数学中表达式化简类人过程生成为背景,对这三个问题进行了研究。一、知识表示问题。本文将初等数学中的知识表示为实体和关系,并以此为基础构建了初等数学概念知识图谱。其中,概念知识图谱包含实体551个,关系561条,三元组204763个。同时,将表达式用表达式树的形式进行表示以用于表达式化简变形。最后,将推理的规则用类人语言进行描述,构建了包含655条推理规则的规则库。二、知识更新问题。本文提出了基于表达式树匹配的表达式变形方法以及三元组匹配更新实体和关系的方法。通过将类人描述的规则与表达式化简题目进行匹配,匹配成功后,将依据规则对知识库进行更新。三、规则控制问题。表达式的化简变形方式多样,每一步化简变形操作都将对下一步产生影响,因此容易产生组合爆炸问题。为了让表达式实现“好”的变形,基于BERT训练了一个用于评判表达式优劣的神经网络模型。该模型将用于基于A*算法实现的表达式多步化简变形。在改进的A*算法中,神经网络模型被视为估价函数,每一个与当前表达式匹配的规则相当于A*算法中一条可扩展的路径。通过上述算法,解决了通过控制规则找到证明路径的问题。本文研究的课题使用了知识图谱、自然语言理解、类人答题等前沿技术,构建了一个表达式类人化简系统。本文选取了 280道初等数学的表达式化简和不等式证明题目,用于该系统的类人解答过程生成测试。该系统在上述测试中达到了72.50%的准确率。