Research
Foundation models, representation learning, formal methods, scientific discovery, and reinforcement learning.
Agentic AI & Formal Methods
Current work at Axiomatic AI / Head of AI Research
Building machine-checkable, reusable infrastructure for scientific reasoning through Lean4 libraries and AI-powered autoformalization, to bring to physics the same success formal methods recently had in mathematics.
AxProverBase: A Minimal Agent for Automated Theorem Proving
A minimal agent for automated theorem proving in Lean4, combining LLM reasoning with formal verification to prove real-world mathematical theorems.
SorryDB: A Real-World Benchmark for Theorem Provers
A dynamically-updating benchmark of theorem proving tasks sourced from real GitHub projects, measuring how well AI provers can complete real-world Lean theorems.
Foundation Models for Science
Flatiron Institute / Flatiron Research Fellow
Training multimodal foundation models that learn shared representations across scientific data types (images, spectra, time series, and metadata) to enable cross-domain transfer and accelerate discovery.
AION-1
Omnimodal foundation model for astronomical sciences, processing 15+ data types including images, spectra, time series, and metadata.
AstroCLIP
Cross-modal foundation model for galaxies using contrastive learning to align galactic images and spectroscopic data into a shared embedding space.
Spectral Tokenization
Universal self-supervised representation learning for astronomical spectra, enabling transfer across instruments and wavelength ranges.
Joint Embeddings go Temporal
Adapting Joint Embedding Predictive Architectures (JEPA) for scientific time series, learning temporal representations without contrastive pairs.
Exploration in Reinforcement Learning
Google DeepMind / Research Scientist Intern
Novelty-based Exploration
A representation-based approach to long-horizon exploration that achieves state-of-the-art performance in hard sparse-reward environments like Montezuma's Revenge, using learned representations to drive novelty-seeking behavior over extended time horizons.
Artificial Scientific Discovery
Max Planck Institute for the Science of Light / Doctoral Researcher
Developing machine learning methods for automated scientific reasoning, from unsupervised feature extraction to optimal experimental design and program synthesis.
Renormalized Mutual Information
An unsupervised method for extracting physically meaningful features from complex systems. The resulting paper was selected as the cover for Physical Review Letters Vol. 126, Issue 20.
Bayesian Experimental Design
Deep active learning approach for optimally designing experiments on quantum many-body systems, maximizing information gain per measurement.
Program Synthesis for Quantum Circuits
Using program synthesis techniques to automatically discover reusable quantum circuit components, decomposing complex unitaries into interpretable building blocks.
Reinforcement Learning with Learned Gadgets
An RL agent that automatically discovers reusable quantum circuit primitives (gadgets) and composes them to solve hard optimization problems on real quantum hardware.
PhD Thesis: Artificial Scientific Discovery
Machine learning methods for automated scientific reasoning, combining information-theoretic approaches, active learning, and program synthesis to accelerate discovery in quantum physics.
Statistical Physics, Biophysics and Quantum Information
Sapienza University / collaborations
Spin Glasses
Study of longitudinal fluctuations of the Sherrington-Kirkpatrick model, conducted under the supervision of Nobel laureate Giorgio Parisi at Sapienza University.
Gene Expression Patterns
Maximum entropy models for patterns of gene expression, applying statistical physics methods to understand biological systems.
Device-Independent Quantum Tests
Experimental semi-device-independent tests of quantum channels, bridging quantum information theory with laboratory experiments.