Grounded Proof Completion & Animation

[ibenian]

AlgeBench can take a starting expression and a target expression, ask an LLM to write the step‑by‑step derivation between them, verify every step with a computer‑algebra system, rank how confident we are in each step, and then animate the whole thing as a smooth, morphing transformation on the semantic graph — with a confidence badge on each step that never overclaims.

Quadratic.Roots.mov

(Live Examples)

This post is the 10,000‑ft tour. Each numbered section below is really its own deep‑dive — I'll expand each into a standalone post later.

---

The big picture

One sentence: an LLM writes the math, a CAS judges it, and a deterministic renderer animates it — confidence flows all the way to a badge the user sees.

---

1. How proof completion works

The model never touches graphs. It's given the start and target as LaTeX and asked to emit a single trajectory of steps. Each step is one mathematical move plus the complete expression you reach after it:

field	example
operation	"add $\frac{c}{a}$ to both sides"
expr_latex	x^2 + \frac{b}{a}x = -\frac{c}{a}
justification	"addition property of equality"
change_type	rewrite · solve · substitute · approximate · given

It's a thin DSPy module — dspy.ChainOfThought(ProofCompletionSig) — so the prompt itself is optimizable (MIPROv2/GEPA), and the expert binds the start/target LaTeX from the context graphs before inference.

flowchart LR
  A[start and target as LaTeX] --> B[ChainOfThought]
  B --> C[ProofTrajectory]
  C --> D[step 1 operation expr justification type]
  C --> E[step 2 ...]
  C --> F[step n reaches target]

Loading

The crucial design choice: the model emits full expressions, not graph edits. That keeps it doing what LLMs are good at (math in LaTeX) while the code side owns everything structural.

Here it is end‑to‑end on a product‑rule derivative — a real, unedited CLI run against the uncompiled baseline with refinement and the LLM‑judge off (--attempts 1, no --judge), so you're seeing the raw model + grounding:

$ ./run.sh scripts/proof_completion_derive.py \
    "\frac{d}{dx}\left(x^2 \sin x\right)" "2 x \sin x + x^2 \cos x" \
    --domain calculus --attempts 1

start : \frac{d}{dx}\left(x^2 \sin x\right)
target: 2 x \sin x + x^2 \cos x
(model: baseline (uncompiled))

=== derivation (LaTeX): 4 step(s) ===
   start :   \frac{d}{d x} x^{2} \cdot \sin{\left(x \right)}
   step 1:  🥇 x^{2} \cdot \frac{d}{d x} \sin{\left(x \right)} + \sin{\left(x \right)} \cdot \frac{d}{d x} x^{2}
   step 2:  🥇 x^{2} \cdot \frac{d}{d x} \sin{\left(x \right)} + 2 \cdot x \cdot \sin{\left(x \right)}
   step 3:  🥇 x^{2} \cdot \cos{\left(x \right)} + 2 \cdot x \cdot \sin{\left(x \right)}
   step 4:  🥇 x^{2} \cdot \cos{\left(x \right)} + 2 \cdot x \cdot \sin{\left(x \right)}

result:
  steps convertible : 4/4    (each state is a single sympy-convertible expression)
  math correct      : ✓    (final state reaches the target expression)
  exact graph       : ✗    (identical structure to the parsed target)
  step grounding    : 🥇🥇🥇🥇    (each transition follows from the previous state)
  confidence        : 🥇 Grounded    (4/4 steps verified · endpoint reached)

The model applied the product rule, differentiated each factor, and every transition is symbolically proven (🥇). Note exact graph: ✗ while math correct: ✓ — the final tree isn't node‑for‑node identical to the parsed target (a·b vs b·a ordering), but SymPy confirms they're equal, which is why the endpoint gate still passes.

---

2. How grounding works — semantic graph + SymPy

This is the heart of "grounded." Every state the model wrote is turned into a semantic graph, the graph is reconstructed into a SymPy expression, and each transition state[k‑1] → state[k] is classified by what SymPy can prove.

flowchart TD
  L[state LaTeX] --> G[semantic graph]
  G --> S[graph_to_sympy]
  S --> R{relation to previous state}
  R -->|sympy_equiv holds| EQ[equivalent]
  R -->|solution set is subset| NA[narrows]
  R -->|landmarks or solutions differ| RF[refuted]
  R -->|CAS cannot decide| UN[unknown]
  EQ --> T[tier]
  NA --> T
  RF --> T
  UN --> T

