@inproceedings{matsuoka-2026-invariantspec,
title = "{I}nvariant{S}pec: Benchmarking {LLM} Autoformalization of Conservation and Dissipation Laws into Verifiable State-Space Constraints",
author = "Matsuoka, Hikaru",
editor = "Valentino, Marco and
Ferreira, Deborah and
Thayaparan, Mokanarangan and
Ranaldi, Leonardo and
Cheng, Jo-Ku and
Freitas, Andre",
booktitle = "The Proceedings of the 4th Workshop on Mathematical Natural Language Processing ({M}ath{NLP} 2026)",
month = oct,
year = "2026",
address = "Budapest, Hungary",
publisher = "Association for Computational Linguistics",
url = "https://aclanthology.org/2026.mathnlp-main.8/",
pages = "101--111",
ISBN = "979-8-89176-468-2",
abstract = "Mathematical descriptions of dynamical systems denote conjunctions of proof obligations{---}the advection{--}diffusion equation conserves mass and dissipates the $L^2$ energy{---}yet common task designs ask language models to summarize a system with a single structure label, a target wrong by construction for mixed systems. We recast the problem as autoformalization: translating natural language, equations, and stated assumptions into a typed formal specification whose atoms are machine-checkable matrix conditions on a linear state-space generator ($A^{\top}c=0$, $A^{\top}M+MA=0$, $A^{\top}M+MA\preceq 0$, $A^{\top}J+JA=0$). We release InvariantSpec: 12 dynamical systems $\times$ 5 linguistic variants $\times$ 3 modality conditions (180 inputs) with verifier-executable gold specifications, contrastive minimal pairs (boundary conditions, conserved vs. non-increasing, sentence order, linear vs. nonlinear generators), and two systems whose correct answer is not representable by a fixed linear generator. A symbolic verifier checks every predicted obligation and returns typed counterexample feedback; verified specifications are then compiled into constrained generators, including a projector-based parameterization conserving a linear quantity while dissipating a quadratic one. Across four frontier LLMs, single-label structure selection has exact specification match 0.00{---}a ceiling imposed by the answer space, not the models{---}while autoformalization with one round of verifier-guided refinement reaches up to 0.88 with soundness 0.98{--}1.00; the residual gap is dominated by unstated side conditions, not by obligation algebra. Downstream, one-step MSE does not predict long-rollout structural fidelity: spec-compiled generators satisfy every verified conservation or dissipation obligation over 1000-step rollouts (worst conservation defect $2.1\times10^{-10}$), while unconstrained models with equal or better MSE violate them by up to $10^{17}$."
}<?xml version="1.0" encoding="UTF-8"?>
<modsCollection xmlns="http://www.loc.gov/mods/v3">
<mods ID="matsuoka-2026-invariantspec">
<titleInfo>
<title>InvariantSpec: Benchmarking LLM Autoformalization of Conservation and Dissipation Laws into Verifiable State-Space Constraints</title>
</titleInfo>
<name type="personal">
<namePart type="given">Hikaru</namePart>
<namePart type="family">Matsuoka</namePart>
<role>
<roleTerm authority="marcrelator" type="text">author</roleTerm>
</role>
</name>
<originInfo>
<dateIssued>2026-10</dateIssued>
</originInfo>
<typeOfResource>text</typeOfResource>
<relatedItem type="host">
<titleInfo>
<title>The Proceedings of the 4th Workshop on Mathematical Natural Language Processing (MathNLP 2026)</title>
</titleInfo>
<name type="personal">
<namePart type="given">Marco</namePart>
<namePart type="family">Valentino</namePart>
<role>
<roleTerm authority="marcrelator" type="text">editor</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">Deborah</namePart>
<namePart type="family">Ferreira</namePart>
<role>
<roleTerm authority="marcrelator" type="text">editor</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">Mokanarangan</namePart>
<namePart type="family">Thayaparan</namePart>
<role>
<roleTerm authority="marcrelator" type="text">editor</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">Leonardo</namePart>
<namePart type="family">Ranaldi</namePart>
<role>
<roleTerm authority="marcrelator" type="text">editor</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">Jo-Ku</namePart>
<namePart type="family">Cheng</namePart>
<role>
<roleTerm authority="marcrelator" type="text">editor</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">Andre</namePart>
<namePart type="family">Freitas</namePart>
<role>
<roleTerm authority="marcrelator" type="text">editor</roleTerm>
</role>
</name>
<originInfo>
<publisher>Association for Computational Linguistics</publisher>
<place>
<placeTerm type="text">Budapest, Hungary</placeTerm>
</place>
</originInfo>
<genre authority="marcgt">conference publication</genre>
<identifier type="isbn">979-8-89176-468-2</identifier>
</relatedItem>
<abstract>Mathematical descriptions of dynamical systems denote conjunctions of proof obligations—the advection–diffusion equation conserves mass and dissipates the L² energy—yet common task designs ask language models to summarize a system with a single structure label, a target wrong by construction for mixed systems. We recast the problem as autoformalization: translating natural language, equations, and stated assumptions into a typed formal specification whose atoms are machine-checkable matrix conditions on a linear state-space generator (A^pc=0, A^pM+MA=0, A^pM+MA\preceq 0, A^pJ+JA=0). We release InvariantSpec: 12 dynamical systems \times 5 linguistic variants \times 3 modality conditions (180 inputs) with verifier-executable gold specifications, contrastive minimal pairs (boundary conditions, conserved vs. non-increasing, sentence order, linear vs. nonlinear generators), and two systems whose correct answer is not representable by a fixed linear generator. A symbolic verifier checks every predicted obligation and returns typed counterexample feedback; verified specifications are then compiled into constrained generators, including a projector-based parameterization conserving a linear quantity while dissipating a quadratic one. Across four frontier LLMs, single-label structure selection has exact specification match 0.00—a ceiling imposed by the answer space, not the models—while autoformalization with one round of verifier-guided refinement reaches up to 0.88 with soundness 0.98–1.00; the residual gap is dominated by unstated side conditions, not by obligation algebra. Downstream, one-step MSE does not predict long-rollout structural fidelity: spec-compiled generators satisfy every verified conservation or dissipation obligation over 1000-step rollouts (worst conservation defect 2.1\times10⁻10), while unconstrained models with equal or better MSE violate them by up to 10¹7.</abstract>
<identifier type="citekey">matsuoka-2026-invariantspec</identifier>
<location>
<url>https://aclanthology.org/2026.mathnlp-main.8/</url>
</location>
<part>
<date>2026-10</date>
<extent unit="page">
<start>101</start>
<end>111</end>
</extent>
</part>
</mods>
</modsCollection>
%0 Conference Proceedings
%T InvariantSpec: Benchmarking LLM Autoformalization of Conservation and Dissipation Laws into Verifiable State-Space Constraints
%A Matsuoka, Hikaru
%Y Valentino, Marco
%Y Ferreira, Deborah
%Y Thayaparan, Mokanarangan
%Y Ranaldi, Leonardo
%Y Cheng, Jo-Ku
%Y Freitas, Andre
%S The Proceedings of the 4th Workshop on Mathematical Natural Language Processing (MathNLP 2026)
%D 2026
%8 October
%I Association for Computational Linguistics
%C Budapest, Hungary
%@ 979-8-89176-468-2
%F matsuoka-2026-invariantspec
%X Mathematical descriptions of dynamical systems denote conjunctions of proof obligations—the advection–diffusion equation conserves mass and dissipates the L² energy—yet common task designs ask language models to summarize a system with a single structure label, a target wrong by construction for mixed systems. We recast the problem as autoformalization: translating natural language, equations, and stated assumptions into a typed formal specification whose atoms are machine-checkable matrix conditions on a linear state-space generator (A^pc=0, A^pM+MA=0, A^pM+MA\preceq 0, A^pJ+JA=0). We release InvariantSpec: 12 dynamical systems \times 5 linguistic variants \times 3 modality conditions (180 inputs) with verifier-executable gold specifications, contrastive minimal pairs (boundary conditions, conserved vs. non-increasing, sentence order, linear vs. nonlinear generators), and two systems whose correct answer is not representable by a fixed linear generator. A symbolic verifier checks every predicted obligation and returns typed counterexample feedback; verified specifications are then compiled into constrained generators, including a projector-based parameterization conserving a linear quantity while dissipating a quadratic one. Across four frontier LLMs, single-label structure selection has exact specification match 0.00—a ceiling imposed by the answer space, not the models—while autoformalization with one round of verifier-guided refinement reaches up to 0.88 with soundness 0.98–1.00; the residual gap is dominated by unstated side conditions, not by obligation algebra. Downstream, one-step MSE does not predict long-rollout structural fidelity: spec-compiled generators satisfy every verified conservation or dissipation obligation over 1000-step rollouts (worst conservation defect 2.1\times10⁻10), while unconstrained models with equal or better MSE violate them by up to 10¹7.
%U https://aclanthology.org/2026.mathnlp-main.8/
%P 101-111
Markdown (Informal)
[InvariantSpec: Benchmarking LLM Autoformalization of Conservation and Dissipation Laws into Verifiable State-Space Constraints](https://aclanthology.org/2026.mathnlp-main.8/) (Matsuoka, MathNLP 2026)
ACL