Robert Joseph

My work in AI4Science focuses on developing novel neural operator architectures for solving complex partial differential equations (PDEs). Key contributions include:

• Incremental Fourier Neural Operator (iFNO): Developed spatial and spectral learning methods for large-scale PDEs (TMLR 2024)
• CoDA-NO: Pretraining Codomain Attention Neural Operators for Multiphysics PDEs, achieving state-of-the-art results (NeurIPS 2024)
• Neural Operator library: Contributing to an open-source library for learning neural operators (under review)
• Extended work on physics-informed neural operators and spectral methods for parametric PDEs

Leading efforts to integrate large language models with formal theorem proving in Lean. Major projects include:

• LeanAgent: Lifelong Learning for Formal Theorem Proving - demonstrates curriculum learning over different mathematical domains (ICLR 2025)
• LeanProgress: First-of-its-kind reward model predicting proof progress in Lean (under review)
• LeanPDE: Formalizing PDEs in general Euclidean spaces, working toward millennium problems
• Collaborating on autoformalizers and unified interfaces for Lean tools

Developing memory-efficient training methods and optimization techniques for large-scale models:

• Tensor-GaLore: Memory-Efficient Training via Gradient Tensor Decomposition (NeurIPS Optimization Workshop 2024)
• Working on efficient training methods for foundation models in scientific domains
• Exploring connections between optimization theory and neural operator architectures
• Investigating theoretical foundations of deep learning and generalization bounds