Loading

The checks run cheapest‑first and stop at the first that decides: symbolic equivalence → exact solution‑set containment → squared/branch pair for roots → scaled residual for multiply/divide both sides → parametric narrowing for multivariate → a characteristic fingerprint (real roots, singularities, limits — landmarks, not random sampling) → numeric tolerance for declared approximations. Each consecutive pair collapses to one of five tiers:

Tier	Icon	Meaning
Grounded	🥇	symbolically proven to follow from the previous step
Verified	🥈	strong CAS evidence, short of a full symbolic proof
Plausible	🔹	valid math, but the CAS couldn't decide this step
Unchecked	○	not a single convertible expression (e.g. \pm, \dots)
Refuted	✗	the CAS shows it does not follow

The overall verdict is the weakest link plus an endpoint gate (did the chain actually reach the target?). And the model's change_type is only an advisory claim — SymPy is the judge; a mislabeled step is downgraded one tier.

A wrong middle step like x^2 = 4 → x = 7 parses fine, so it used to slip through. Now it's Refuted — and that isn't hypothetical. Even though the model technically "reached" the target we asked for, grounding refuses to bless the bad step:

$ ./run.sh scripts/proof_completion_derive.py "x^2 = 4" "x = 7" --domain algebra --attempts 1

=== derivation (LaTeX): 2 step(s) ===
   start :   x^{2} = 4
   step 1:  🥇 x = 2
   step 2:  ✗ x = 7
             (refuted: introduces value(s) that do not solve the previous step: 7 — but the step was declared 'rewrite')

result:
  step grounding    : 🥇✗    (each transition follows from the previous state)
  confidence        : ✗ Refuted    (1/2 steps verified · 1 refuted · endpoint reached)

math correct and the endpoint gate both pass — the chain did end at x = 7 — but the overall verdict is ✗ Refuted, because reaching the requested target is not the same as every step being valid. The CAS is the judge.

And here's a longer one with a genuine spread of tiers — deriving the quadratic formula. Every step is individually grounded or verified, yet the overall verdict is honestly held at 🔹 Plausible because the ∨‑form final state isn't the exact ±‑form target we asked for (the endpoint gate, not a weak step):

$ ./run.sh scripts/proof_completion_derive.py \
    "a x^2 + b x + c = 0" "x = \frac{-b \pm \sqrt{b^2 - 4ac}}{2a}" \
    --domain algebra --attempts 1

=== derivation (LaTeX): 8 step(s) ===
   start :   a \cdot x^{2} + b \cdot x + c = 0
   step 1:  🥇 a \cdot x^{2} + b \cdot x = - c
   step 2:  🥈 x^{2} + \frac{b \cdot x}{a} = - \frac{c}{a}
   step 3:  🥇 x^{2} + \frac{b \cdot x}{a} + \frac{b^{2}}{4 \cdot a^{2}} = - \frac{c}{a} + \frac{b^{2}}{4 \cdot a^{2}}
   step 4:  🥇 \left(x + \frac{b}{2 \cdot a}\right)^{2} = - \frac{c}{a} + \frac{b^{2}}{4 \cdot a^{2}}
   step 5:  🥇 \left(x + \frac{b}{2 \cdot a}\right)^{2} = \frac{- 4 \cdot a \cdot c + b^{2}}{4 \cdot a^{2}}
   step 6:  🥈 x + \frac{b}{2 \cdot a} = - \frac{\sqrt{- 4 \cdot a \cdot c + b^{2}}}{2 \cdot a} \vee x + \frac{b}{2 \cdot a} = \frac{\sqrt{- 4 \cdot a \cdot c + b^{2}}}{2 \cdot a}
   step 7:  🥈 x = - \frac{b}{2 \cdot a} - \frac{\sqrt{- 4 \cdot a \cdot c + b^{2}}}{2 \cdot a} \vee x = - \frac{b}{2 \cdot a} + \frac{\sqrt{- 4 \cdot a \cdot c + b^{2}}}{2 \cdot a}
   step 8:  🥇 x = \frac{- b - \sqrt{- 4 \cdot a \cdot c + b^{2}}}{2 \cdot a} \vee x = \frac{- b + \sqrt{- 4 \cdot a \cdot c + b^{2}}}{2 \cdot a}

