Ke Zhang
PhD Student in Mathematics • University of California, Riverside
I am a PhD student in Mathematics at UC Riverside. My research sits at the intersection of large language models and formal / scientific reasoning: I build tool-augmented LLM agents for Lean 4 autoformalization and for repairing optimization code, and study how different tool categories causally affect agent performance through factorial experiments. I also work on physics-informed neural networks for nonlinear elasticity on curved surfaces.
Research Interests
- Tool-augmented LLM agents and causal analysis of tool effects
- Lean 4 autoformalization and machine-checkable theorem verification
- Agent-based code repair for optimization models (Gurobi)
- Physics-informed neural networks for nonlinear elasticity on curved surfaces
- Car maintenance, oil change, rotor and brake pad change
Publications
-
Understanding Tool-Augmented Agents for Lean Formalization: A Factorial Analysis
Ke Zhang, Patricio Gallardo, Maziar Raissi, Sudhir Murthy.
ICML 2026 — Under Review. A factorial study of how symbol retrieval, expert drafting, and Lean REPL feedback causally affect compilation and semantic faithfulness on a new 400-theorem graduate-level benchmark. The full agent framework lifts compilation from 26.0% (one-shot) to 89.5% and faithfulness from 28.0% to 60.5%. -
Learning Parameterized Nonlinear Elasticity on Curved Surfaces
Yankang Liu, Ke Zhang, Maziar Raissi, Roya Zandi.
ICLR 2026 — Accepted. A parameter-conditioned physics-informed neural network that represents a continuous family of nonlinear elastic equilibria on curved manifolds from a single trained model. I led the training pipeline and ablation studies. -
Agent-Based Code Repair System for Gurobi Optimization Models
AAAI 2025 Workshop — Accepted. Benchmark of 26 Gurobi problems with 260 unit tests, an LLM-based bug generator, and a RAG-grounded repair agent over the Gurobi Python API, analyzed via fractional factorial design.
Projects
- Lean 4 Autoformalization System – Tool-augmented agent that translates natural-language mathematical statements into Lean 4 code, with symbol retrieval, expert drafting (Herald), and REPL feedback in a closed loop. Evaluated by full factorial design on 400 graduate-level theorems.
- Gurobi Code Repair Agent – Wrote optimization problem use cases and unit tests, then ran them through an agent that automatically repairs buggy Gurobi code using a tool stack with RAG, code execution, and feedback loops.
- Parameterized PINN for Nonlinear Elasticity on Curved Surfaces – Parameter-conditioned physics-informed neural network that learns families of nonlinear elastic equilibria on spheroidal surfaces, generalizing across geometric and material parameters without per-instance retraining (PyTorch, dual NVIDIA RTX A6000).
Contact
Email: kzhan153@ucr.edu