Third-year BSc Artificial Intelligence student at Harbin Engineering University, graduating in July 2027. I build AI systems around mathematical reasoning, computer vision, generative models, and machine-verifiable evaluation.
I am currently seeking paid AI/ML, computer vision, and generative AI internships.
| Project | Engineering focus |
|---|---|
| Model Observatory | Dependency-light classification evaluation toolkit with calibration, selective risk, subgroup analysis, drift diagnostics, 29 tests, and deterministic HTML/JSON reports. |
| ProofOrCounter | Model-agnostic prove-or-disprove harness that races Lean 4 proof generation against exhaustive and Z3 finite countermodel search. Verified artifacts only; 5/5 deterministic benchmark cases pass in CI. |
| Uncertainty-Aware QA | Reproducible black-box LLM uncertainty study with semantic clustering, calibration metrics, paired bootstrap intervals, confirmatory pooling, and an offline analysis path. |
| Multimodal Perception | Real-time MediaPipe/OpenCV pipeline combining hand, face, and body landmarks with tested geometry-based gesture and posture events. |
| Reasoning Eval Lab | Reproducible mathematical-reasoning inference and evaluation pipeline with concurrent OpenAI-compatible requests, resumable JSONL runs, answer extraction, and exact/numeric scoring. |
| Robotics Control Lab | Obstacle-avoidance state control and PID self-balancing with anti-windup, deterministic simulation, and a generated closed-loop response artifact. |
| Prompt Storyboard Studio | Validated storyboard-to-prompt compiler with exact continuity checks and a reviewable five-shot generative-video reconstruction. |
- Built an LLM inference and evaluation pipeline for the SAIR mathematical reasoning competition; ranked first university-wide and approximately 80th overall.
- Developed a real-time multimodal hand, face, and body tracking system with OpenCV and MediaPipe landmark geometry.
- Deployed a CVPR 2024 texture-preserving diffusion model on Alibaba Cloud PAI-DSW using an NVIDIA A10 GPU.
- Developing a private automated theorem-proving system that produces verified Lean 4 proofs or finite counterexample certificates. Competition-specific code and protocols remain private pending disclosure clearance.
- Built content and scheduling automation for a commercial driver training school.
Python, C++, PyTorch, TensorFlow, OpenCV, MediaPipe, Lean 4, Z3, LLM inference and evaluation, formal verification, diffusion models, robotics control, finite-model search, reproducible experiments, and GitHub Actions.
Harbin Engineering University
BSc Artificial Intelligence, expected July 2027
Portfolio | Email | Phone | LinkedIn | GitHub Discussion