Dhruv Gupta

Ather Energy · Robotic welding reliability (K383)

Causal root-cause analysis under drift. Deployed, 2025.

Problem. Intermittent welding anomalies on a production line produced high MTTR because the linkage between alarm, defect, and action was weak and ad-hoc.

Approach. A causal world-model for the welding cell aligned to the 4Ms: Man (operator context), Machine (telemetry/configs), Method (process recipes), Material (batch provenance). Implemented as an OWL ontology, internally named K383.

Uncertainty diagnostic. A geometric belief-function analysis (Cuzzolin framework) classifies each failure path by resolvability: 60% are diagnosable from error codes alone, 12% require targeted additional evidence, and 28% are structurally unresolvable without live data integration. The diagnostic tells the operator not just what happened, but what else needs to be known.

Output. Ranked suspects, fault-path narrative, and minimum next checks that collapse uncertainty fastest. Drift is treated as first-class; verification gates keep explanations tethered to evidence rather than LLM fluency.

Temple · Sensor validation & causal calibration

Speckle plethysmography feasibility; phantom-first. Engagement with Continue Research (Eternal).

Three workstreams. (1) A stable SPG reference system with primary flow/perfusion metrics; (2) a reproducible multi-layer phantom with controlled confounders; (3) a calibration mapping with QC gates.

Thesis. Calibration is where sensing programmes quietly fail. Making confounders and interventions first-class (rather than nuisance) makes calibration transferable rather than artisanal.

Terrapulse · Research-grade soil CO₂ flux

Open-source instrument · IISc B.S. Research thesis (A+, Rank 1) · code: github.com/ARC-Net / CO2mmunity

Low-cost NDIR CO₂ cell (K33-ELG) on embedded compute, designed to capture sub-minute flux pulses at research-grade precision. Three-layer Bayesian calibration chain: FTIR step-test → lab pulse simulation → multi-day field mass-closure via alkali trap. Field-deployed in Lahaul–Spiti valley over 2024–25.

Open methods, datasets, and analysis pipeline released at ARC-Net / CO2mmunity. Final 95% posteriors: gain = 0.993 ± 0.005; offset = 16 ± 10 ppm; drift = 0.002 ± 0.020 ppm h⁻¹.

Current iteration is a miniaturised, solar-powered revision of the same sensing chain, designed for unattended multi-month deployments in remote terrain.

iGEM · Halocleen · Pseudomonas putida for halocarbon biodegradation

IISc iGEM 2022 project, Paris Jamboree Gold Medal, Climate-track finalist. Two bioreactor designs with patents pending.

Problem. CFC-11 and CFC-12 persist in the stratosphere for decades with no scalable biological degradation path. The project asked whether an engineered soil bacterium could be coaxed into degrading halocarbons at rates relevant to atmospheric removal.

Approach. Engineered Pseudomonas putida as the chassis, carrying synthetic circuits assembled from plasmids drawn from the methanotroph halocarbon-oxidation literature. Two bioreactor designs (continuous-flow trickle-bed and gas-lift variants) were optimised for the low-solubility substrate regime; patents filed, pending.

Team Lead, 2022. ~10-person team (bio, hardware, modelling, wet-lab validation). Covered in the IISc press release: IISc students win again at iGEM.

Formal Learning Theory Kernel Synthetic Discovery

21,728 lines of Lean4, machine-checked with no gaps.

A self-contained Lean4 kernel of formal learning theory, currently under arXiv review and being upstreamed to Lean4 cslib and mathlib. Four results it carries that the field had been citing rather than proving:

• Borel–analytic separation theorem: weakens the Borel-measurability hypothesis of Krapp–Wirth 2024 to analytic / null-measurable, with a strict separation witness (a concept class whose bad event is null-measurable but not Borel). Closure under patching, interpolation, and amalgamation. All main results formalised in Lean4.
• Constructive MWU-based compression proof.
• PAC-Bayes bound: first Lean4 formalization of record.
• Choquet capacitability: previously absent from Mathlib4.

Formalization is the claim, checked by the Lean4 compiler.

The fundamental theorem, stated and proved in the kernel as a single term (FLT_Proofs/Theorem/PAC.lean):

