Experience

Formal verification of surgical skill-assessment networks

Python · n2v · α,β-CROWN · ONNX · VNN-LIB

• Developed and validated a flat-reformulation method for grouped 1D FCNs that enables formal verification with Star-based tools, bypassing architectural constraints in n2v's slice/concat/ReduceMean handling.
• Certified four robustness properties — noise, output range, segmentation, and monotonicity — on surgical skill-assessment networks across three JIGSAWS tasks using n2v and α,β-CROWN; certified a noise margin 11.7× the physical da Vinci sensor-noise bound at T=10.
• Characterized a two-regime certifiable horizon via T-sweep analysis, identifying verifier approximation looseness (not memory) as the scalability bottleneck, with full cross-verifier agreement at T≤60.
• Contributing a benchmark (ONNX models, VNN-LIB property encodings, verification harness) to VNN-COMP 2026; preparing a case-study paper targeting QEST+FORMATS 2026.

Emotional reasoning app

Python · LangChain · Flutter · Dart · FastAPI

• Designed and implemented a multi-stage AI emotional-reasoning chatbot coach using LangChain and GPT-4, boosting user retention by 31% and engagement by 47%.
• Designed UI for tracking emotions over time and AI-generated summaries of conversations.
• Coordinated between design, emotional-science, and development teams to maintain project vision and ensure timely delivery.

Program Design & Data Structures (Java)

• Hold weekly office hours assisting 100+ students with programming assignments.
• Grade assignments and exams, giving detailed feedback on correctness, efficiency, and readability.