使用大型语言模型进行形式化 / 非形式化及自然论证练习，面向初学者
使用大型语言模型进行科学综合、推理和解释，通过从科学文献综合知识，将其应用于预测分子属性等任务，提高了当前机器学习系统的性能，并能解释其预测结果，将加速科学发现的进程。
Oct, 2023
该研究采用深度神经网络进行数学形式化的自动化，使用机器翻译模型将非正式的 LaTeX 写的 Mizar 文本转化成正式的 Mizar 语言，并进行了多次实验以测试其可行性。结果表明，通过人工神经网络进行数学形式化是一种有前途的方法。
May, 2018
通过提出一种新的流程，我们利用合成数据来将自然语言数学问题转化为 Lean 4 语句，并相应地进行过滤，从而为解决 LLMs 在理解复杂数学问题和证明上的性能提供有用的训练数据。最终数据集包含约 57K 个正式 - 非正式问题对以及来自数学竞赛论坛的搜索证明和 21 个新的 IMO 问题。
Jun, 2024
大语言模型在多步数学推理方面表现出色，但包含文字和图像的数学推理问题需要评估视觉语言模型的推理能力。通过几何问题的镜头，我们通过多个角度评估视觉语言模型的推理能力。我们创建了一个合成的几何问题数据集，具有可控的难度级别，从而进行系统评估。我们的基准测试结果表明，这些模型在几何等主题的推理能力上并不如先前的基准测试所暗示的那样出色，特别是通过我们基准测试的多个深度级别构建，因为解决更深的问题需要更长的推理链而不是额外的记忆知识。我们释放这个数据集供进一步研究使用。
Dec, 2023
本文旨在通过实验探讨利用神经网络自动将 LaTeX 格式的非正式数学语句翻译成 Mizar 语言中的正式数学陈述。研究通过监督和非监督方法训练了三个基于神经网络的机器翻译模型，并开发了自定义的类型详细说明机制来优化结果。
Dec, 2019
本研究使用大型语言模型 (Codex) 探讨将使用自然语言书写的数学（即定义，定理陈述和证明）转化为可以被程序检查正确性的形式语言的能力，并发现对于 120 个定理，Codex 可以在本科水平上以近 75％的准确率进行短数学陈述的形式化。同时在选择合适的输入和后处理策略下，Codex 可以以自然语言形式翻译本科水平的 13 个定理的证明，这些具有两到三自然段长度的证明可以在 12 次中有至少一次完成翻译，这表明大型语言模型是完全或部分自动化形式化的有前景的途径。
Nov, 2022
通过一个包含系统 1 和系统 2 的双系统，本论文提出了一种用于多步骤多模态推理的方法，其中系统 1 用于提取视觉信息，系统 2 用于深入推理。通过实验证明，我们的方法在图表数据集上与之前的工作相比表现出竞争力，在多步骤推理的少量数据上通过微调系统 2 模块（LLaMA-2 70B），我们的方法的准确性得到进一步提升，并在具有人工提出问题的挑战性数据集上超过最佳全监督端到端方法 5.7% 以及具有 FlanPaLM（540B）的流水线方法 7.5%。
Oct, 2023
本论文展示了一个结合多个大型语言模型的智能代理系统，可自主设计、规划和执行科学实验，并通过三个不同的实例展示代理的科学研究能力，最为复杂的是成功执行加催化交叉偶联反应。最后，讨论了这种系统的安全影响，并提出了防止滥用的措施。
Apr, 2023
大型语言模型在科学计算应用中的应用领域和研究进行了概述，重点突出了涉及科学文献和描述物理系统的专用语言的自然语言处理的使用案例。在医学、数学和物理学领域，聊天机器人样式的应用可以与领域专家进行迭代，进行问题解决。同时，我们还对分子生物学中的专用语言进行了审查，这些语言包括分子、蛋白质和 DNA 的使用，语言模型被用于预测特性，甚至以比传统计算方法快得多的速度创建新型物理系统。
Jun, 2024