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 defence 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\conventions. Another thing I emphasize is defining a baseline and a train, test and validaiton split that can't leak, and may reward the fancier model.
- Formal reasoning — fine-tuning LLMs to prove theorems in Lean 4 with GRPO, rewarded by the Lean kernel's accept-or-reject, measured against goal-blind frequency baselines.
- Rigorous evaluation — chronological splits over shuffled ones, frequency-table baselines, 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.
| Project | What it shows |
|---|---|
| Generated Formal Theorem Proofs | A goal-blind 16,850-parameter tactic-frequency Unigram model proves 26.2% of miniF2F-test vs 49.6% for a ~7B neural prover at the same search budget — a floor provers are rarely measured against (in 2021, SOTA GPT-f produced 29% success rate, comparable to the baseline). |
| Room Occupancy | How a shuffled split fabricates skill on sensor time series (macro-F1 inflated 21–62 pts); under an honest chronological holdout a simple QDA (~0.77) transfers while tree ensembles don't. |
| Gaussian Geometry | Three widely-taught covariance "facts" turned into exact, unit-tested statements — including that the "1σ" ellipse holds only ~39% of the mass in 2D, not 68%. |
| Decision Boundary Atlas | SVM overfitting made visible as geometry: one kernel-width sweep fragments the boundary into 282 memorized islands exactly as test accuracy turns over. |
| Agentic Research Advisor | An autonomous paper-reproduction harness graded on the artifacts it produces, not the agent's self-report — honest negatives are first-class. |
| Technical Interviewer | Voice and motion-driven, offline-first technical AI interviewer. |
| TripWise | Couples' trip-planning as a decision-integrity problem — blind-rate-then-reveal enforced by Postgres row-level security + triggers, not the UI. Built quickly with an AI-assisted (vibe-coding) workflow to plan an autumn trip to Italy with my girlfriend. |
A goal-blind baseline vs a ~7B neural prover at an identical best-first search budget.
Languages
ML / DL
Formal methods
Scientific & data
Data & infra
- 🌐 Portfolio — amitaminov.github.io
- 👔 LinkedIn — amit-a-94a85822a
- 📧 Email — amit.aminov@mail.huji.ac.il