/-- Fundamental theorem of statistical learning (5-way equivalence, BP₅). -/
theorem fundamental_theorem (X : Type u) [MeasurableSpace X]
    [MeasurableSingletonClass X]
    (C : ConceptClass X Bool) [MeasurableConceptClass X C] :
    (PACLearnable X C ↔ VCDim X C < ⊤) ∧
    ((VCDim X C < ⊤) ↔
      ∃ (k : ℕ) (cs : CompressionSchemeWithInfo0 X Bool C), cs.size = k) ∧
    ((VCDim X C < ⊤) ↔
      ∀ ε > 0, ∃ m₀, ∀ (D : MeasureTheory.Measure X),
        MeasureTheory.IsProbabilityMeasure D →
        ∀ m ≥ m₀, RademacherComplexity X C D m < ε) ∧
    (PACLearnable X C →
      ∃ (L : BatchLearner X Bool) (mf : ℝ → ℝ → ℕ),
        -- PAC guarantee, sample-complexity upper bound, and matching lower bound
        ...) ∧
    ((VCDim X C < ⊤) ↔
      ∃ (d : ℕ), ∀ (m : ℕ), d ≤ m →
        GrowthFunction X C m ≤
          ∑ i ∈ Finset.range (d + 1), Nat.choose m i) :=
  -- BP₅: 5-way conjunction assembles from component theorems
  ⟨vc_characterization X C,
   fundamental_vc_compression X C,
   (vc_characterization X C).symm.trans (fundamental_rademacher X C),
   pac_sample_complexity_sandwich X C,
   ⟨vcdim_finite_imp_growth_bounded X C,
    growth_bounded_imp_vcdim_finite X C⟩⟩

PAC-learnability ↔ finite VC dim ↔ bounded compression scheme ↔ vanishing Rademacher complexity ↔ polynomial growth function. Sauer–Shelah, symmetrisation, and concentration inequalities are the three loadbearing lemmas.

Transformer Learning Theory

Measurability-theoretic foundations for attention architectures.

Lean4 results: attention-routing measurability; softmax–argmax equivalence under appropriate limits; a universality statement (every measurable router is attention); and a NullMeasurable necessity result.

Spekkens 2007 · Hidden Capacity Synthetic Discovery

31 machine-checked theorems extending Spekkens's epistemic toy-theory of quantum states.

A Lean4 formalization of Spekkens's 2007 epistemic toy-theory of quantum states, together with HC(κ): the first continuous measure of interpolation failure in epistemic theories of mechanics. HC = 0 iff the theory's admissible configurations are rectangular (decomposable).

Boundary results. The four entangled states admit HC = 2.00 bits; the three separable states admit HC = 0. Only private-evidence conditioning collapses nonzero HC; shared evidence resolves 0% of it. A cross-domain oscillation theorem the Lean4 kernel checks by construction. Three predictions beyond Spekkens follow as corollaries and are verified in the kernel.

LLM harness · First Proof Challenge Synthetic Discovery

Operational pipeline; Harvard benchmark, commodity compute.

An LLM-driven proof search harness that reached 4 of 10 on Harvard's First Proof Challenge benchmark using $32 of commodity API compute on a single MacBook. The number is not the point. The shape of the failures is. Where the harness succeeds is where formalization gates exist; where it fails is where they are absent.

Hyper-Resonant Dendritic Oscillations (HDO)

Single-neuron timing primitive · preprint on request.

Claim. A single stellate cell carries two stable intrinsic oscillatory regimes (a θ-like slow regime and a high-frequency HDO regime) with stochastic switching driven by channel noise.

Mechanism. Stochastic Ca_V gating (Gillespie) plus a calcium-activated current plus BCM-like intrinsic plasticity regulates the transition probability between regimes. Bifurcation reasoning points to a subcritical Hopf / SNIC candidate; robustness confirmed under parameter sweeps.

Consequence. A timing primitive that is neither a fixed oscillator nor a pure integrator. The metaplasticity-gated switching between regimes is itself the computation.

Origin: a final-project artifact of Prof. SP Arun's Theoretical and Computational Neuroscience course at IISc.

Dawn Arbor Synthetic Discovery

Open Python platform for machine-checked neurobiophysics.

Converts ModelDB .hoc models into a type-inheritance DAG so neurobiophysics models can be composed, type-checked, and verified like programs rather than passed around as opaque simulation scripts.

NIAS collaboration · Neurochaos learning for calibration

