CAREER: Automated Reasoning to Advance Chemical Theory

在化学系(CHE)和高级网络基础设施办公室(OAC)化学理论、模型和计算方法(CTMC)计划的共同支持下，巴尔的摩县马里兰大学(UMBC)的泰勒·约瑟夫森(Tyler Josephson)正在开发一种在计算化学中编写代码的新方法。在测试新算法时，确保它们被正确编码是很重要的。LEAN是一种编程语言，可以帮助检查数学证明是否正确。约瑟夫森的实验室--密歇根大学人工智能与理论导向的分子科学(ATOM)实验室--将使用并教授其他人使用精益编写精益推导和模拟软件，以确保数学和代码是正确的。他们将开发LeanMD(精益分子动力学)软件来模拟分子的运动，该软件的设计没有错误和数学错误。该项目将扩展到SciLib，这是一个来自社区的证据图书馆，涵盖了科学和工程的所有领域。其他人可能会使用这些证据来探索科学文献并验证他们自己的证据，从而加速新理论的发现。社区大学的外展活动和为本科生研究招募转校生将支持多样化的STEM(科学、技术、工程和数学)劳动力。与微软研究院精益开发人员的跨学科合作有望促进学生的学习和专业发展。计算机科学家使用交互式定理证明器来验证数学和软件，但它们很少用于科学计算。LEAN是由微软研究院(MSR)开发的一种现代定理证明器和编程语言，旨在使数学家能够定义高级数学对象并证明有关它们的语句。泰勒·约瑟夫森的研究小组--AI&Amp；面向理论的分子科学(ATOM)实验室正在探索如何将经典力学和分子动力学(MD)的数学转化为Lean代码(定义哈密顿和牛顿运动方程，以及Verlet算法等可计算表达式，并证明它们之间的关系)，并使用这些代码来构建LeanMD，正式验证的MD软件。这是创建SciLib的第一步，这是一个科学和工程方面的开放源码证明库，类似于Lean的社区源码数学库Mathlib。大型证据数据库可用于评估大型语言模型(LLM)，用于自动完成证据(由精益编译器提供验证)、将非正式科学转换为正式证据(反之亦然)，以及用于生成、证明和解释新理论。为了向科学家和工程师讲授精益，原子实验室正在计划举办年度培训研讨会，参与度由成员对本实验室的持续贡献来衡量，以及互动在线游戏，精益内置的游戏向非数学家介绍定理证明和精益语言。该奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

With joint support from the Chemical Theory, Models and Computational Methods (CTMC) program in the Division of Chemistry (CHE) and the Office of Advanced Cyberinfrastructure (OAC), Tyler Josephson of the University of Maryland, Baltimore County (UMBC) is developing a new approach to writing code in computational chemistry. It is important when testing new algorithms that they be coded correctly. Lean is a programming language that can help check whether math proofs are correct. Josephson's lab, the AI & Theory-Oriented Molecular Science (ATOMS) Lab at UMBC, will use and teach others to use Lean to write derivations and simulation software in Lean, ensuring that the math and code is correct. They will develop LeanMD (Lean-molecular dynamics) software for simulating the motion of molecules, that is designed to be free of bugs and math errors. This project will expand to SciLib, a community-sourced library of proofs across all fields of science and engineering. Others may use these proofs to probe the scientific literature and verify proofs of their own, accelerating the discovery of new theories. Community college outreach activities and recruitment of transfer students for undergraduate research will support a diverse STEM (science, technology, engineering and mathematics) workforce. Cross-disciplinary collaboration with the developers of Lean at Microsoft Research is anticipated to foster student learning and professional development. Computer scientists use interactive theorem provers to verify mathematics and software, but these are scarcely used in scientific computing. Lean, a modern theorem prover and programming language developed by Microsoft Research (MSR), is designed to enable mathematicians to define high-level mathematical objects and prove statements about them. Tyler Josephson's research group, the AI & Theory-Oriented Molecular Science (ATOMS) Lab, is exploring how to translate the mathematics of classical mechanics and molecular dynamics (MD) into Lean code (defining the Hamiltonian and Newton's equations of motion, as well as computable expressions like the Verlet algorithm, and proving relationships between them), and use these to build LeanMD, formally-verified software for MD. This is the first step toward creating SciLib, an open-source library of proofs in science and engineering, similar to mathlib, Lean's community-sourced mathematics library. A large database of proofs can be used to evaluate large language models (LLMs) for auto-completing proofs (with verification provided by the Lean compiler), translating informal science into formal proofs (and the reverse), and for generating, proving, and explaining new theories. To teach Lean to scientists and engineers, the ATOMS Lab is planning annual training workshops, with engagement measured by members' sustained contributions to SciLib, as well as interactive online games, built in Lean, that introduce theorem proving and the Lean language to non-mathematicians.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.