result:
  steps convertible : 8/8    (each state is a single sympy-convertible expression)
  step grounding    : 🥇🥈🥇🥇🥇🥈🥈🥇    (each transition follows from the previous state)
  confidence        : 🔹 Plausible    (8/8 steps verified · endpoint NOT reached)

Steps 6–8 carry a disjunction (∨) — the two roots — and SymPy grounds the square‑root branch and the algebra around it (🥇/🥈) rather than punting. That disjunction support is recent (#375); without it those steps would have shown as ○ Unchecked ("not a single convertible expression").

---

3. How the animation stays stable — rebasing for stable ids

A smooth morph needs to know which glyph is which across two states — the 2 in c^2 must keep its identity so it glides instead of vanishing and reappearing. We get that by rebasing every state's graph onto the previous one and threading a stable node id through.

The rebase is GumTree‑style: anchor the largest identical subtrees first (by a downward subtree signature), recursively align their descendants, then a content‑only fallback for what changed; genuinely new nodes get a fresh id. Render with to_latex(..., with_ids=True) and every glyph carries \htmlData{n=<id>}. The browser engine then runs a FLIP animation keyed on data-n:

flowchart LR
  P[ids in both states] -->|MOVE| M[translate and scale]
  D[id only in old] -->|DELETE| O[ghost fades out]
  I[id only in new] -->|INSERT| N[fades in last]

Loading

So everything that persists interpolates; only genuinely new pieces fade in and removed pieces fade out. That's the whole trick behind the Manim‑style morph.

---

4. The agent tool that triggers a derivation

The chat agent can produce a derivation on demand. The user asks in natural language; the agent infers the endpoints and calls a tool that returns a verified animation, identical to clicking a node's "Derive" button.

sequenceDiagram
  participant U as User
  participant AI as Chat Agent
  participant T as derive_proof_animation
  participant E as ProofCompletionExpert
  participant V as Grounding
  U->>AI: derive the quadratic formula
  AI->>T: start and target LaTeX
  T->>E: run expert
  E-->>T: trajectory
  T->>V: ground every step
  V-->>T: tiers and overall confidence
  T-->>AI: verified animation payload
  AI-->>U: animated derivation with badges

Loading

Because the payload carries the confidence tiers, the agent can't present hand‑waving as proof — an ungrounded step shows up honestly as Unchecked or Refuted rather than a confident‑looking wrong answer.

---

Where this is going — upcoming improvements

flowchart TD
  CORE[Grounded proof completion and animation] --> R[Refinement loop]
  CORE --> SYNC[Graph and term sync]
  CORE --> CAS[Grounded symbolic ops on the fly]
  CORE --> PAGE[Interactive page generation]
  CORE --> GAME[Gamification]

Loading

• Refinement. Today we rank confidence; next we raise it. A retry loop scores each draft with a blended signal — well‑formedness + tier‑graded grounding + a soft LLM‑judge for clarity/pedagogy — and regenerates against a single threshold, feeding the specific failure back to the model. Hard gates set the floor, the judge shapes the gradient. (All the CLI runs above have this turned off — --attempts 1, no judge — so you're seeing the raw baseline.)
• Graph ↔ term sync. Bidirectional, loop‑safe binding so editing the term updates the semantic graph and vice‑versa — the graph and the algebra stay one object, not two views that can drift.
• Grounded symbolic operations on the fly. A conversational CAS: the user talks to do math — "simplify this", "multiply both sides by $a$", "substitute $u = x+1$" — and each operation is applied and grounded on the live expression.
• Interactive page generation. The user plays with equations and proofs, then drops any of them into a beautifully rendered page alongside other content (charts, text), and saves it.
• Gamification. The AI rolls out little games to make the learner an active participant — "what's the next step?", multiple‑choice moves, predict‑before‑reveal — instead of passively watching the animation.
• Stable-id robustness. On larger or symmetric expressions the GumTree-inspired matcher (top-down, exact-subtree only) still mis-identifies nodes — glyphs not only pop in/out but sometimes slide unintuitively, e.g. the two near-identical branches of a disjunction gliding across each other — so a bottom-up similarity phase and position/parent-aware tie-breaking are the next couple of fixes.

---

TL;DR

An LLM proposes the math, a semantic‑graph + SymPy pipeline grounds every step into one of five honest confidence tiers, and a deterministic rebasing renderer animates the whole derivation with stable ids and per‑step badges — all triggerable straight from chat. Ranking confidence was step one; raising it (refinement), talking math into existence (conversational CAS), and turning it into shareable, playable pages are what's next.