Semantic Alignment Models for Math and Software Engineering

TL;DR

• The problem: autoformalization — translating natural language math (English, French, …) into formal language math (Lean or another theorem-proving language). The motivation is that human-written proofs are often incomplete, with missing steps the mathematicians may not be aware of, and sometimes outright incorrect. Once formalized, you can run the Lean theorem prover and check whether the theorem was actually proven.
• A sharp target: build a box at least 1000× smaller than frontier models that nevertheless outperforms the largest frontier models on this one task.
• The key property is semantic alignment: two objects represented in different modalities with the same semantic content should be close in the model's embedding space; different semantic content should be far apart. The training recipe is semantic contrastive learning, and the concrete payoff is far more effective retrieval.
• It generalizes: code translation between languages, specification → circuit, and connecting definitions across areas of math to surface relationships and discover new math — all with small models, no frontier access required.
• Current extension: COBOL → Python legacy code translation. No specification is needed because the input program is the specification; they use LLM-driven symbolic execution to generate a test suite from the input, then run it against the output to check semantic equivalence.

Key Points

What autoformalization is and why it matters (~01:18–01:19)

He introduces himself as a professor of computer science at Georgia Tech working broadly in formal methods and neuro-symbolic AI for mathematics, physics, and code, and notes his problem differs from those of the previous two speakers.

Autoformalization means translating natural language math — math written in English, French, and so on — into formal language math, meaning Lean or another theorem-proving language.

Why bother? Because human-written proofs are often incomplete, missing steps that the human mathematicians may not be aware of; and worse, sometimes the proofs are incorrect. Translating into formal language lets you deploy the Lean theorem prover and check whether the theorem was indeed proven.

What "equivalent" means (~01:19–01:20)

The goal is a box that takes natural language math in and produces equivalent formal language math out, where equivalence means semantic equivalence: the semantic content of, say, the Pythagorean theorem going in must be the same as the semantic content of the Lean coming out — it has to talk about right-angle triangles, and the relationship must be the same.

The task they set themselves: build that box at least 1000× smaller than frontier models, maybe smaller still, and train it so it outperforms the largest frontier models on this one task of autoformalization.

Semantic alignment and semantic contrastive learning (~01:20–01:22)

The property he proposes is semantic alignment. The concept isn't new in general — people have discussed it in many settings — but in mathematics it takes a particular meaning: if two objects represented in different modalities have the same semantic content, they should be close by in the model's embedding space; if their semantic content differs, they should be far apart.

Imbuing the model with this property makes it much more effective at autoformalization, and specifically far more effective at retrieval time.

The value isn't confined to natural-to-formal math translation. It also covers code translation from one language to another, going from a specification to a circuit, and connecting definitions from different areas of math — seeing relationships between definitions across areas and thereby discovering new math — all doable with very small-scale models, without frontier model access.

They trained their models using a recipe they call semantic contrastive learning, imbuing the model with the property. The result was a far more powerful model than frontier models on all the benchmarks they tested.

Extending to code translation (~01:22–01:23)

They're now taking the idea into code translation: a tool that takes programs in legacy languages like COBOL and translates them into Python, deploying verification tools and automated testing tools on the input program.

The neat design argument: in this setting you don't need a specification, because the input program is the specification. They use LLM-driven symbolic execution to generate a test suite from the input program, then run that suite against the output to check whether the input and output programs are semantically equivalent. He notes the strong business case for code translation.

Takeaway (~01:23–01:24)

In settings where you have access to formal objects — translating between formal objects, or from an informal object into a formal object in another modality — imbuing the model with the property of semantic alignment is a good way to build a system that scales: much smaller in size, yet still able to scale to very large codebases.

Quotes

"Often human-written proofs are incomplete, meaning they are missing steps, and the human mathematicians may not be aware of that. Worse, sometimes the proofs are incorrect." (~01:19)

The real motivation for autoformalization isn't formalist purity — it's that human proofs contain errors.

"If two objects which are represented in different modalities have the same semantic content, then we want them to be close by in the embedding space of the model." (~01:21)

Semantic alignment in one sentence.

"In this setting, we don't need specifications because the input program is the specification." (~01:23)

Why code translation is an easier formalization target than math.