How I got here, in order

Research Intern

emergence AI

Formal verification applied to a physics engine, so that reinforcement learning agents cannot farm rewards out of the simulator's own numerical mistakes.

• Built a 2D collision detection engine in Lean 4 with correctness proofs carried alongside the implementation, structurally eliminating the tunnelling exploit where a fast body passes through a wall between two timesteps.
• Replaced IEEE-754 floating point with exact rational arithmetic, making the state machine fully deterministic: identical inputs produce bit-identical output on any machine, so a training run is reproducible and a replay is trustworthy.
• Tunnelling matters because an RL agent will find it. Any gap between the physics you intended and the physics you shipped becomes a reward the agent learns to collect instead of the task.

• Lean 4
• Formal Verification
• Theorem Proving
• Rational Arithmetic
• Physics Simulation

Robotics Engineering Intern

Saturn Labs

Bengaluru

Synthetic data and simulation for egocentric vision: generating the training set in NVIDIA Isaac Sim, then making the model that consumed it fast enough to run live.

• Built synthetic data pipelines and physics-based simulation environments in NVIDIA Isaac Sim, Isaac Lab and Gazebo.
• Took the real-time 3D hand pose pipeline from 50 FPS to 85 to 90 FPS on the same hardware, roughly a 75 percent increase, by reworking the data path and the network architecture together rather than tuning either alone.
• Latency is the whole product in egocentric vision. A hand tracker running at 50 FPS on a headset is one the wearer can feel lagging behind their own hand.

• Isaac Sim
• Isaac Lab
• Gazebo
• Synthetic Data
• PyTorch
• Real-time Inference