Amit Aminov

About

I’m a data scientist and ML researcher with a physics foundation (B.Sc. through Bar-Ilan’s program for youth gifted in mathematics) and years of applied quantitative work. I led an Operations Research and Data Science team in Unit 8200 — hiring, mentoring, and shipping end-to-end ML pipelines — then built statistical models in the IAF’s Operations Research Branch, work recognized with the Israel Defense Prize. In my research M.Sc. at the Hebrew University I work on machine learning for formal reasoning; my thesis reads a frozen theorem prover’s internal states to predict, early, which proof attempts will fail, where a verifier, not a leaderboard, decides what counts. Across all of it I build ML systems with careful evaluation, reproducible experiments, and statistically grounded analysis — I try not to trust a number until I understand how it was produced.

• 2024–Present IAF Operations Research Branch · Israel Defense Prize
• 2023–Present M.Sc. Computer Science (research), Hebrew University of Jerusalem
• 2022–2024 Unit 8200 · Operations Research & Data Science team lead
• 2018–2021 B.Sc. Physics, Bar-Ilan University (gifted-in-math program)

Featured projects

• 

  Internal-State Probes for Kernel-Verified Theorem Proving

  My M.Sc. thesis: small probes read a frozen prover’s hidden states mid-proof and tell, early, which attempts will never close the goal.

  Problem

  A prover samples many proofs per theorem and keeps whichever one Lean accepts, so most attempts are wasted — and the worst ones loop until the token cap, one of them re-emitting the same rewrite lemma 208 times. On the 8B model, 24.4% of failed attempts run longer than anything that ever verified, consuming 49.2% of all generated tokens.

  Method

  MLP and LSTM heads under 3M parameters read the frozen Goedel-Prover-V2’s hidden state at each proof-line start and predict failure, then feed that probability back into generation. Labels come from a robust verification protocol: every proof recompiled in a fresh Lean process, accepted only if it type-checks with no “sorry” and rests on trusted kernel axioms alone.

  Result

  The signal is real and early — ROC-AUC 0.89–0.92 in leakage-safe cross-validation, 0.81–0.86 out of domain, and 0.64–0.79 from only the first 250–4,000 generated tokens, where a token counter sits at chance. Steering generation on that signal is a reported negative result: 35 of 360 theorems solved versus the base’s 41 on 8B, 59 versus 60 on 32B — neither difference significant (paired exact McNemar, p = 0.109 and p = 1.00), so the hypothesis is unsupported rather than steering shown to hurt. Single run; no confidence intervals. The same protocol reproduces Goedel-Prover-V2’s published 32B pass@32 exactly (60=60), produces the first robustly verified 8B score I know of (41), and rejects a constructed proof of “False” that a long-running Lean server accepts.

  Stack Python · PyTorch · Lean 4 · Mathlib · Goedel-Prover-V2 · HPC / Slurm

  Code on GitHub → · Read the thesis (PDF) →

  • LLMs
  • Statistics
• 

  Agentic Research Advisor

  An autonomous agent that reproduces ML papers and is graded on the artifacts it produces, not on what it claims.

  Problem

  Autonomous coding agents will narrate success they never achieved, so running them unattended is a problem of accountability, not capability.

  Method

  A harness that treats on-disk artifacts as the only source of truth, scoring what each run actually produced rather than the agent’s self-report — so incomplete runs and honest negatives become first-class outcomes.

  Result

  A searchable reproduction dashboard; as of July 2026, 252 papers ingested and 47 reproduced with full / partial / minimal verdicts backed by per-paper figures and tests.

  Stack Python · LLM agents · pytest · static dashboard

  Code on GitHub →

  • LLMs
  • Engineering
• 

  Gaussian Geometry

  Turns three widely-taught covariance “facts” into exact, unit-tested statements.

  Problem

  Covariance is the most-taught, least-understood object in data science, and its geometry hides traps practitioners repeat.

  Method

  Closed-form derivations backed by unit tests and animation, in place of eyeball and Monte-Carlo intuition.

  Result

  Rotating a Gaussian and constructing its covariance are the same operation; principal-axis orientation becomes pure noise as the variances equalize; and the “one-sigma” ellipse holds only ~39% of the mass in 2D, not the 68% carried over from one dimension.

  Stack Python · NumPy · Plotly · unit-tested derivations

  Code on GitHub →

  • Statistics
