Kinglake Research

Rigorous research, applied to hard problems.

Kinglake Research LLC is a research consultancy. We take on technically demanding work in machine learning, mathematical modeling, formal verification, and quantitative finance, and we build AI workflows and software for clients.

Discuss a project
Services

What we do

AI and machine learning research

Research-grade analysis of how models learn and what they compute.

  • Mechanistic interpretability and circuit analysis
  • Training dynamics and diagnostics
  • Experiment design, evaluation, and reproducible pipelines

Mathematics and formal verification

Mathematical models, and machine-checked mathematics with evidence that it says what it should.

  • Mathematical and quantitative modeling
  • Formalization in Lean 4 and Mathlib
  • Faithfulness audits: does the formal statement match the source?
  • Human-readable verification reports for non-specialists

Quantitative research

Systematic trading research with machine learning at its core.

  • Neural-network signals for market-neutral long/short strategies
  • Portfolio construction, backtesting, and robustness testing
  • Risk and regime analysis

AI workflows and software

We also design and build working systems for clients.

  • AI-assisted workflows with built-in verification and review
  • Data pipelines and internal tools
  • Web and mobile applications
Selected work

Recent projects

  • Interpretability. Unsupervised methods for finding the circuits inside large language models as they train.
  • Training dynamics. How optimizers shape the path a model takes during training, from small transformers to GPT-2 scale.
  • Grokking. Early-warning signals for the sudden jump from memorizing to generalizing, and what the learned solutions look like.
  • Formal verification. Complete Lean 4 formalizations of graduate mathematics texts, with audits that the formal statements match the originals.
  • Quantitative finance. A neural-network-driven, market-neutral long/short trading strategy.
About

A small research firm

Kinglake Research is a small, research-led firm. We work directly with each client, keep teams small, and focus on one thing: results that work in practice.

Yongzhong Xu · Co-founder

Mathematician (Ph.D., Rutgers; formerly Courant Institute and Institute for Advanced Study), working on machine learning, formal verification, and quantitative finance.

Research GitHub
Contact

Start a conversation

Tell us about the problem, the timeline, and what a good outcome looks like. We reply to every serious inquiry.