Quang Nguyen

ML research

Short bio

I'm Quang Nguyen. My research explores how symbolic structure and learned representations can work together in machine learning.

I'm also a contributor and maintainer of LemmaScript, a verification toolchain for TypeScript.

I build research software connecting typed programs to transformers, generative models to speech restoration, and formal proofs to the mathematical foundations of learning. My current work includes the Cajal compiler, TEMF with WavJEPA and FiLM conditioning, language-model steering with learned twisting functions and sequential Monte Carlo, and an ELBO formalization in Lean 4.

Research interests

  • Neuro-symbolic learning and program-to-transformer compilation
  • Generative speech restoration and audio representation learning
  • Probabilistic inference and language-model steering with twisted SMC
  • Formal methods and mathematical foundations of machine learning

News

— RE-USE speech enhancement on Apple silicon
Released an independent Swift/MLX/Metal port of NVIDIA NemotronLabs RE-USE, with verified M4 Pro GPU inference, a Mac CLI, and an iPhone/iPad app target. Physical iPhone/iPad testing is pending.

— Lean-verified learning for protected representations
Added proofs that gradient descent learns protected linear encoders and that a specified IID SGD update halves expected population task risk at each step, alongside a counterexample where joint encoder–decoder training gets stuck. These results cover finite linear models with a frozen, already-perfect predictive branch; full nonlinear H-JEPA convergence remains open.

Selected work

Recorded audio passes through a shared Swift, MLX, and Metal RE-USE engine to produce enhanced audio, with Mac and iPhone/iPad interfaces.
Shared inference engine; GPU inference verified on M4 Pro.

RE-USE Apple

An independent Apple port of NVIDIA NemotronLabs RE-USE, with a shared Swift/MLX/Metal engine for a Mac CLI and an iPhone/iPad app target.

code documentation project details

Proposed H-WavJEPA architecture with fine, intermediate, and coarse latent spaces, separate predictors, EMA targets, and per-level losses.
Proposed forecasting design; illustrative horizons.

H-WavJEPA

Hierarchical audio representation research with three learned latent spaces, EMA targets, and a PyTorch Lightning + Hydra training workflow.

code documentation project details

Input Input speech spectrogram from the repository demo. 20 inference steps Output speech spectrogram from the repository demo after 20 inference steps.

RMFSR

An experimental MeanFlow speech-restoration implementation, with PyTorch models, training pipelines, and evaluation tools.

code project details