Ke Zhang
PhD Student in Mathematics • University of California, Riverside
Research Interests
- Gurobi optimization coding repair agent
- Lean4 autoformalization and theorem verification using AI agents
- Tool-augmented LLM reasoning, and tools effect analysis
- Car maintenance, oil change, rotor and brake pad change
Projects
-
Gurobi Code Repair Agent
— AAAI 2026 AI4Research Workshop.
Wrote optimization problem use cases and unit tests, then evaluated an agent that automatically repairs buggy Gurobi models using retrieval-augmented generation, tool execution, and feedback loops. -
Lean4 Autoformalization System
— NeurIPS 2025 LLM Evaluation Workshop (Poster).
Translates mathematical natural language statements into Lean4 code using an agent-based workflow with REPL feedback and theorem checking.
Contact
Email: kzhan153@ucr.edu