toooold

When a language model tells you “this function is correct,” how much should you trust it? The answer is: not very much — unless the claim comes with a machine-checked proof. This post describes a pipeline that asks an LLM to translate a Python function into Lean 4, proposes a correctness theorem, and then runs five independent gates to decide whether to trust the result. The point is not the translation; it’s the gates.

If you are running local LLMs, you already know the bottleneck isn’t compute; it’s memory. Specifically, the KV cache. As your context window grows, storing Keys and Values for every token eats your VRAM alive. On a standard 16GB consumer GPU, you are typically hard-capped around an 8K context length after loading the model weights.

In December 2025, Tony, Yuhao, and I have published AdvJudge-Zero: Binary Decision Flips in LLM-as-a-Judge via Adversarial Control Tokens https://arxiv.org/abs/2512.17375 . This post serves to clarify the underlying mathematical mechanics of our method, stripping away heuristic explanations to focus purely on Lagrangian optimization and the Principle of Least Action in discrete sequence generation.

It has been a few months since my colleague Tony and I published our paper on Logit Gap Steering. In that work, we demonstrated a practical method for steering LLM behavior—specifically bridging the gap between “Refusal” and “Compliance”—by optimizing token sequences.

Research is a deeply personal and tailored process; it’s not something that regular prompting can replicate. ChatGPT, or any LLM or AI agents, can’t simply find the research gap or invent a groundbreaking idea for you. What this post shares is how I work with AI as a collaborator to transform a wild intuition into a concrete new research direction of logit gap steering*.

When I first read the Manifold-Constrained Hyper-Connections (mHC) paper https://www.arxiv.org/abs/2512.24880 , I didn’t see it as just another optimization trick or a clever use of Sinkhorn iterations, but the other way round. This is physics.

Last weekend, I found myself applying data science in an unexpected setting: a baby shower. The host announced what seemed like a simple party game - guessing the circumference of the mother-to-be’s baby bump. What made this particularly interesting was that I could see everyone else’s guesses on a decorated board, transforming a simple estimation game into a fascinating exercise in probability theory and strategic decision-making.

It is a live blog post of some knowledge snippets of AI to bridge the gap among text books, papers, other blog posts. Most content has been posted on my Linkedin.

In the rapidly evolving field of AI agents, there’s a growing trend towards complex frameworks and libraries. However, for many practical applications, a simpler, more flexible approach can be just as effective. This blog post introduces a lightweight financial agent framework that demonstrates how powerful tool use and orchestration can be achieved without relying on heavy libraries like LangChain or LlamaIndex or CrewAI etc.

The short answer: it’s more nuanced—agentic systems have potential, but only if implemented correctly.

Disclaimer: the open source community and the AI community evolve so fast. This blog post can only include content up to early April 2023. The cover image is generated using Midjourney.

Disclaimer: the following blog post is mostly generated by GPT-4. The image is generated by Midjourney. I used the following prompt to produce a diagram and a short blog post for highlights:

How I teamed up with ChatGPT, an AI language model, to identify and analyze a critical security vulnerability in a JPEG2000 decoder.

Since ChatGPT is good at hallucination, why not make a CatGPT out of it? Let’s engineer the prompt step by step:

Disclaimer: Nothing in this blog is related to the author’s current day-to-day work. The content is neither affiliated nor sponsored by any companies. The story in this post is based on a true event that happened in two parts, six years apart, and is full of nostalgia.

Disclaimer: Nothing in this blog is related to the author’s day-to-day work. The content is neither affiliated nor sponsored by any companies.

Disclaimer: Nothing in this blog is related to the author’s day-to-day work. The content is neither affiliated nor sponsored by any companies. I am not employed by Linkedin.

Disclaimer: Nothing in this blog is related to the author’s day-to-day work. The content is neither affiliated nor sponsored by any companies. The story in this post is NOT based on a true event.

TL, DR