CAREER: Automated Reasoning to Advance Chemical Theory

在化学部（CHE）和高级网络基础设施办公室（OAC）的化学理论，模型和计算方法（CTMC）计划的联合支持下，巴尔的摩县马里兰州大学（UMBC）的泰勒约瑟夫森正在开发一种新的方法来编写计算化学中的代码。在测试新算法时，正确编码是很重要的。精益是一种编程语言，可以帮助检查数学证明是否正确。Josephson的实验室，UMBC的人工智能理论导向分子科学（ATOMS）实验室，将使用并教导其他人使用Lean来编写Lean中的推导和模拟软件，确保数学和代码正确。他们将开发用于模拟分子运动的LeanMD（精益分子动力学）软件，该软件旨在消除错误和数学错误。该项目将扩展到SciLib，这是一个跨科学和工程所有领域的社区来源的证明库。其他人可能会使用这些证明来探索科学文献并验证他们自己的证明，加速新理论的发现。社区学院的外展活动和为本科研究招收转学生将支持多元化的STEM（科学，技术，工程和数学）劳动力。与微软研究院的精益开发人员的跨学科合作预计将促进学生的学习和专业发展。计算机科学家使用交互式定理证明器来验证数学和软件，但这些很少用于科学计算。Lean是由微软研究院（MSR）开发的一种现代定理证明器和编程语言，旨在使数学家能够定义高级数学对象并证明有关它们的陈述。泰勒约瑟夫森的研究小组，人工智能理论导向分子科学（ATOMS）实验室，正在探索如何将经典力学和分子动力学（MD）的数学转化为精益代码（定义哈密顿和牛顿运动方程，以及Verlet算法等可计算表达式，并证明它们之间的关系），并使用这些来构建LeanMD，正式验证的MD软件。这是创建SciLib的第一步，SciLib是一个开源的科学和工程证明库，类似于Lean的社区来源的数学库mathlib。大型证明数据库可用于评估大型语言模型（LLM），以自动完成证明（由Lean编译器提供验证），将非正式科学转换为正式证明（或相反），以及生成，证明和解释新理论。为了向科学家和工程师教授精益，ATOMS实验室正在计划年度培训研讨会，通过成员对SciLib的持续贡献来衡量参与度，以及在精益中构建的互动在线游戏，将定理证明和精益语言引入到非该奖项反映了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.