若干离散几何问题及反问题的机器证明与可解释性研究

用计算机处理离散数据并在问题的可行解集找出最优解一直是计算机科学的重要组成部分。而在求解过程中的机械化算法构建，早已成为机器证明的重要分支。另一方面，随着图神经网络显示出的巨大潜力，可推理可解释的机器学习模型成为人工智能领域正在寻找的下一代智能范式。本项目将聚焦于用符号计算、数值计算与图神经网络结合的机械化算法求解离散几何中有代表性的几个公开问题及其反问题，如Thomson问题(n≥7)，Tammes问题，Erdos-Szekeres问题等；并致力于改进和推广层相关度传播、深度泰勒分解等算法，给出上述机器证明模型的可解释性。因此，本项目也是对符号学派和联结学派融合与交叉的一次探索。获得这些有难度的离散几何公开问题解答不仅本身有积极的数学意义，推进过程中可能产生的一些新的理论和方法也将是计算机科学领域正在引起重视的创新试验而有着很好的应用前景。

It has always been an important part of computer science to process mass discrete data by computers and find the optimal solution from the feasible solution set of the problem. As well, the mechanized algorithm construction plays a vital role as the branch of machine proof. Meanwhile on the other hand, following the enormous potential of graph neural network shown in previous works, reasonable and interpretable machine learning models are also the next-generation intelligence paradigm that the field of artificial intelligence is looking for. We will focus on solving several open problems and related inverse problems in discrete geometry with mechanization algorithms combining symbolic-numerical hybrid computation and graph neural network, such as Thomson problem(n≥7), Tammes problem, Erdos-Szekeres problem, etc. Furthermore, we will work on improving and generalizing algorithms such as Layer-wise Relevance Propagation and Deep Taylor Decomposition, and gives the interpretability of the above machine proof model. Therefore, this project can be considered as an exploration of the fusion and intersection of the symbolist and the connectionist. Obtaining answers to these open questions with significant difficulty of discrete geometry not only has positive mathematical impact in itself, but also some new theories and methods that may arise in the process of advancing will also be innovative experiments that are attracting attention in the field of computer science and have promising application prospects.