利用机器智能生成数学猜想

Jun, 2023

Mathematical conjecture generation using machine intelligence

Challenger Mishra, Subhayan Roy Moulik, Rahul Sarkar

TL;DR本文提出了一种利用机器智能在数学数据中找到抽象模式生成数学不等式的猜想的系统方法，以 < f<g 类型的严格不等式为重点研究对象，并将它们与一个向量空间相关联，并在这个称为猜想空间的空间中执行几何渐进式下降算法，生成了有关素数计数函数和非阿贝尔简单群的 Cayley 图直径的新猜想，并突显了该空间中数学发现的重要性和领域专业知识的必要性。

Abstract

Conjectures have historically played an important role in the development of pure mathematics. We propose a systematic approach to finding abstract patterns in mathematical data, in order to generate conjectures about mathematical inequalities, using machine intelligence. We focus on s

machine intelligence mathematical inequalities conjecture space geometric gradient descent mathematical discovery

发现论文，激发创造

从场论到庞加莱猜想的机器学习严谨性

在这篇论文中，我们讨论了如何利用机器学习在自然科学中获得严谨性，通过猜想生成或通过强化学习进行验证，可以使用非严谨的方法得到严谨的结果。我们还描述了受神经网络理论启发的场论新方法，以及通过神经网络梯度下降诱导的黎曼度量流理论，其中包含了 Perelman 的黎曼流公式，该公式用于解决 3D Poincaré 猜想。

Feb, 2024

机器学习和信息论概念对人工智能数学家的贡献

当前人工智能的最新技术在语言方面非常出色，但在数学推理方面则相对不足。本文以数学家的思维方式为参考，建立在当前深度学习在直觉和习惯性行为等方面取得成功的基础上，指出其在推理和稳健性不确定性估计等方面仍存在重要缺陷。文中以信息论的观点探讨了什么样的数学陈述是有趣的，这可能为塑造高级数学家人工智能的未来工作提供指导。重点不是证明给定的定理，而是发现新奇的猜想。核心假设是，一个有用的定理组应更好地总结所有可证陈述的集合，例如通过具有较小的描述长度，同时在推导步骤的数量上接近许多可证陈述。

Mar, 2024

算法辅助发现数学常数之间的内在顺序

通过计算机算法发现大量连分数公式，并揭示了保守矩阵场这一新颖数学结构，统一了现有的数学公式，生成了无穷多个新公式，并引发了不同数学常数之间的意想不到的联系，同时可以用于证明无理性定理。实验证明了大规模计算方法在攻克长期悬而未决的问题并发现不同科学领域之间的意外联系中的潜力。

Aug, 2023

数学代理：计算基础设施、数学嵌入和基因组学

该研究利用生成式人工智能、数学代理、数学嵌入等方法解决信息系统生物学领域的老化问题，并应用多尺度物理数学和基因组数据来分析疾病模型和基因组数据，以探索未解决的阿尔茨海默病问题。

Jul, 2023

基于约束求解的合成几何陈述和证明的自动补全方法

通过使用合一逻辑和约束求解，我们提出了一个框架，用于补充不完整的猜想和证明。该框架可以将具有缺失假设和不明确目标的猜想转化为正确的定理，并帮助完成草图式证明以使其适于人类阅读和机器检查。

Jan, 2024

学会简单

运用机器学习从数学上的结构化数据中了解有限群，并得出关于有限单群生成元必要属性的定理，通过使用浅层前馈神经网络对所有 n 个对象的对称群的二元子群进行分类，验证这种神经网络分类器可以根据特征以不同的准确率识别简单性属性，新的玩具定理关于有限单群生成元的必要属性进行评论，对一类稀有群成立的结果进行了明确展示，表明了纯数学中代数结构机器学习的研究可行性，并凸显出借助于机器学习在数学中生成新的猜想和定理的可能性。

Dec, 2023

首个神经推测数据集和实验

该文章介绍了使用神经方法创建猜想的数据集和实验，使用转换器架构中的 GPT-2 模型，其中数据集基于多种处理过的 Mizar 数学库和 MPTP 系统提取的问题，并通过 ENIGMA 指南使用 E 证明器证明。

May, 2020

广义高维线性反问题的几何推断

该论文提出了一个几何统计分析框架，适用于泛化的不适定线性反问题模型，包括噪声压缩感知、符号向量恢复、迹回归、正交矩阵估计和噪声矩阵完成等特殊情况，提出了可行的计算凸规划方法，用于统计推断，包括估计、置信区间和假设检验。该论文建立了一个理论框架，以表征局部估计收敛速度，并提供统计推断保证，其结果基于局部锥几何和对偶性，并通过高斯宽度和 Sudakov 最小化估计量表征局部切锥的几何。

Apr, 2014

具有正交约束的算法几何学

本文介绍了关于 Grassmann 和 Stiefel 曼陀罗上的一些新的数值线性代数算法，具有优秀的性能表现，并可用于对称特征值问题、非线性特征值问题、电子结构计算和信号处理等领域中出现的约束条件进行建模。

Jun, 1998

从内在动机学习形式数学

通过构造一个 agent，它能够自我产生推测和证明，我们探索了从自有公理中探索数学的方法。使用约束解码和类型导向综合的方法，我们在依赖类型理论中对数学领域进行公理化，从中采样有效的推测，同时使用相同的模型生成策略和价值函数来引导证明搜索，从而生成难以证明但可证明的猜测，agent 能够从公理开始自我提高，并通过在证明搜索树上应用回顾重新标记等创新方法显著提高其样本效率，实验证明我们的 agent 能够从只有公理开始，自我提高产生真实且具有挑战性的猜测和找到证明。

Jun, 2024