With the National Institute of Advanced Studies, IISc campus.

Using neurochaos-learning primitives (chaotic-attractor features) as a calibration substrate for biosensors where conventional linear calibration is brittle to nonstationary confounders.

Virog MedTech

Founder · IISc-funded student medtech club. ~5 people. Institutional grant pool of ₹10 L.

What was tested. Whether a five-person student team, with an institutional grant pool but no commercial pressure, could deliver three independent medtech devices from first principles on pre-clinical timelines.

Devices. OECT wound bandage; UV-SSI patch for HAI prevention; physics-driven CVD predictor.

Highlight. The CVD predictor won 1st prize at IIC 2025 (IISc Innovation Challenge).

The club is now inactive; the three devices and the mentorship chains came out of it, and the structure of the experiment is what we kept.

Origin (most naive version of the work): Virog · MIT Solve submission.

IISc Robotics Club

Founder & President, 2023–. ~30 members. ₹5 L club budget.

What was tested. Whether parallel multi-domain student robotics projects can run concurrently under a shared budget without losing depth. Active lines under the club: lunar rover, rehab exoskeleton, drone, 6-DoF manipulator, legged-locomotion prototypes.

Team Vicharaka · University Rover Challenge. Out of the club, the Mars-rover team Vicharaka ("one who thinks") qualified for the University Rover Challenge (URC) at the Mars Desert Research Station, Utah. I led the Life-Detection subsystem: biosignature-sampling and onboard assay for the Martian-soil analogue, pipelined to the rover's onboard compute. Coverage by IISc's Connect IISc: “Red Rover”.

Prof. Pradipta Biswas's lab team · ISRO IRoC-U 2024 finalist. A separate rover team, based in Prof. Biswas's group at the Nahar Centre for Robotics · Robert Bosch Centre for Cyber-Physical Systems, IISc. The team was a finalist in the ISRO Robotics Challenge (IRoC-U 2024) run by URSC, securing a ₹25 L grant. I was the undergraduate team member contributing the biology half of the lunar-surface assay stack.

IEEE Computer Society / CIS Student Chapter, IISc

Chair.

What was tested. Whether the chapter could broker a concrete undergraduate-to-graduate research-exposure loop at low institutional friction, alongside running an open curriculum under the IEEE brand.

“Hire an Undergrad” programme. The main operational artifact of my term. MTech and PhD students could post short project briefs on the chapter board and, with their supervising professor's approval, “hire” an undergraduate as a research assistant for a scoped piece of the project. Undergrads got first-contact research exposure on active problems (not make-work); grad students got a documented assistant pool without rewriting bureaucracy. The matching itself was lightweight: a one-page brief, a faculty sign-off line, a handshake.

Other outputs. Open-source 6G lecture series.

EntIISc · IISc Entrepreneurship Cell

Vice-President. 44 deep-tech proposals screened. Brokered ₹15 L seed pool (FSID).

What was tested. Whether a campus cell, working inside the IISc incubation structure, could route deep-tech student proposals to institutional funding at scale. Output: 44 screened proposals, Boeing sponsorship, and a working pathway to the FSID institutional grant pool.

External validation. EntIISc won first place at E-merge, the inter-institution entrepreneurship-cell competition run by IIT Hyderabad's E-Cell. I pitched on behalf of the cell and served on the event's panel alongside other cell leads and invited speakers.

Cell overview: About EntIISc.

JRD Tata Innovation Support Center · IISc

Founder-Director · PI, 2024. 40+ students. 8 project tracks.

What was tested. Can the same operator catch the center-of-mass unknown in eight unrelated domains within a single summer? All 8 tracks reached working prototype; the portfolio itself is the contribution.

• Voice-first teleoperation of a robotic arm from smartphone (safety + latency trade-off).
• Digital-twin-driven bionic arm with calibration drift as the primary failure mode.
• Low-cost servo + encoder stack (FSM decoding of noisy inputs).
• BCI/EEG → text with generative-AI coherence gates.
• Physics-to-math knowledge engine (compiler as verification gate).
• General-purpose multi-I/O power converter.
• Fuel-quality automation with Pass/Fail/Inconclusive as a first-class output.
• Forensic triage with Bayesian uncertainty and mandatory justification chains.

Also prototyped SoTA instrumentation for the Karnataka Forensics Lab.

