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; previously computer science and mathematics at Brown.
Open to full-time research and research-engineering positions worldwide.
The question
How do you establish trustworthy claims about an AI system when the system, the operator, and the evaluator may each be untrusted?
Cryptography attacks this from below, proving what a computation actually did. Evaluations attack it from above, measuring what a model actually does. Formal methods supply the machinery for checking a claim without trusting the party who made it. My work below is four attempts on different faces of the same problem.
Selected work
Verifiable LLM inference
A compute operator can claim that a particular model produced a particular output without having actually run it, and ordinary logging cannot distinguish the two — the logs are written by the party under suspicion. The work applies zero-knowledge proofs to cryptographic verification of claims about LLM training, inference, and deployment.
My contributions are merged upstream into JamesPetrie/VerInf: a dry-run profiler with a manifest contract, cost model, execution DAG, and partition scorecard, together with cost-model corrections matching the paper’s analysis. I am currently porting the verifier from single-chip to multi-GPU, across both the mathematics and the engineering, and working on mathematical techniques for further optimization.
Upcoming. Multi-GPU results are preliminary; technical write-up expected Q4 2026, for review and publication.
Frontier-model evaluation and red-teaming
Reasoning evaluation, red-teaming, reinforcement-learning environments, and evaluation research on frontier language models, under contract.
Disclosure. This work is subject to confidentiality restrictions. I can discuss the technical categories of work and my own engineering responsibilities, but not much beyond this.
Proof Broker
Automated provers disagree, fail differently, and return certificates in mutually unintelligible formats. Proof Broker takes proof goals from Lean 4 and Rocq, routes them through a shared intermediate representation to SMT solvers, automated theorem provers, and LLM provers, then verifies the returned certificates and lifts the resulting proof terms back into the home system.
The verifier is deliberately fail-closed: it checks that a returned refutation actually refutes the negated goal and reaches a contradiction, and that no axioms were smuggled in along the way. The worked function-composition example closes through a real Vampire invocation, axiom-free.
Boundary. Individual inference steps are not re-derived; the home system’s kernel check is what ultimately closes the proof. Phase 3 (breadth across backends) is in progress — the Vampire path is complete end-to-end, others are not.
Order-invariant ICD-10-CM embeddings
Comorbidity indices compress a patient’s diagnosis history into a single weighted score, discarding both order and interaction. 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, trained on the Nationwide Readmissions Database. The calculator is deployed.
Status. Under review at JAMIA; results are unrefereed.
More work
Systems and performance
- pmacs — Rust-cored, Lua-scripted editor
- kyber-simd-profiling — SIMD post-quantum cryptography across AVX2, ARM NEON-SVE, and RISC-V V, with hardware counters and RAPL energy
- LeVCS — federated version control with signed authority chains
- Weenix — Unix kernel
- TCP/IP stack — written from scratch in Go
Mathematics
- 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
Machine learning and agents
- specification-dilemma — experiment on underspecification in language models
- arcana — Magic: The Gathering rules engine, built as a substrate for reinforcement-learning research