- 从内在动机学习形式数学
通过构造一个 agent，它能够自我产生推测和证明，我们探索了从自有公理中探索数学的方法。使用约束解码和类型导向综合的方法，我们在依赖类型理论中对数学领域进行公理化，从中采样有效的推测，同时使用相同的模型生成策略和价值函数来引导证明搜索，从 - 数学实体：语料库与基准
本文旨在提供可用于研究数学语言的不同背景下的带有注释的文献资料，并使用神经解析模型和人工干预预处理这些资料，以提供词性标签、词形还原和依赖树。我们评估了几种自然语言处理模型，在从文献资料中提取的基准数据上测试它们的性能，并展示它们在数学领域 - ICLRLean4 中自动形式化的评估基准
大型语言模型 (LLMs) 具有彻底改变自动形式化的潜力。引入数学编程语言 Lean4 为评估 LLMs 的自动形式化能力提供了前所未有的机会。本文介绍了一种专为 Lean4 设计的新型评估基准，将其应用于测试包括 GPT-3.5、GPT- - MathBench：利用分层数学基准评估 LLMs 的理论和应用水平
通过 MathBench 新的基准测试，我们能够全面评估大型语言模型在数学能力方面的表现，首次提供了一个多维度视角，从基础算术到大学数学的不同阶段评估模型的能力，旨在提高对大型语言模型在数学能力方面的评估，为其知识水平和问题解决技能提供更深 - LoRA 学习更少，遗忘更少
通过在编程和数学这两个目标领域上比较 Low-Rank Adaptation (LoRA) 和全精调 (full finetuning) 的性能，我们发现在大多数情况下，LoRA 的表现明显逊于全精调；然而，LoRA 展现了一种理想的正则化 - PARAMANU-GANITA: 具备数学能力的语言模型
Paramanu-Ganita 是一种基于 208 百万参数的全新 Auto Regressive (AR) 解码器的数学语言模型，该模型在数学语料库上进行了从头预训练，在困惑度度量和 GSM8k 数学基准测试中表现出色，优于多个专业和通用 - SIGIRLLM 能掌握数学吗？研究大型语言模型在数学 Stack Exchange 上
本研究通过分析 GPT-4 在回答数学问题中的表现，探讨了大型语言模型在复杂的数学问题解决中的局限性和不足，为未来人工智能驱动的数学推理的研究和进展奠定了基础。
- Graph2Tac: 数学定理证明中的数学概念的分层表示学习
使用新的基于图的数据集进行 Coq 的机器学习，我们提出了 Graph2Tac（G2T）模型，通过考虑以往定义层次与当前目标之间的依赖关系，将新的数学概念整合到模型的知识库中。
- 为教育适应大型语言模型：基本能力、潜力和挑战
基于大型语言模型的教育系统研究，评估其在教育能力方面的潜力，并提出统一和专家混合两种方法构建下一代智能教育系统，同时探讨了挑战和未来发展方向。
- 数学语言模型综述
近年来，在数学领域中，利用语言模型（LMs）取得了显著进展，本文从任务和方法论两个不同的角度对数学 LMs 进行了全面的调查和分类，揭示出大量的数学 LLMs 和超过 60 个数学数据集的应用和研究。
- 数学的人工智能：认知科学视角
人工智能领域的认知科学视角在构建人类或超人类水平的数学系统方面具有重要价值，通过借鉴认知科学的经典和持续研究方向，与人工智能研究人员和数学家的跨学科合作，可以推动数学人工智能系统的进一步发展。
- Llemma: 数学领域的开放语言模型
我们提出了 Llemma 这个大型数学语言模型，通过将 Code Llama 进行预训练得到了 Llemma，并在 MATH 基准测试中表现优于所有已知的开源基础模型，同时还能进行工具使用和形式定理证明而无需进一步微调。
- 物理、数学和计算机科学之间的跨学科互动建模
本论文通过对物理学、数学和计算机科学三个领域的引用流进行建模，并通过时间桶签名对这三个领域之间的引用互动进行量化。基于最近提出的中继链接框架的变体，本文提出了数值模型，试图解开这三个领域之间引用链接形成的基本原理。
- 论将哲学、心理学和数学相结合的思辩学与心测学
本文提出了哲学与心理学与数学相结合的两个概念：philomatics 和 psychomatics，并解释了这种结合的四个动机：满足分析哲学的愿望，提出哲学科学，通过哲学为数学算法提供正当性，以及哲学和数学的抽象。文章举了各种 philom - 使用语言模型隐性自动评估数学简答题
我们提出了一种新的方法来评估数学题的一些简短构建性回答。我们的方法使用一个流程来识别学生回答中指定的关键值，从而确定回答的正确性并发现任何误解。这些关键值的信息可以用于为教师和学生提供反馈，以提供更准确和有用的评估方法，有效改善学生对数学的 - Parmesan 教育数学概念提取
我们开发了一个原型系统 Parmesan，用于在上下文中搜索和定义数学概念，以帮助不熟悉数学概念的研究人员，该系统依赖于自然语言处理组件，包括概念提取、关系提取、定义提取和实体链接技术，并提供了两个修订后的数学语料库。
- 利用大型语言模型探索麻省理工学院数学和电子工程学课程
本文展示了大型语言模型在解决麻省理工学院数学和电气工程与计算机科学课程期末试卷及期中考卷等问题时的表现，GPT-3.5 可成功解决了麻省理工学院三分之一的课程，而经过优化的 GPT-4 在去除图像题后表现完美；同时，作者将该数据集应用于语言 - 考古学中的内在形状分析：对古代日规的案例研究
探索一种新的数学方法从集合相似的物品形状中提取考古洞见。通过在形状空间中执行回归，我们发现罗马日晷的弯曲程度随纬度变化。我们使用这个趋势来推断一个日晷的纬度。同时，还提出了一种基于几何统计和形状分析理论的差异化形态趋势断言方法。
- 聊天机器人在数学和逻辑问题中的应用：ChatGPT-3.5、ChatGPT-4 和 Google Bard 的初步比较和评估
对基于大型语言模型的三个聊天机器人（ChatGPT-3.5、ChatGPT-4 和 Google Bard）进行了比较，重点关注它们解决数学和逻辑问题的能力，并通过一系列测试发现对于简单的算术、代数表达式和基本的逻辑谜题，聊天机器人可能会提 - 揭示思维链背后的谜团：理论视角
研究表明 Chain-of-Thought 提示可以显著改善大型语言模型的性能，特别是在涉及数学或推理的复杂任务中。本文首先对这些问题的潜在机制进行了理论方面的探讨， 然后通过构建的方式证明了带有 CoT 的自回归机器人可以解决基本算术方程