ARCNet Research · R&D foundry at ARTPARK @ IISc

Founder & PI, 2024–Jun 2025. 18-member institutionally- funded lab at ARTPARK. Transitioned to permanent team.

What was tested. Whether an institutionally-funded deep-tech foundry can deliver unrelated research engagements end-to-end, each on its own scientific terms. Four independent engagements below.

Satsure · KALIDEO

Remote-sensing QC · classical + deep-learning

Dockerized pipeline testing classical and deep-learning approaches for cloud segmentation on satellite hardware. Optimized for on-device inference under bandwidth and power constraints.

Satellite-Cloud-Segmentation on GitHub

School of Meaningful Experiences

Multimodal evaluation · full-stack deployment · 5 microservices

Automated grading of interviews, presentations, and speech, with LMS integration. Audio capture, video capture, grading pipeline, LLM feedback, and report generation run as independent microservices so each can be scaled, swapped, or audited without touching the others.

Audio · Video · Flask · Report · LLM

Open Science Stack · Science Compiler

Autonomous science · robotic-lab orchestration · ontology-driven protocol synthesis

OSS is a volunteer-driven, non-profit digital public infrastructure for AI-powered, self-driving labs, backed by ARTPARK (IISc) and the Red Black Trust. Its architectural thesis: treat experiments as cloud-dispatchable programs (“write once, run anywhere”) across a network of programmable physical labs. The Science Compiler is my contribution: a three-layer behaviour-tree architecture for robotic laboratories that compiles high-level scientific intent into robot-agnostic execution via ontology-driven protocol synthesis. It slots into OSS's inner experiment-optimization loop and feeds the ROS2-based Robotic Application Stack (RAS).

opensciencestack.org · About & founding team · RAS architecture

LeanAide · Prof. Siddhartha Gadgil (IISc)

Lean4 assistant for natural-language math

ARCNet contributed to LeanAide, a Lean4 assistant for natural-language mathematics, at Prof. Siddhartha Gadgil's lab at IISc. It tackles autoformalization (natural-language math into machine-checkable Lean4), one of the least-developed bridges between LLMs and formal verification.

siddhartha-gadgil/LeanAide

Zetesis Labs · ARTPARK Industry 5.0 Board

Principal Investigator · Innovator-in-Residence · Board Member, 2025–Present.

What is being tested. Whether a sustained research programme can close the loop from formal epistemology to industrial deployment across multiple partners. Active: manufacturing R&D automation pilots with BEL, Bosch, and Toyota.

Creative Engineering Design · Classroom Chair

PD 203, Prof. Amaresh Chakrabarti, CPDM / IISc, 2024. Group project.

A classroom chair with a steering tripod (so it can be lifted and wheeled for easy cleaning) and a floor-pedal coupled to a dynamo that trickle-charges a phone once the rider is pedaling stably. The problem we chose to solve was classroom sleepiness, a very real pandemic.

Neuromorphic Analog VLSI Design · Binary Encoder Bit Correction

E0 204, Prof. Chetan Singh Thakur, DESE / NeuRonICS Lab, IISc.

Final project: bit-correction in a binary encoder via a neuromorphic construct. Alongside, during the course: a neuromorphic mod of SPICE, built as a local substitute because Cadence access was gated to department MTech and PhD students only.

Information–energy efficiency operator

MB 208 Theoretical and Computational Neuroscience, Prof. SP Arun, IISc.

A complex-valued operator that expresses the energy–information tradeoff in neural computation, studied in Brian2 simulations of a two-cell post-inhibitory rebound oscillator.

-- Complex efficiency phasor
Λ = |Λ| · e^(jθ)  ∈  ℂ

-- Phase-lag taxonomy
 θ-band              Regime              Functional role
 ────────────────   ──────────────────  ─────────────────────────────
 0°  ≤ θ < 30°      reactive            immediate transduction
 30° ≤ θ < 45°      memory-forming      partial integration
 θ ≥ 45°            memory onset        past input dominates
 60° ≤ θ < 75°      planner/anticipatory predictive buffering
 θ ≥ 75°            generative planner  information allocates energy

Partial validation. Baseline and temperature-drift Λ posteriors recovered in Experiments 1–2; the MPMOSS falsification sweep (Experiment 3) was not completed. Mixed results; the taxonomy is a design proposal, not a validated claim.