Researching large language models for formalized mathematics and automated reasoning.
I work on robust methods for autoformalization and automated theorem proving using large language models. My current interest is in making LLM-based reasoning systems more controllable, predictable, and verifiable by combining them with formal methods. My background spans machine learning, compiler optimization, static analysis, multimodal navigation, and causal reasoning.
Introduced a scalable vision-language distance learning framework for goal-conditioned navigation that decouples perception from control. Trained on roughly 3,000 hours of video data and plugged into independently trained RL policies as a drop-in replacement for privileged simulator distances, outperforming prior distance models (ViNT, VIP) and yielding strong sim-to-real transfer on real-robot deployment.
Developed a GNN-based context-sensitive static profiler for Graal Native Image, achieving a 10.13% runtime speedup on industry-standard benchmarks and a 3.7% throughput gain on real-world microservices.
Designed CESAR, a new BERT-based causal strength metric that outperformed prior metrics (ROCK, CEQ) by more than 50% on the newly introduced δ-CAUSAL benchmark for defeasible causal reasoning.
Created a notebook-aware static analysis framework that models notebook execution semantics and catches data leakage and related bugs while preserving interactive performance.
Explored propagation dynamics in evolving knowledge graphs, showing that structural updates primarily affect local entity embeddings while preserving overall stability.
Additional work spanning interpretable ML for climate communication, vision-only autonomous navigation, and a handwritten equation solver built in C++.
EPFL, Lausanne
Developing robust methods for autoformalization and automated theorem proving with large language models, with emphasis on controllability, predictability, and reasoning reliability.
Robotics Systems Lab, ETH Zurich
Built VLD, a scalable vision-language distance function that predicts how many steps remain to reach an image- or text-specified goal. Designed a two-stage navigation framework that decouples perception (the distance predictor, learned from ~3,000 hours of internet-scale video) from control (an RL policy trained in simulation on privileged geometric distances), so the real-robot policy can swap in VLD predictions at deployment without any retraining.
Oracle Labs, Zurich
Integrated a GNN-based profiling model into Graal, automated monitoring and retraining, and contributed to research that improved performance over both production and benchmark baselines.
Palantir, London
Enhanced the SAMv2 architecture for visual search and implemented data-source-side aggregation pushdown for Spark workloads.
Microsoft, Inria Center at École Polytechnique, EPFL, Anemone
Worked on notebook static analysis, Azure Service Fabric infrastructure, spatiotemporal action detection, teaching assistance in reinforcement learning, and co-founded a creative-industry networking startup.
Programming: Python, Java, C++, C, JavaScript, React Native, React, C#, Prolog, R
ML and Systems: PyTorch, Hugging Face, Transformers, machine learning, deep learning, NLP, computer vision, reinforcement learning, graph neural networks, compiler optimization, static analysis
Languages: English (C2), French (B2), Serbian (C2)