I'm a data scientist and ML researcher, currently doing a research M.Sc. at the Hebrew University of Jerusalem. My bachelor's was in physics, at Bar-Ilan, through its gifted-in-math track.
For a few years before grad school my job was building models that people actually acted on — first leading an operations-research and data-science team in Unit 8200, later writing statistical models in the Air Force's Operations Research branch. Some of that work was recognized with the Israel Defense Prize, the highest award in Israel’s defense establishment.
One habit stuck from all of it: don't trust a number until you know how it came out. So a project of mine usually starts with formalizing the problem and looking for standard / open-source solutions and conventions. Another thing I emphasize is defining a baseline and a train, test and validation split that can't leak, and may reward the fancier model.
- Formal reasoning — reading a frozen Lean 4 prover's internal states mid-proof to predict, early, which attempts will never close the goal, with every label settled by the Lean kernel rather than a proof server.
- Rigorous evaluation — chronological splits over shuffled ones, verifier-checked verdicts over a scorer's say-so, negative results reported as negative, artifact-scored reproductions, closed forms over Monte-Carlo intuition.
- LLMs & agentic pipelines — evaluation harnesses that score what a run actually produced on disk, not what the agent claims.
- Statistics & operations research — experimental design, uncertainty, optimization, and resource-allocation modeling.
Failure prediction from the first N generated tokens: probes on the prover’s internal state vs the tokens-so-far baseline, which stays at chance in those early windows and only becomes predictive once an attempt has ended.
Languages
ML / DL
Formal methods
Scientific & data
Data & infra
- 🌐 Portfolio — amitaminov.github.io
- 👔 LinkedIn — amit-a-94a85822a
- 📧 Email — amit.aminov@mail.huji.ac.il