Conference

From the start of AI, mathematical theorem proving has been an important challenge and technique. We sketch the topics of Automated and Interactive Theorem Proving and present the checking of naturally readable mathematical texts in the Naproche proof system. This involves translations between informal, semi-formal and formal mathematical languages and shows great potential for the use of new AI techniques.

What would effective and usable tools for searching text and graphics in research papers look like? In this talk we sketch a partial answer to this question, with reference to recent work in the Document and Pattern Recognition Lab at RIT. Two multimodal paper search prototypes, one for math (MathDeck) and one for chemistry (ReactionMiner search) will be used for illustration. A simple framework based on 'jars' of available information sources can organize and relate the actions performed by people and automated systems when retrieving, analyzing, and synthesizing sources. We will organize our answer sketch around this framework, and share open questions and research opportunities related to enhancing multi-modal search tools for expert and non-expert users. Note: ReactionMiner was developed in collaboration with NCSA and the Han lab at the University of Illinois, Urbana-Champaign. MathDeck demo: [https://people.rit.edu/ma5339/mathdeck_landing](https://people.rit.edu/ma5339/mathdeck_landing) ReactionMiner search demo: [https://reactionminer.platform.moleculemaker.org/home](https://reactionminer.platform.moleculemaker.org/home) Biography: Richard Zanibbi is a Professor of Computer Science at the Rochester Institute of Technology (RIT, USA) where he directs the Document and Pattern Recognition Lab (dprl@RIT). His research focuses upon the recognition and retrieval of graphical notations, particularly for mathematics and chemistry. He is also a member of the Molecule Maker Lab Institute (MMLI), one of the first NSF AI Centers. He received his PhD from Queen's University (Canada), and was an NSERC Postdoctoral Fellow at the Centre for Pattern Recognition and Machine Learning (CENPARMI) at Concordia University before joining RIT.

This short talk will outline some of LaTeXML's uses as infrastructure, as well as its enabling effect for search, AI, assistive technologies and the mobile web. We have been on a journey towards scholarly articles with web-native mathematics since the dawn of the internet. The physics Open Science movement has led the way along with LaTeX, its authoring framework of choice. NIST's LaTeXML is a conversion tool that in the last twenty years has increasingly bridged that gap.

The rise of AI, in particular recent LLM based tools, has had an immediate impact on the production of physics, in ways both good and bad. I discuss some of the impact seen on arXiv in particular, what the status quo and prospects are, and speculate on the longer term impact.

UniverseTBD is an interdisciplinary community of astronomers, AI researchers, engineers, artists and enthusiasts aligned on a bold mission to democratise Science for everyone. From releasing the first large language model in Astronomy, AstroLLaMA-1, to the AI-enabled literature discovery tool Pathfinder, and through our research with AstroPT and HypoGen, our team has pushed the boundaries of AI for Science for the past two years. In this talk, I discuss for the first time how UniverseTBD came to be, our vision, our values, and what drives us and has enabled us to scale our team projects in our commitment to share our learnings with the broader scientific community. I also briefly discuss our latest results with hypothesis generation (HypoGen), multimodal language models (AstroLlaVA-1) and agentic AI (AstroCoder). I conclude with a vision for the future where AI teams up with human researchers to "help us understand the Universe".

The newest large-language reasoning models are for the first time powerful enough to perform mathematical reasoning in theoretical physics at graduate level. In the mathematics community, data sets such as FrontierMath are being used to drive progress and evaluate models, but theoretical physics has so far received less attention. In this talk I will present our dataset TPBench (arxiv:2502.15815, tpbench.org), which was constructed to benchmark and improve AI models specifically for theoretical physics. We find extremely rapid progress of models over the last months, but also significant challenges at research level difficulty. I will also briefly outline strategies to improve these models for theoretical physics.

Recent advancements have positioned Large Language Models (LLMs) as transformative tools for scientific research, capable of addressing complex tasks that require reasoning, problem-solving, and decision-making. Their exceptional capabilities suggest their potential as scientific research assistants, but also highlight the need for holistic, rigorous, and domain-specific evaluation to assess effectiveness in real-world scientific applications. This talk describes a multifaceted methodology for Evaluating AI models as scientific Research Assistants (EAIRA) developed at Argonne National Laboratory. This methodology incorporates four primary classes of evaluations. 1) Multiple Choice Questions to assess factual recall; 2) Open Response to evaluate advanced reasoning and problem-solving skills; 3) Lab-Style Experiments involving detailed analysis of capabilities as research assistants in controlled environments; and 4) Field-Style Experiments to capture researcher-LLM interactions at scale in a wide range of scientific domains and applications. These complementary methods enable a comprehensive analysis of LLM strengths and weaknesses with respect to their scientific knowledge, reasoning abilities, and adaptability. Recognizing the rapid pace of LLM advancements, we designed the methodology to evolve and adapt so as to ensure its continued relevance and applicability. This talk describes the current methodology's state. Although developed within a subset of scientific domains, the methodology is designed to be generalizable to a wide range of scientific domains.

The standard way to do this is to use the chain rule to backpropagate gradients through layers of neurons. I shall briefly review a few of the engineering successes of backpropagation and then describe a very different way of getting the gradients that, for a while, seemed a lot more plausible as a model of how the brain gets gradients. Consider a system composed of binary neurons that can be active or inactive with weighted pairwise couplings between pairs of neurons, including long range couplings. If the neurons represent pixels in a binary image, we can store a set of binary training images by adjusting the coupling weights so that the images are local minima of a Hopfield energy function which is minus the sum over all pairs of active neurons of their coupling weights. But this energy function can only capture pairwise correlations. It cannot represent the kinds of complicated higher-order correlations that occur in images. Now suppose that in addition to the "visible" neurons that represent the pixel intensities, we also have a large set of hidden neurons that have weighted couplings with each other and with the visible neurons. Suppose also that all of the neurons are asynchronous and stochastic: They adopt the active state with a log odds that is equal to the difference in the energy function when the neuron is inactive versus active. Given a set of training images, is there a simple way to set the weights on all of the couplings so that the training images are local minima of the free energy function obtained by integrating out the states of the hidden neurons? The Boltzmann machine learning algorithm solved this problem in an elegant way. It was proof of principle that learning in neural networks with hidden neurons was possible using only locally available information, contrary to what was generally believed at the time.