Work
Levi Neuwirth
I work on technical AI assurance: establishing verifiable claims about what a model actually did, when the operator, the evaluator, or the model itself may not be trusted. That question spans cryptography, systems, evaluations, and mathematics, which is roughly the shape of my background.
I am a MARS V fellow with the Cambridge AI Safety Hub, mentored by James Petrie (Future of Life Institute), and a graduate student in computer science and engineering at DTU. I previously studied computer science and mathematics at Brown.
Open to full-time research and research-engineering positions worldwide.
Selected work
Verifiable LLM inference
An operator who claims to have run a model may not have, and the logs that would settle it are written by the party under suspicion.
VerInf, a Future of Life Institute project led by James Petrie, proves LLM inference in zero knowledge with no trusted setup by bounding the unexplained information in an output stream rather than re-running the computation. I built the dry-run profiler (manifest contract, cost model, execution DAG, partition scorecard) and validated it against an archived full-scale Llama 4 Maverick run and live B200 calibration; the measurements also corrected my own cross-shard communication model, from roughly 950 GB to 2.4–2.8 GB per sweep. Since then I have implemented a verifier-transparent weight split, whose partitioned proofs are byte-identical to ordinary ones, built and measured weight caches, and integrated a collaborator’s expert-weight bridge. That integration exposed two verification gaps, which I fixed: an expert-weight root the verifier never compared against policy, and a sumcheck verifier that did not enforce its round count. A later verifier review strengthened the enrollment identity and made main-proof Merkle openings follow the challenged index rather than path directions supplied by the proof. My current work is on multi-GPU proving, which is the ceiling on model scale, context length, and mixture-of-experts breadth.
Ongoing. The profiler, calibration tooling, and accounting corrections are
merged upstream; the weight split, caches, and bridge hardening are on the
public weight-split-model branch. The multi-GPU figures are projections from a
validated cost model rather than measurements at that scale. The verifier fixes
are targeted review, not a full construction audit. Technical write-up expected
Q4 2026, for review and publication.
Proof Broker
Proof Broker separates proof search from trust. Lean and Rocq can dispatch goals through a shared intermediate representation to external SMT solvers, saturation provers, and learned search, while returned evidence is graded, checked, and ultimately reconstructed or replayed as a proof term the home kernel verifies. The search machinery itself never enters the logical trusted base.
The R4 downstream demonstration applies the system to a real VerInf Lean development: 19/19 targeted arithmetic obligations close through broker calls, spanning reconstructed Farkas witnesses, cvc5/Alethe trace replay, certificate-gated tactics, and one explicitly reported oracle-tier case. Integrating the unmodified downstream file also exposed three defects that the broker’s own test suite had missed.
Since R4, R5 consolidated the specification, and R6 evaluated a live language model proposing Farkas certificates behind the unchanged boundary, on a frozen 15-obligation VerInf census with an audited harness. Every certificate-feasible slot returned a verified witness (80 of 80), but proofs covered 6 of 15 obligations (48 of 88 slots), the same at each of eight draws and two more than the deterministic baseline: posing goals and turning certificates into proofs, not finding them, was the constraint. The companion essay reports the result and its two post-collection amendments. Finite-field certificates and broader independent consumers remain open.
Frontier-model evaluation and red-teaming
I design evaluation environments and scoring rubrics for frontier language models, execute models against them, debug agent scaffolds when they fail, and analyze the failures that result. I have led environment design and evaluator calibration; most of it is built in Harbor.
Calibration passes often reveal that a rubric is measuring something other than what the task was designed to measure: a task-design failure, not a grading one. I calibrate before a task is scaled, because redesigning a task is cheap and rescoring a finished run is not.
For a similar methodology on public data, see The Specification Dilemma — pre-registered, matched-pairs, with its instrumentation failures reported in full.
Disclosure. Client identities and specific results are confidential. I can discuss the technical categories of work and my own engineering responsibilities.
Order-invariant ICD-10-CM embeddings
Comorbidity indices compress a patient’s diagnosis history into a single weighted score, discarding the interactions between diagnoses. This work learns a permutation-invariant representation over ICD-10-CM diagnosis-code sets and predicts 30-day unplanned readmission and 30-day post-discharge mortality, built on 113M+ adult hospitalizations from the Nationwide Readmissions Database. Trained on 2016–2020 and tested on 2021–2022, it reaches 0.750 AUROC for readmission against 0.655 for the Charlson index. The calculator is deployed.
Status. Under review at JAMIA; results are unrefereed.
The question
The first three are one problem approached from different sides. Cryptography works from below, certifying properties of a computation without trusting the party that ran it. Evaluations work from above, measuring what a model actually does under conditions you control. Formal methods supply the machinery for checking a claim without trusting its author.
The clinical study is a separate research-engineering line, built and tested at population scale.
The question underneath all of it: how do you establish trustworthy claims about an AI system when the system, the operator, and the evaluator may each be untrusted?
More work
Systems and performance
- pmacs — Rust-cored, Lua-scripted editor
- where-simd-helps — where hand-written AVX2 beats the compiler in ML-KEM, with a reproducible artifact; ARM, RISC-V, and energy next
- LeVCS — federated version control with signed authority chains
- arcana — Magic: The Gathering rules engine, built as a substrate for reinforcement-learning research
- Weenix — Unix kernel
- TCP/IP stack — written from scratch in Go
Mathematics
- Timed guarding in degree-reduction clouds — preprint, revising
- Ball-occupation certificates under coarse graph projections — preprint, revising
- Branch-tube persistence and static coverage in tree-ball geometry — preprint, revising
- The annealed critical window for growing-radius domination in random regular graphs — preprint, revising
Research engineering
- NeuroPose — 3D pose estimation and kinematic analysis, built in Liqi Shu’s laboratory at Brown Neurology
- NeuroAI — ongoing research engineering
Selected essays
- The Specification Dilemma — pre-registered, matched-pairs, with its instrumentation failures reported in full
- Provenance Is Not Warrant — where an artifact came from, and why anyone is entitled to rely on it, are different questions