Compiling Is Not Correctness: MMFormalizer Turns Physics Diagrams into Verifiable Lean Statements

The problem: from pictures to provable mathematics

The original post discusses a paper led by a University of Hong Kong team (MMFormalizer, arXiv 2601.03017) that hands the classic physicist's task—translating phenomena into equations—to AI. Given an image (a geometry diagram, a physics problem sketch, even a hand drawing), the model writes out the circles, line segments, and arrows—along with information *not* visible in the image—as formal propositions a compiler can verify.

This direction is known as autoformalization: translating human-written mathematics into a language that proof assistants like Lean can read and check. Prior work handled plain text; this paper goes one step further because physics problems inherently come with diagrams, and diagrams are incomplete. An inclined-plane sketch shows no mass, no friction coefficient, and certainly not the words "conservation of energy"—these invisible constraints must be inferred from visual elements and domain knowledge.

Recursive grounding

The paper calls this process recursive grounding:

1. Recognize visual content as basic primitives (points, line segments, angles, mass, temperature). 2. Use domain axioms to assemble primitives layer by layer into proposition chains. 3. Each abstraction step must be backed by visual evidence. 4. A termination condition decides when to stop.

Physical quantities (mass, charge, Planck's constant) each have their own grounding procedure; anything that fails to ground is decomposed further, until the result finally compiles.

PhyX-AF benchmark

The authors claim this is the first multimodal autoformalization method covering Hamiltonian classical mechanics, relativity, quantum mechanics, and thermodynamics simultaneously. They release PhyX-AF, a benchmark of 115 carefully selected problems from MathVerse, PhyX, and two geometry datasets, specifically testing image-based formalization. The appendix case list reads like a physics syllabus: Newton's three laws, quantum tunneling, relativity, a regular hexagonal prism—and one failure case.

The headline finding: three gates, shrinking numbers

Each translation passes through three checks: Compile (does the code compile?), Semantics (is the meaning correct?), and Human Check (do human verifiers accept it?). The gap between these gates is more striking than any single number:

• GPT-5 on MathVerse image problems: 24% compile → 20% semantics → 12% human-verified.

Roughly half of the translations the compiler accepts are semantically wrong, and verified correctness drops further. The compiler only checks types and syntax—not whether the physics is actually right. Writing "a ball falls" as "a ball rises at constant velocity" compiles fine as long as the types are correct.

Other notable results

• Geometry is the hardest domain: on synthetic and analytic geometry, all models drop noticeably; models still struggle with specific length and angle relations, and degrade further on unseen diagram distributions.
• Modality gap: the same model often scores several times higher on text problems than on image problems.
• Qwen3-VL-235B, the strongest open-source model, nearly collapses on physics domains and out-of-distribution synthetic geometry.

Counterintuitive ablations

• On synthetic geometry unseen during training, removing retrieved reference code from a theorem library and letting the model freely synthesize *improves* accuracy—reference answers lock down the output space; withholding them improves generalization.
• Without an explicit recursion termination condition, the recursion tree grows deep and large and the whole synthesis fails. "Knowing when to stop" is not an engineering detail—it is the line between success and failure.
• Grounding with images helps markedly on hard domains like relativity and quantum mechanics; sampling multiple paths (pass@k) also buys points.

Weak models as reviewers

One easily-missed finding: for semantic checking, even the weakest Qwen2.5-VL-72B supervising the strongest open-source model's generated code performs on par with the strongest Gemini-3-Pro. Checking is cheaper than generating, and weak models can serve as competent reviewers—a conclusion familiar to anyone building agent systems.

Takeaway

The paper was posted to arXiv on January 6—months before the "latest breakthrough" framing suggests—and has neither been overturned nor widely deployed, because the three-gate gap remains. Formalization's value is not in solving any single problem, but in converting "what the model says" into "what a compiler can decide," giving verification a handle. But PhyX-AF's numbers show that translating into verifiable form only relocates the problem: from "can't parse it" to "compiles but may not be true." The first gate's signpost is up; the remaining thresholds are still 12% versus 24% apart.