AI Dynamics

Global AI News Aggregator

About

@animaanandkumar

  • Lean Community Infrastructure Enables LLM Advancement in Proof

    Honestly, a huge part of this is thanks to the incredible Lean community @leanprover ! Mathlib, proof tooling, and years of infrastructure work made this possible —Lean is far more usable today because of that collective effort. And yes, LLMs have gotten much better at Lean lately 🙂 definitely helps accelerate learning and prototyping. Evan Chipman (@evanchipman) This is the 3rd time this week I thought “someone ought to make x” then open this app and see a team announce x. The speed of this era is disorienting. — https://nitter.net/evanchipman/status/2028157017597374837#m

    → View original post on X — @animaanandkumar, 2026-03-01 22:57 UTC

  • TorchLean: First Fully Verified Neural Network Framework in Lean
    TorchLean: First Fully Verified Neural Network Framework in Lean

    Super excited to release TorchLean!! I’m happy to answer questions and would love to discuss verified NNs + theorem proving especially what it’ll take for the field to become widely usable in real ML systems. Blog post + codebase release soon! Prof. Anima Anandkumar (@AnimaAnandkumar) We’re excited to release TorchLean which is the first fully verified neural network framework in Lean. The Lean community has largely focused on pure mathematics. TorchLean expands this frontier toward verified neural network software and scientific computing. With the recent release of CSlib, we see this as another step toward a fully verified ML stack. We support features: 1. Executable IEEE-754 floating-point semantics (and extensible alternative FP models) verified tensor abstractions with precise shape/indexing semantics 2. Formally verified autograd system for differentiation of NN programs Proof-checked certification / verification algorithms like CROWN (robustness, bounds, etc.) 3. PyTorch-inspired modeling API with eager-style development + export/lowering to a shared IR for execution and verification Project page: leandojo.org/torchlean.html Paper: [2602.22631] TorchLean: Formalizing Neural Networks in Lean Work done @Robertljg, Jennifer Cruden, Xiangru Zhong, @huan_zhang12 and @AnimaAnandkumar. #MachineLearning #ScientificComputing #Lean — https://nitter.net/AnimaAnandkumar/status/2027907453908857298#m

    → View original post on X — @animaanandkumar, 2026-03-01 22:38 UTC

  • Formal Verification for Neural Networks in Lean

    Verification is a cornerstone for reasoning. Recent progress in mathematical reasoning and theorem proving has relied on LLMs + formal verification in Lean. But so far, Lean has focused on pure math, and lacks support for verification involving neural nets themselves. Applications include: 1. Certified robustness in neural networks, crucial in safety critical applications such as neural control. 2. Physics informed neural networks, which have been used to prove singularity problems related to the Millennium prize problem in fluid dynamics. 3. Theory related to neural networks such as approximation bounds, effect of quantization etc.

    → View original post on X — @animaanandkumar, 2026-03-01 01:04 UTC

  • TorchLean: First Fully Verified Neural Network Framework in Lean
    TorchLean: First Fully Verified Neural Network Framework in Lean

    We’re excited to release TorchLean which is the first fully verified neural network framework in Lean. The Lean community has largely focused on pure mathematics. TorchLean expands this frontier toward verified neural network software and scientific computing. With the recent release of CSlib, we see this as another step toward a fully verified ML stack. We support features: 1. Executable IEEE-754 floating-point semantics (and extensible alternative FP models) verified tensor abstractions with precise shape/indexing semantics 2. Formally verified autograd system for differentiation of NN programs Proof-checked certification / verification algorithms like CROWN (robustness, bounds, etc.) 3. PyTorch-inspired modeling API with eager-style development + export/lowering to a shared IR for execution and verification Project page: leandojo.org/torchlean.html Paper: [2602.22631] TorchLean: Formalizing Neural Networks in Lean Work done @Robertljg, Jennifer Cruden, Xiangru Zhong, @huan_zhang12 and @AnimaAnandkumar. #MachineLearning #ScientificComputing #Lean

    → View original post on X — @animaanandkumar, 2026-03-01 00:43 UTC

  • Neural Operators Enable Million Simulations in Single Run Time

    RT @DanTurnerEvans: What if you could run a million simulations in the time it takes to run one? Neural operators are making this a realit…

    → View original post on X — @animaanandkumar, 2026-02-23 19:09 UTC

  • Neural Operators: Running Million Simulations in Seconds
    Neural Operators: Running Million Simulations in Seconds

    What if you could run a million simulations in the time it takes to run one? Neural operators are making this a reality. These neural networks learn to approximate the physics behind conventional simulations and then produce new solutions almost instantly. The result? Better-performing chips, smarter fusion reactors, faster drug discovery. A new neural operator is trained for each design problem. The design process unfolds as follows: 1. The problem is defined. For example, optimizing the layout of a computer chip to minimize hot spots that arise during operation and can lead to device failure. 2. The parameter space is defined. In the above example, this could be the range of possible layouts and connections between chip components. 3. Hundreds or thousands of conventional simulations are run to sample the parameter space. These simulations can be very computationally intensive, requiring a supercomputer in some cases. 4. The neural operator is trained on those simulations. Crucially, while the training simulations use discrete grids, neural operators learn continuous solutions. This means they can be trained on lower-resolution simulations and still produce accurate results at higher resolutions, saving even more compute. 5. The trained network evaluates candidate designs almost instantly, enabling rapid optimization across the parameter space. 6. The solution is verified with a conventional simulation. In practice, these checks are run periodically throughout the process to keep the neural operator honest. By replacing the bulk of expensive simulations with near-instant neural operator evaluations, engineers can explore vast design spaces that were previously out of reach. Yet another example of how neural networks beyond LLMs are quietly transforming science and engineering.

    → View original post on X — @animaanandkumar, 2026-02-23 19:00 UTC

  • AAAS 2026 Highlights: Science, Policy, and Research Innovation
    AAAS 2026 Highlights: Science, Policy, and Research Innovation

    ✨ New Article: #AAASmtg Highlights! ✨ @aaas is where science and policy meet, and this year’s Science @ Scale theme brought big ideas from across the research landscape. From climate and public health to biomedical innovation, it was inspiring to step outside our usual orbit—and even convert a few particle physicists into organ‑on‑chip fans. This year, we saw real momentum for non‑animal, human‑relevant science. SAO’s Gabby Vidaurre, PhD delivered a standout Postdoc Talk on our Research Modernization NOW #SciPol roadmap, and AI‑driven innovations took center stage—from lung‑ultrasound interpretation to exposome analytics. The SNAP Coalition made AAAS history with the first‑ever graduate student–led plenary, and science‑integrity icon @MicrobiomDigest reminded us why integrity is essential to all of what we do. ⬇️ Read the full recap, also featuring @AnimaAnandkumar of @CaltechEAS, @ThomasHartung19 of @jhucaat, and researchers from @ASU, @asuhealth, and @tue_mech: linkedin.com/pulse/sao-actio…

    → View original post on X — @animaanandkumar, 2026-02-20 15:20 UTC

  • CO₂ Storage Subsurface Modeling for Carbon Capture Scaling

    RT @jiacheny7: Accurate modeling of CO₂ storage in the subsurface is a critical challenge for scaling Carbon Capture and Storage (CCS). 🌎 B…

    → View original post on X — @animaanandkumar, 2026-02-19 20:08 UTC

  • Fun-DDPS: Decoupled Diffusion for CO₂ Storage Inverse Modeling

    Accurate modeling of CO₂ storage in the subsurface is a critical challenge for scaling Carbon Capture and Storage (CCS). 🌎 But here’s the catch: the inverse problem (recovering geological properties from sparse field observations) is severely ill-posed. 🤒 Traditional approaches either struggle with the scarcity of measured data or are too computationally expensive. 💸 In our new work, we introduce Fun-DDPS (Function-space Decoupled Diffusion Posterior Sampling), a generative framework that decouples the problem into two parts: a function-space diffusion model that learns a prior over geological parameters, and a differentiable Local Neural Operator surrogate for physics modeling and conditioning. ✨ Why does the decoupling matter? The diffusion prior handles the heavy lifting of recovering missing geological information, while the neural operator surrogate makes data assimilation fast and physically grounded — no expensive full-physics simulations in the loop. Key results on synthetic CCS datasets: ⏩ 11x improvement in forward modeling with only 25% observations ✅ Robust inverse modeling for data assimilation under sparse, noisy conditions 🔥 First rigorous validation of diffusion-based inverse solvers against asymptotically exact Rejection Sampling (RS) posteriors This points toward a scalable, practical path for uncertainty-aware subsurface characterization — something the CCS community needs as projects move from pilots to full-scale deployment. 📷 arxiv.org/abs/2602.12274 Huge kudos to my amazing collaborators — this work wouldn’t have been possible without them: @IsaacJu13 @AnimaAnandkumar Sally M Benson @ggg_www_ #CarbonCapture #CO2Sequestration #MachineLearning #DiffusionModels #NeuralOperators #AI4Science #CCS #Sustainability

    → View original post on X — @animaanandkumar, 2026-02-19 20:06 UTC

  • Anima Anand Kumar Cancels India AI Summit Trip Due to Commitments

    Unfortunately I have had to cancel my trip for India AI summit due to other commitments. I hope the Indian leadership continues to grow the AI ecosystem and invest in education and research. Data centers and GPU access needs to be democratized broadly. #IndiaAISummit2026

    → View original post on X — @animaanandkumar, 2026-02-17 05:26 UTC