• 

  Decision Boundary Atlas

  Makes SVM overfitting physically visible as the geometry of a decision boundary.

  Problem

  Overfitting is usually argued from the gap between two accuracy curves — hard to see, and easy to miss when validation labels are scarce.

  Method

  A single RBF-SVM kernel-width sweep in 2D PCA space, with the boundary first confirmed two independent ways as a consistency check.

  Result

  Added flexibility stretches and fragments the boundary into hundreds of isolated islands exactly as test accuracy turns over — boundary complexity as an early warning for memorization.

  Stack Python · scikit-learn · PCA · Matplotlib

  Code on GitHub →

  • Machine Learning
  • Statistics
• 

  Technical Interviewer

  Voice and motion-driven, AI-led technical interview that trains you for the real thing — tailored to your target role and seniority, it asks role-planned questions, holds a real spoken back-and-forth, and does what real interviews never do: scores every answer and hands back a readiness report and study plan. Bilingual (EN/HE); runs fully offline with no API key.

  Problem

  Real technical interviews are scarce and give no feedback: an average corporate opening draws ~250 applicants, ~4–6 are interviewed and one is hired (Glassdoor), and ~94% of candidates who want post-interview feedback never get any. There’s nowhere realistic to rehearse a spoken, role-specific interview and learn from it.

  Method

  A voice-driven mock interviewer tailored to role (Data Scientist / Algorithm Researcher / AI Engineer) and seniority (Junior → Staff/Lead): it plans role-specific questions, listens with real-time barge-in in EN and HE, asks follow-ups and hints, and scores every answer on an 8-metric rubric into a readiness report and cross-session study plan. Production-hardened — every dependency degrades to a deterministic offline engine and the loop resists prompt injection — so it runs fully offline with no API key.

  Result

  A role- and seniority-tailored mock interview that gives the rubric feedback and study plan real interviews never do — resilient, prompt-injection-aware, fully offline, and deterministically testable (221 tests).

  Stack FastAPI · React · Gemini · FAISS + MiniLM RAG · pytest

  Code on GitHub →

  • Engineering
• 

  TripWise

  I built TripWise quickly with an AI-assisted (vibe-coding) workflow to plan an autumn trip to Italy with my girlfriend, and it reframes couples’ trip planning as a decision-integrity problem so the first opinion can’t anchor the second.

  Problem

  Shared decisions are distorted by anchoring: the first partner to voice a preference biases the other.

  Method

  Each partner rates options blind; both sets reveal only once everyone has rated everything — and the rule lives in a Postgres row-level-security policy and trigger, not the UI.

  Result

  No client or future frontend can peek early, because the integrity invariant is enforced in the database rather than the interface.

  Stack Next.js · TypeScript · Postgres (row-level security)

  Code on GitHub →

  • Engineering
• 

  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.

  Problem

  With sensor readings taken every ~30 seconds, a shuffled split drops a near-duplicate of almost every test row into training and inflates the score by tens of macro-F1 points.

  Method

  Compared the shuffled split against an honest chronological holdout — trained on the past, tested on a genuinely later window.

  Result

  Evaluated honestly the task is far harder and shaped by drift between sessions: a simple generative model (QDA, macro-F1 ~0.77) transfers, while tuned tree ensembles built on absolute thresholds do not.

  Stack Python · scikit-learn · QDA · signal processing

  Code → · Interactive dashboard → · Original paper (IEEE) → · LinkedIn post →

  • Statistics
  • Signal Processing

Research focus

My research is on machine learning for formal reasoning. My M.Sc. thesis asks whether a theorem prover knows, while it is still writing, that the proof it is producing will fail — and whether that knowledge can be fed back to steer generation. I train small probes, under three million parameters, on the hidden states of a frozen Goedel-Prover-V2, and label every attempt with Lean’s own kernel verdict rather than a proof server’s reply: a proof either type-checks against the trusted axioms or it doesn’t, so nothing is credited for merely looking finished. The signal is there and it is early; the steering is not, and I report that as a negative result.

The same discipline runs through the rest of my work: chronological splits instead of shuffled ones, verifier-checked verdicts instead of a scoring server’s say-so, negative results reported as negative, artifact-scored reproductions instead of agent self-reports, and closed forms in place of Monte-Carlo intuition. It also shows up as system design — invariants placed where they cannot be bypassed. The goal throughout is evaluation you can trust and systems whose results hold up under scrutiny.