{"data":{"awards":["American Invitational Mathematics Exam (AIME) Qualifier","USACO Silver Division","Quiz Bowl Nationals"],"education":{"coursework":["Abstract Algebra","Number Theory","Abstract Linear Algebra","Discrete Structures","Statistics & Probability","Differential Equations","Data Structures","Computer Architecture","System Programming","Computational Science"],"coursework_tags":[{"name":"System Programming","tags":["systems"]},{"name":"Computer Architecture","tags":["systems"]},{"name":"Data Structures","tags":["software_engineering","systems"]},{"name":"Abstract Algebra","tags":["formal_methods"]},{"name":"Number Theory","tags":["formal_methods"]},{"name":"Abstract Linear Algebra","tags":["formal_methods"]},{"name":"Discrete Structures","tags":["formal_methods"]},{"name":"Statistics & Probability","tags":["quant","ai_ml"]},{"name":"Differential Equations","tags":["quant"]},{"name":"Computational Science","tags":["software_engineering"]}],"dates":"Aug 2025 -- May 2028","degree":"B.S. in Mathematics (Technical GPA: 4.0, Overall GPA: 3.98); James Scholar in the College of LAS","school":"University of Illinois at Urbana-Champaign"},"email":"advayth2@illinois.edu","experience":[{"bullets":["Built a **Streamlit** UI enabling CRUD operations for **300+** JSON configuration files used by an internal Generative AI API and migrated **300+** prompt templates into a **PostgreSQL** database.","Designed a modular configuration system enabling dynamic pipeline updates without code changes, reducing reconfiguration time from **hours to minutes** for internal AI workflows."],"dates":"June 2024 -- Aug 2024","id":"abbvie","name":"AbbVie","subtitle":"Generative AI Platform \\& Workflow Automation Intern","tags":["swe","python","sql","ml"]},{"bullets":["Held **4+ open office hours per week** for **15+ students**, covering every **math and CS course** offered (Advanced Programming, Object Oriented Programming, etc.) and adapting explanations to each learner's prerequisites.","Ran **2 additional hours per week** of dedicated **advanced math support** (Abstract Algebra, Number Theory), walking students through **undergraduate-level proofs** and frameworks beyond the scope of standard coursework.","Tutored supplementary subjects including **AP Chemistry** and **French**, broadening access to on-demand academic support across IMSA's STEM and humanities curriculum."],"dates":"Aug 2023 -- May 2025","id":"imsa_tutoring","name":"Illinois Math and Science Academy","subtitle":"Peer Tutor \\& Special Math Support","tags":["pedagogy","math","cs"]},{"bullets":["Led weekly **USACO study sessions** for **20+ members**, breaking down **competitive algorithms and data structures** (binary search, monotonic stacks, BFS/DFS) into step-by-step implementation walkthroughs.","Aided **5+ members** in advancing to the **Silver Division** within one year of consistent attendance.","Organized quarterly **cross-club outreach events** connecting advanced STEM topics to olympiad problem-solving, growing **general membership to 60+**."],"dates":"Aug 2023 -- May 2025","id":"imsalympians","name":"IMSAlympians (IMSA Competitive Olympiad Club)","subtitle":"President \\& CS Coordinator","tags":["pedagogy","cs","math"]}],"github":"https://github.com/AamindMandragora/","language_tags":[{"name":"Lean4","tags":["formal_methods"]},{"name":"Dafny","tags":["formal_methods"]},{"name":"Python","tags":["software_engineering","ai_ml"]},{"name":"C++","tags":["systems"]},{"name":"C","tags":["systems"]},{"name":"Verilog","tags":["systems","hardware"]},{"name":"Rust","tags":["systems"]},{"name":"SQL","tags":["software_engineering"]},{"name":"React","tags":["software_engineering"]},{"name":"TypeScript","tags":["software_engineering"]}],"languages":["Lean4","Dafny","Python","C++","C","Verilog","Rust","SQL","React","TypeScript"],"linkedin":"https://www.linkedin.com/in/advayth-pashupati/","location":"Chicago, IL","name":"Advayth Pashupati","phone":"+1 (224) 391-2254","projects":[{"bullets":["Developing an interactive **Lean4** proof game hosted on the Lean Game Server comprising **2 worlds** and **24 levels** that teach group theory through guided theorem proving, covering abelian groups, subgroups, and normal subgroups.","Formalized **1,200+** lines of Lean4 encoding identity uniqueness, inverses, cancellation laws, commutators, conjugation, subgroup intersection, and the one-step subgroup test, building a notation-agnostic `MyGroup` typeclass.","Designed progressive level sequences that decompose **formalized proofs** into **structured learning blocks**, with layered hints and narrative annotations guiding players from basic group axioms to advanced subgroup characterizations."],"id":"lean4game","name":"Abstract Algebra, the Game","subtitle":"Interactive Lean4 Proof Game","tags":["formal_verification","math","lean4","pedagogy"]},{"bullets":["Developed a custom memory allocator (malloc, calloc, realloc, free) in pure **C**, outperforming glibc by up to **100\\%** in throughput and achieving over **300\\%** memory reduction on select test cases, placing **3rd out of ~300** students.","Designed a **two-level segregated fit** (TLSF) allocator utilizing **128-bit** bitmask free-list indexing, localized arena allocation, and a deferred-free cache to optimize repeated alloc/free patterns.","Engineered aggressive block-level optimizations, including compressed **32-bit** pointers, boundary-tag coalescing with footer elision, and flag-encoded headers for **O(1)** neighbor status verification."],"id":"malloc","name":"Two-Level Segregated Fit Malloc","subtitle":"High-Performance Memory Allocation","tags":["systems","c","cpp","quant_dev"]},{"bullets":["Developed a multithreaded UDP server in **C** (Linux/Raspberry Pi) to serve as an asynchronous store-and-forward audio relay.","Architected a custom client-server protocol using **POSIX sockets** and **pthreads** to efficiently manage connection lifecycles and message delivery.","Engineered a **lock-free** ring buffer for concurrent audio ingestion, reducing synchronization overhead and improving system latency over mutex-based alternatives."],"id":"audio_relay","name":"Asynchronous Audio Relay","subtitle":"Low-Latency Concurrent Systems \\& Networking","tags":["systems","c","cpp","networking","quant_dev"]},{"bullets":["Built a full-stack platform that translates natural language into executable soft robotics physics simulations via PyElastica (Cosserat rod theory), placing **3rd** on the TRAE track among **200+** participants.","Architected a high-performance **FastAPI** backend utilizing Numba JIT compilation, coupled with a headless Matplotlib and FFmpeg rendering pipeline for end-to-end simulation generation in **under 20 seconds**.","Developed an interactive **React/Vite** frontend featuring real-time simulation visualization and LLM-routed code generation through the Keywords AI gateway."],"id":"squishy","name":"Squishy.ai","subtitle":"LLM-Driven Soft Robotics Simulation Platform","tags":["swe","ml","python","hackathon"]},{"bullets":["Designed, backtested, and deployed **multi-asset algorithmic trading strategies** in Python, utilizing SMA, EMA+RSI, MACD, and statistical arbitrage approaches across **6 symbols**.","Integrated custom strategies into a live simulation framework, executing **40+ trades** over a one-week evaluation period on real-time cryptocurrency and FX market data.","Achieved **positive PnL** across a diverse portfolio including BTC, ETH, SOL, INR, ZAR, and JPY."],"id":"sigecom","name":"SIGEcom","subtitle":"Systematic Trading Strategy Research \\& Simulation","tags":["quant_dev","python","trading","finance"]},{"bullets":["Implemented the **Cox-Ross-Rubinstein** binomial model in Python to price European and American options, verifying convergence toward Black-Scholes benchmark values.","Leveraged **neural network de-Americanization** techniques to convert market American option prices into equivalent European prices, enabling **accurate implied volatility** computation.","Analyzed **early exercise boundaries** and computational efficiency across various market regimes to optimize pricing accuracy."],"id":"fin_eng","name":"Financial Engineering","subtitle":"Quantitative Options Pricing \\& ML-Based Volatility Modeling","tags":["quant_dev","python","finance","ml"]}],"research":[{"bullets":["Researching verified generation of custom constrained decoding strategies (CSDs) that enforce syntactic and semantic correctness on LLM outputs, synthesizing **40+** CSDs to date.","Authoring **500+** lines of verified **Dafny** specifications across **15+** helper functions, formally proving that generated CSDs satisfy termination and grammatical correctness invariants.","Evaluating the framework on HuggingFace models (Qwen, Mistral, Llama 3) across **GSM-Symbolic** and **PDDL** benchmarks, comparing against CRANE and DINGO baselines."],"dates":"Sept 2025 -- Present","id":"focal","name":"FOCAL Lab","subtitle":"Formal Verification \\& Verified LLM Decoding Research","tags":["formal_verification","ml","dafny","python"]}],"tools":["Git","Linux","Tensorflow","NumPy","Jupyter Notebook","MongoDB","FastAPI","PyElastica"]},"source":"cv_data.json","updated":1540000000.0}