LM Academic profile
EPFL EDIC

Lazar
Milikic

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.

Open CV LinkedIn GitHub
Venturi Space Award 2026 EPFL Excellence Fellowship ICML 2026 AI for Math CGO 2025 ACL 2024 ICSE 2022
PhD Computer Science at EPFL since November 2025
5.86/6 EPFL MSc GPA with Excellence Fellowship
4.16/4 École Polytechnique BSc GPA, summa cum laude
5+ major research projects across NLP, compilers, robotics, and systems

Selected Projects

NeurIPS 2026 VERICODEGEN Workshop · Best Paper Award

Learning Lean Feedback for Efficient Proof-Candidate Evaluation on GPUs

Developed neural evaluators trained on 4.84M labelled Lean programs to predict proof validity and compiler feedback on GPUs. A two-stage evaluator achieved 87.8% accuracy on 68,932 proof candidates and processed 3.5 candidates per second on a single H100 GPU. Hybrid rewards combining model predictions with Lean checks shortened GRPO training steps by approximately 31%, with comparable miniF2F pass@1 to Lean-only rewards (62.2% vs. 62.4%).

Paper
Master's Thesis · Venturi Space Award 2026

VLD: Vision-Language Distance for Goal-Conditioned Navigation

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.

Project page
ICML 2026 AI for Math Workshop

LeanFlow: Workflow-Driven Lean Autoformalization

Developed LeanFlow, an LLM agent that translates mathematical papers into buildable Lean projects through a verifier-driven workflow. LeanFlow placed second in the TCS Proving in Lean competition, solving 31 of 34 problems for 650/1000 points.

Paper LeanFlow Leaderboard
Lean Tooling

LeanProbe

Developed LeanProbe as part of LeanFlow: a fast Lean 4 proof-feedback tool for coding agents, available as an MCP server, CLI, and Python API. It keeps a Lean REPL warm and reuses elaborated environments for fast repeated checks.

LeanProbe
CGO 2025

GraalNN: Context-Sensitive Static Profiling with Graph Neural Networks

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.

Paper
ACL 2024

Exploring Defeasibility in Causal Reasoning

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.

Paper
ICSE 2022

A Static Analysis Framework for Data Science Notebooks

Created a notebook-aware static analysis framework that models notebook execution semantics and catches data leakage and related bugs while preserving interactive performance.

Paper
Projects

Additional Project Links

Additional work spanning interpretable ML for climate communication, vision-only autonomous navigation, and a handwritten equation solver built in C++.

Climate project Vision project Equation solver

Experience

Nov 2025 - Present

PhD Student / Doctoral Assistant

EPFL, Lausanne

Developing robust methods for autoformalization and automated theorem proving with large language models, with emphasis on controllability, predictability, and reasoning reliability.

Focus areas: LLM reasoning, formal verification, theorem proving Positioned at the Laboratory for Automated Reasoning and Analysis (LARA lab)
Mar 2024 - Nov 2025

Student Researcher

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.

Improved distance-model ordinal consistency by more than 20% over ViNT and VIP baselines At deployment, retained ~82% of the privileged-distance simulator success rate after replacing the simulator signal with VLD Strong sim-to-real transfer: 93.3% real-robot navigation success vs. 60% for the strongest image-based baseline (FGPrompt-EF)
Master's thesis graded 6/6; received the Venturi Space Award at EPFL (2026) for excellence in robotics Winner in the Master's thesis category of the Serbian Academic Society in Switzerland's Best Student Work 2026 competition
Venturi Space Award EPFL ceremony post Best Student Work award
EPFL award ceremony, with Lazar Milikic's name and master's thesis title displayed on the stage screen.
Venturi Space Award ceremony at EPFL, 3 October 2026.
Aug 2023 - Feb 2024, Oct 2024 - Feb 2025

Student Researcher

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.

4% production runtime improvement over the prior XGBoost-based model 10.13% runtime speedup on industry-standard benchmarks CGO 2025 paper and patent on the static profiler
Jul 2024 - Sep 2024

Machine Learning Researcher and Software Engineer

Palantir, London

Enhanced the SAMv2 architecture for visual search and implemented data-source-side aggregation pushdown for Spark workloads.

74.7% template object search accuracy on Objects365 Up to 41% lower query response time through aggregation pushdown
2021 - 2024

Earlier Research and Engineering Roles

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.

ICSE 2022 publication and patent for notebook static analysis More than 45% faster emergency response workflow for Azure Service Fabric hosts More than 1,000 users reached through the Anemone platform

CV and Skills

Current CV Materials

Academic CV Up-to-date academic CV. EPFL Profile Institutional page with doctoral affiliation and research summary.

Technical Areas

Programming: Python, Lean, Rocq, 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)