Open to 2026-2027 internships
AI / ML ENGINEERING STUDENT
Building AI systems that hold up under inspection.
My work combines formal reasoning, computer vision, and model evaluation with explicit tests, reproducible artifacts, and clear verification boundaries.
01 / SELECTED WORK
Four projects selected for technical range: verified reasoning, ML observability, real-time perception, and uncertainty analysis. Every claim below links to runnable code or a generated artifact.
$ proofcounter solve semigroup_associativity
strategy lean_generation
result PROVED
certificate build/certificates/associativity.lean
verification Lean kernel accepted
status VERIFIEDRaces Lean 4 proof generation against exhaustive and Z3 finite-countermodel search. Only verified artifacts are accepted.
Dependency-light classification diagnostics covering calibration, selective risk, subgroup gaps, and distribution shift.
Combines hand, face, and pose landmarks into interpretable gesture and posture events with a camera-independent geometry core.
Studies black-box confidence signals using semantic clustering, calibration metrics, paired bootstrap intervals, and confirmatory pooling.
02 / CURRENT RESEARCH
I am leading development of a private SAIR Stage 2 solver that must return either a Lean 4 proof accepted by the kernel or a validated finite operation-table counterexample.
Private while competition disclosure rules are unresolved. No prompts or judge protocols are exposed here.
03 / PROJECT LIBRARY
Public repositories, private competition work, and documented deployment experience.
04 / ENGINEERING PRACTICE
Define metrics, baselines, slices, and failure conditions before presenting a model result.
Label pilots, simulations, synthetic demonstrations, and measured outcomes so they cannot be confused.
Use kernel checks, certificate validation, schema validation, and deterministic tests where the domain allows it.
Prefer documented CLIs, machine-readable artifacts, fixed seeds, and CI over one-off notebook screenshots.
05 / EXPERIENCE
BSc Artificial Intelligence at Harbin Engineering University, expected July 2027.
Leading the private Stage 2 solver and previously led Stage 1 prompt design and evaluation. Ranked first university-wide and approximately 80th overall.
Deployed and exercised a CVPR 2024 implementation on Alibaba Cloud PAI-DSW with an NVIDIA A10 GPU.
Designed prompt sequences, scene composition, and narrative continuity for a future-and-drone technology video.
Supported advertising, client communication, scheduling, and reporting in a remote cross-time-zone role. Campaign work improved conversion by approximately 30%.
06 / TECHNICAL FOUNDATION
PyTorch, TensorFlow, model evaluation, calibration, diffusion models, experiment design
Lean 4, Z3, proof search, finite-model search, symbolic rewriting, proof repair
OpenCV, MediaPipe, landmark geometry, real-time frame processing, multimodal perception
Python, C++, Git, Linux, GitHub Actions, pytest, reproducible CLI workflows
07 / CONTACT
Available for paid AI/ML, computer vision, generative AI, and research engineering internships.