我们构建了一种神经符号系统，利用神经部分（HyperGNet）根据超树预测定理，并利用符号部分（FormalGeo）应用定理和更新超树，从而形成了一个可追踪的、可读的几何问题自动求解的预测 - 应用循环，实现了 87.65% 的逐步准确率和 85.53% 的总体准确率。

Feb, 2024

在过去十年的工作中，我们构建了一个完整且兼容的平面几何形式系统，该系统在 IMO 级别的平面几何挑战和可读的 AI 自动推理之间建立了重要的桥梁。通过这个形式系统，我们成功地将现代 AI 模型与形式系统无缝整合。在这个形式框架内，AI 能够像处理其他自然语言一样，为 IMO 级别的平面几何问题提供演绎推理解决方案，并且这些证明是可读、可追溯和可验证的。我们提出了几何形式化理论（GFT）来指导几何形式系统的发展。根据 GFT，我们构建了 FormalGeo，它包含 88 个几何谓词和 196 个定理，可以表示、验证和解决 IMO 级别的几何问题。我们还使用 Python 开发了 FGPS（形式几何问题解决器），它既可作为交互式助手验证问题解决过程，又可作为自动化问题解决器利用前向搜索、后向搜索和 AI 辅助搜索等多种方法。我们标注了 FormalGeo7k 数据集，其中包含 6,981 个几何问题的完整形式语言注释（通过数据增强扩展为 186,832 个问题）。对形式系统的实施和对 FormalGeo7k 的实验验证了 GFT 的正确性和实用性。后向深度优先搜索方法只有 2.42% 的问题解决失败率，而我们可以结合深度学习技术实现更低的失败率。FGPS 和 FormalGeo7k 数据集的源代码可在此 https URL 获取。

Oct, 2023

提出了一个名为 DualGeoSolver 的双重推理几何求解器，通过模拟人类的双重推理过程，从对人类推理过程和知识应用的显式建模中提高求解几何问题的准确率和鲁棒性。

May, 2024

应用现代人工智能技术解决几何问题和自动演绎证明一直以来都是数学和人工智能交叉领域的重要挑战。本文提出了一种名为 FGeo-P 的定理预测器，利用语言模型预测几何问题的定理序列，从而提高了解决几何问题的性能，实验证明在 FormalGeo7k 数据集的问题解决率从 39.7% 提升至 80.86%。此外，FGeo-TP 在不同难度问题上表现出了解决时间和搜索步骤显著减少的特点。

Feb, 2024

构建了一个大规模的几何问题的数据集，并提出了一种基于形式语言和符号推理的新的解决方案，称为可解释几何问题求解器 (Inter-GPS)，其能够显著提高当前方法的解决几何问题的效果。

May, 2021

该研究提出了一个神经和符号端到端强化学习架构，能够克服当前深度学习技术的局限性，如需要非常大的数据集工作、难以实现高级认知功能和透明性欠佳等。研究者以简单的视频游戏为例，展示了这个架构的实现原型，结果表明它能够有效地学习，并通过获得一组符号规则，可将性能提高到比传统完全神经强化学习系统更好的水平。

Sep, 2016

该研究提出了一种基于命题逻辑的生成模型 (LoGe)，它提供了更高效的生成抽象推理答案的方法，并在 RAVEN 基准测试中超越了黑盒深度神经网络的表现。

Jul, 2021

提出了一种定理证明算法，该算法使用几乎没有领域启发式来指导其连接风格的证明搜索，而是运行许多蒙特卡罗模拟，通过强化学习来指导以前的证明尝试。

May, 2018

本文介绍了一个基于深度学习的 EuclidNet 框架，通过视觉推理解决几何构造问题，特别适用于自动化几何定理证明；该框架使用神经网络架构 Mask R-CNN 从初始设置和目标配置中提取视觉特征，并生成可能的构造步骤作为中间数据模型，并反复重复这个过程，直到问题得到解决或被识别为不可解决。最后使用回溯方式得到一个逐步构造指南，并使用日本 Sangaku 几何难题验证了 EuclidNet 框架的有效性。

Dec, 2022

通过统一的几何原理，深度学习可以更好地揭示基本规律，提供数学框架来研究卷积神经网络、循环神经网络、图神经网络和变压器网络等神经网络，且可以将物理学知识结合到神经网络结构中，从而提供了未来神经网络结构的原则性方法。

Apr, 2021