Cross-Dialect Generalization Without Retraining: Benchmarks and Evaluation of Schema-Derived Constrained Decoding for MLIR

# Cross-Dialect Generalization Without Retraining: Benchmarks and Evaluation of Schema-Derived Constrained Decoding for MLIR
Source: [https://arxiv.org/html/2607.18254](https://arxiv.org/html/2607.18254)
Plawan Kumar Rath Meta plawan@meta\.com This work was conducted in the author’s personal capacity\. The views expressed in this paper are those of the authors and do not reflect the views of Meta\.

###### Abstract

Multi\-Level Intermediate Representation \(MLIR\) underlies modern ML compiler infrastructure including TensorFlow, JAX via StableHLO, PyTorch, Inductor, IREE, etc yet it appears only in trace amounts in code\-LM pretraining corpora\. MLIR is also extensible by design: new dialects ship per application domain, so maintaining a fine\-tuned model per dialect does not scale\. We ask whether inference\-time priors derived mechanically from each dialect’s Operation Definition Specification \(ODS\) can substitute for gradient\-based adaptation\. We make two contributions\. First, we release four natural\-language\-to\-MLIR benchmarks across three dialects; MLIR\-Spec\-150, Linalg\-Spec\-30, StableHLO\-Spec\-30, and StableHLO\-Held\-Out\-200, totaling 410 in\-scope NL→\\toMLIR pairs, plus a 25\-program StableHLO\-Out\-Of\-Grammar stress set and a hand\-authoredn=30n\{=\}30functional reference set \(435 instances total\)\. All artifacts ship under Apache\-2\.0 with Gebru datasheets and Croissant 1\.0 metadata\. Second, on top of these benchmarks we build a three\-layer schema\-derived constraint stack: a context\-free grammar over op signatures \(C1\), type\-domain splits from an ODS\-extracted type lattice \(C2\), and an SSA\-scope validator driving five\-retry rejection sampling \(C3\)\. Porting the stack from arith\+func\+memref\+linalg to StableHLO required no new constraint\-layer code\. Empirically, on dialects whose verifier semantics are dominated by structural constraints, schema\-derived priors let SmolLM2\-1\.7B match or exceed 15B–34B code LMs at 8–25×\\timesthe per\-generation speed: on linalg, SmolLM2 reaches 80\.0% verify\-valid \(three\-seed mean,n=125n\{=\}125, every seed 80\.0%\), beating CodeLlama\-34B, Granite\-Code\-34B, and StarCoder2\-15B by 21 to 44 pp with non\-overlapping CIs, and surviving a same\-family fp16 precision control\. On arith\+func and on the templated parametric StableHLO\-Held\-Out\-200, where verifier semantics turn on attribute values rather than structure, the same baselines match or beat the SLM; we scope these explicitly as non\-win cells\. We release benchmarks, decoder, every per\-prompt generation, and a reproducibility Docker image\.

## 1Introduction

MLIR \(Multi\-Level Intermediate Representation\)Lattneret al\.\([2020](https://arxiv.org/html/2607.18254#bib.bib6)\)has become the compiler infrastructure of choice for modern machine\-learning systems, underpinning TensorFlow’s compiler stack, JAX via StableHLO, PyTorch’s Inductor backend, and open\-source runtimes such as IREE\. Yet MLIR programs appear only in trace amounts in the public code corpora used to pretrain open\-weight LMs, and a model asked to emit MLIR from natural language routinely produces grammatically malformed outputs, references operations that do not exist in the requested dialect, or constructs types that the verifier rejects on sight\. Retraining addresses this in principle, but MLIR is extensible: the community introduces new dialects per application domain, and maintaining a fine\-tuned model per dialect does not scale\.

This paper treats the generation problem as a structural\-priors problem rather than a data problem\. MLIR’s Operation Definition Specification \(ODS\), its TableGen records that declare each operation’s operands, results, type constraints, and structural invariants, offers a uniform, machine\-readable schema shared across dialects\. We ask: on dialects whose verifier semantics are dominated by structural constraints \(operand\-rank parity, type\-domain splits, SSA scope\), do schema\-derived priors let a small LM match or exceed 15B–34B code LMs under matched sampling budgets, and does the construction port mechanically across dialects? The answer separates: the derivation transfers across all three dialects without new constraint\-layer code, but the empirical SLM\-vs\-baseline gap is dialect\- and corpus\-conditional and robust on linalg \(structural\-dominant\), parity\-to\-loss on arith\+func and on templated parametric StableHLO where attribute\-value constraints dominate\.

SmolLM2\-1\.7B\-InstructAllalet al\.\([2025](https://arxiv.org/html/2607.18254#bib.bib17)\)under the fullC1\+C2\+C3C\_\{1\}\+C\_\{2\}\+C\_\{3\}stack, evaluated against CodeLlama\-34BRozièreet al\.\([2023](https://arxiv.org/html/2607.18254#bib.bib18)\), Granite\-Code\-34BMishraet al\.\([2024](https://arxiv.org/html/2607.18254#bib.bib19)\), and StarCoder2\-15BLozhkovet al\.\([2024](https://arxiv.org/html/2607.18254#bib.bib20)\)under the same five\-retry rejection\-sampling budget, robustly wins on linalg \(80\.0% verify\-valid, three\-seed mean at uniformn=125n\{=\}125, half\-range±0\.0\\pm 0\.0pp,\+21\+21to\+44\+44pp over baselines with non\-overlapping CIs\); wins over the 34B baselines on hand\-curated StableHLO\-Spec\-30; is overtaken on the templated parametric StableHLO\-Held\-Out\-200 where the baselines saturate at 98–100%; and is a non\-win cell on arith\+func\. Inference on a single Apple M4 Max laptop runs 8–25×\\timesfaster per generation than the 34B baselines, with no fine\-tuning, reinforcement learning, or distillation: the entire adaptation is at inference time\.

We frame this as a datasets\-and\-evaluation contribution with a methods contribution that exercises the benchmarks\. \(i\)*Datasets:*four NL→\\toMLIR benchmarks; MLIR\-Spec\-150, Linalg\-Spec\-30, StableHLO\-Spec\-30, and StableHLO\-Held\-Out\-200 \(the last a 200\-program parametric op\-signature sweep that checks against author\-curation bias in Spec\-30; 410 in\-scope pairs across three dialects\), plus a 25\-program StableHLO\-Out\-Of\-Grammar stress set and a hand\-authoredn=30n\{=\}30functional reference set that lowers each generation to executable IR for output\-match testing \(435 instances total\), all verifier\-clean at release with difficulty tags, Datasheet\-for\-DatasetsGebruet al\.\([2021](https://arxiv.org/html/2607.18254#bib.bib10)\)records, and Croissant 1\.0MLCommons Croissant Working Group \([2024](https://arxiv.org/html/2607.18254#bib.bib11)\)metadata under Apache\-2\.0; to our knowledge the first published NL→\\toMLIR benchmarks\. \(ii\)*Methods:*a schema\-derived three\-layer constraint pipeline \(CFG over op signatures, type\-domain splits from an ODS lattice, SSA\-scope validator with five\-retry rejection\) extracted mechanically from ODS; porting from arith\+func\+memref\+linalg to StableHLO which is a dialect with different syntax, different scope semantics, and a different downstream verifier \(iree\-compilerather thanmlir\-opt\), required no new constraint\-layer code\. TheC3C\_\{3\}validator admits both a post\-hoc rejection\-sampling form \(used in our measurements\) and an in\-line coupled\-decoder form, with appendix proofs of accepted\-string\-set equivalence\. \(iii\)*Protocol:*an apples\-to\-apples five\-retry rejection\-sampling budget applied identically to all models, closing the constraint\-asymmetry gap that confounds “small model with grammar versus large model with free decoding\.” \(iv\)*Findings:*a robust linalg win, a corpus\-conditional StableHLO result, and an honest non\-win on arith\+func\.

## 2Related Work

#### CFG\-guided decoding\.

Context\-free\-grammar\-guided decoding with token\-level masks is a mature sub\-area of code\-model inference\. Willard and LoufWillard and Louf \([2023](https://arxiv.org/html/2607.18254#bib.bib1)\)formalize efficient mask construction via finite\-state transitions over regular expressions and context\-free grammars; the Outlines library implements this approach, and we use it with the llguidance backend\. Grammar\-Aligned DecodingParket al\.\([2024](https://arxiv.org/html/2607.18254#bib.bib2)\)shows that naive token\-level masking drifts from the CFG\-conditioned distribution it is meant to sample from, and proposes a principled re\-normalization\. Schall and de MeloSchall and de Melo \([2025](https://arxiv.org/html/2607.18254#bib.bib3)\)document a Hidden Cost of Structure: across several small models, constrained decoding produces lower pass\-rates than free decoding, and the effect is sensitive to prompt format\. Our C1 layer is a standard CFG mask over MLIR operation signatures; what distinguishes it is that the grammar is generated mechanically from ODS rather than hand\-written, so the same derivation procedure applies unchanged across dialects\. We replicate the Schall\-and\-de\-Melo setup under three\-shot priming with a bounded\-identifier grammar and do not observe the pass\-rate reversal \(§[6](https://arxiv.org/html/2607.18254#S6)\); we interpret our ablations as a corroborating data\-point on the prompt\-format\-sensitivity claim rather than a rebuttal\.

#### Context\-sensitive constrained decoding\.

Closer to our C3 layer is a smaller body of work on context\-sensitive constrained decoding for formal targets\. SynchromeshPoesiaet al\.\([2022](https://arxiv.org/html/2607.18254#bib.bib7)\)introduces Constrained Semantic Decoding \(CSD\), a per\-step mask procedure that uses target\-language static analyzers \(type checkers, scope analyzers\) to restrict token vocabularies during sampling, evaluated on SQL and Python synthesis\. Type\-Constrained Code GenerationMündleret al\.\([2025](https://arxiv.org/html/2607.18254#bib.bib8)\)integrates a static type\-checker into per\-step decoding for statically\-typed languages with substantial reductions in type\-error rate on a 1B\-scale model\. Correctness\-Guaranteed Code GenerationLiet al\.\([2025](https://arxiv.org/html/2607.18254#bib.bib9)\)extends this direction with a context\-sensitive Tree of Parsers that drives token\-level decoding so generated programs are guaranteed parseable\. Our work differs in three respects\. \(i\) The target is an extensible intermediate\-representation family rather than a general\-purpose programming language, and our C1/C2/C3 layers are derived mechanically from a machine\-readable schema \(ODS\) rather than hand\-implemented against each language’s type system, so a single derivation procedure covers every dialect that ships ODS records \(MLIR core, StableHLO, and any out\-of\-tree dialect that follows the same convention\)\. \(ii\) We prove equivalence between the in\-line coupled decoder and post\-hoc rejection sampling on the same accepted\-string set, with a BPE\-boundary argument that handles subword tokens spanning multiple grammar terminals \(Theorem[A](https://arxiv.org/html/2607.18254#A1.SSx4), Appendix[A](https://arxiv.org/html/2607.18254#A1)\)\. \(iii\) We release four NL→\\toMLIR benchmarks; Synchromesh and the type\-constrained line evaluate on existing code benchmarks but do not release target\-specific datasets\.

#### Small language models for formal targets\.

Language\-model approaches to formal targets have concentrated on proof assistants as shown by Lean tactic generationYanget al\.\([2023](https://arxiv.org/html/2607.18254#bib.bib21)\)and Isabelle whole\-proof synthesisFirstet al\.\([2023](https://arxiv.org/html/2607.18254#bib.bib22)\), and on hardware\-description languages such as VerilogLiuet al\.\([2023](https://arxiv.org/html/2607.18254#bib.bib23)\)\. MLIR has received comparatively little attention as a direct generation target despite its central role in compiler and ML\-systems infrastructure; to our knowledge this is the first work to treat MLIR as a training\-free language\-model generation target at the dialect\-agnostic level\. Our contribution is training\-free; fine\-tuning is an orthogonal axis we do not exercise here but which would compose with the schema\-derived stack\.

## 3Method

#### Pipeline overview\.

Our method takes a natural\-language descriptionxxand produces MLIR codeyyby sampling from a small language model under a three\-layer constraint stackC=\(C1,C2,C3\)C=\(C\_\{1\},C\_\{2\},C\_\{3\}\)derived mechanically from the target dialect’s Operation Definition Specification \(ODS\)\. The three layers cover distinct aspects of MLIR well\-formedness:C1C\_\{1\}is a context\-free grammar over operation signatures,C2C\_\{2\}splits that grammar by operand and result type domain, andC3C\_\{3\}is a dynamic validator that enforces SSA\-scope correctness\.C1C\_\{1\}andC2C\_\{2\}are applied as token\-level masks during decoding;C3C\_\{3\}drives a five\-retry rejection sampler around the masked decoder\. The same derivation procedure applies unchanged across dialects: porting the stack fromarith\+func\+memref\+linalgto StableHLO required no new constraint\-layer code\.

#### Schema extraction\.

We extract ODS records viallvm\-tblgen \-\-dump\-jsonover the LLVM, IREE, and StableHLO TableGen source trees, yielding 276 operation records across the dialects we target\. Each record names an operation’s operands, results, attributes, and structural traits \(e\.g\.,SameOperandsAndResultType,ElementwiseMappable\)\. We flatten the multi\-inheritance class hierarchies and produce two derived structures: \(i\) a per\-dialect operation lattice naming operand and result type constraints, and \(ii\) a per\-dialect attribute lattice naming attribute kinds and value domains\. Both are consumed by theC1C\_\{1\}grammar generator and theC2C\_\{2\}splitter\. \(TableGen’s JSON dump resolves the multi\-inheritance hierarchy correctly; an earlier regex\-based parser resolved only 2 of the 98 linalg operations we need\.\)

#### C1C\_\{1\}: context\-free grammar over op signatures\.

C1C\_\{1\}is a LALR\-compiled context\-free grammar over the MLIR surface syntax restricted to the target dialect’s operation set\. Productions are generated from the flattened ODS: each operation contributes a production naming its mnemonic, operand arity, attribute slots, and result type constraints in the concrete MLIR syntax \(e\.g\.,arith\.addi %a, %b : i32rather than the ODS declaration form\)\. The grammar is compiled to a token\-level automaton and delivered as a logits\-level mask via OutlinesWillard and Louf \([2023](https://arxiv.org/html/2607.18254#bib.bib1)\)with its llguidance backend\. Two engineering choices are critical: explicit whitespace productions \(replacing LARK’s default%ignore WS, which silently exhaustsmax\_tokenswithout grammar progress\) and bounded SSA identifier regexes \(preventing runaway names\)\. With theseC1C\_\{1\}produces 96–99% parse\-valid output across dialects\.

#### C2C\_\{2\}: type\-domain grammar splits\.

C2C\_\{2\}refinesC1C\_\{1\}by splitting productions along type domains read from the ODS type lattice\. For example,arith\.addiis constrained to integer operand and result types,arith\.addfto floating\-point types, andarith\.cmpitakes the integer comparison predicate vocabulary \(eq, ne, slt, …\) whilearith\.cmpftakes the floating\-point predicate vocabulary \(oeq, olt, une, …\)\. In linalg the splits encode richer constraints:linalg\.matmulonmemref<M×\\timesK×\\timesf32\>bymemref<K×\\timesN×\\timesf32\>requires the inner dimension to be consistent across operands;linalg\.transposeconstrains the permutation attribute to match the source memref rank\. Each split is determined mechanically from the ODS record’s trait set e\.g\.,SameOperandsAndResultTypeimplies a single type domain across all positions, and we do not hand\-author splits per dialect\.

#### C3C\_\{3\}: SSA\-scope validator\.

C3C\_\{3\}is a dynamic validator over SSA uses\. Given a generated MLIR fragment, it parses line\-by\-line, maintains a per\-function symbol table seeded with the function’s parameter list, updates the table at each SSA definition site, and validates each use site against the conjunction \(name\-in\-scope∧\\landtype\-matches\-declaration\)\. On a validation failure the fragment is rejected and the decoder retries\. We use a five\-retry budget: the first attempt samples greedily \(temperature 0\) so it coincides with a pureC1\+C2C\_\{1\}\+C\_\{2\}decode on accept; subsequent retries use temperature 0\.8 to sample a different completion\. Onn=200n\{=\}200SmolLM2arith\+funcgenerations, the validator’s confusion matrix againstmlir\-opt \-\-verify\-diagnosticsshows zero false rejects \(Fig\.[1](https://arxiv.org/html/2607.18254#S3.F1)\) which is a property that holds on the SmolLM2 output distribution but is not universal, as Appendix[A](https://arxiv.org/html/2607.18254#A1)discusses\.

![Refer to caption](https://arxiv.org/html/2607.18254v1/x1.png)Figure 1:C3C\_\{3\}scope\-validator confusion matrix vsmlir\-opton 200 SmolLM2 \+C1C\_\{1\}generations\. The \(scope FAIL, verify PASS\) cell is zero*on SmolLM2 outputs*\. On 34B model distributions \(CodeLlama\), the same cell is non\-zero, see Appendix[A](https://arxiv.org/html/2607.18254#A1)“zero\-false\-reject is distribution\- specific” and the−22\.2\-22\.2pp CodeLlamaC3C\_\{3\}drop in Table[3](https://arxiv.org/html/2607.18254#S5.T3)\.
#### In\-line coupled decoder \(theoretical companion\)\.

The post\-hoc validator admits an equivalent in\-line reformulation as a coupled state machine; Appendix[A](https://arxiv.org/html/2607.18254#A1)formalizes the construction and proves soundness, BPE\-refined coverage, and equivalence to post\-hoc rejection sampling \(Theorems 1–3\)\. All empirical results in this paper use the post\-hoc form; the in\-line implementation’s empirical gap is reported in §[7](https://arxiv.org/html/2607.18254#S7)and §[8](https://arxiv.org/html/2607.18254#S8)\.

## 4Experimental Setup

### 4\.1Models

Primary: SmolLM2\-1\.7B\-InstructAllalet al\.\([2025](https://arxiv.org/html/2607.18254#bib.bib17)\)\(MLX fp16\)\. Baselines: CodeLlama\-34BRozièreet al\.\([2023](https://arxiv.org/html/2607.18254#bib.bib18)\)Q4\_K\_M, Granite\-Code\-34BMishraet al\.\([2024](https://arxiv.org/html/2607.18254#bib.bib19)\)Q4\_K\_M, and StarCoder2\-15B:instructLozhkovet al\.\([2024](https://arxiv.org/html/2607.18254#bib.bib20)\)Q4\_K\_M \(all via Ollama / llama\.cpp\)\. The Outlines/llguidance backend used for C1\+C2Willard and Louf \([2023](https://arxiv.org/html/2607.18254#bib.bib1)\)is fixed across all SmolLM2 cells\.

### 4\.2Benchmarks

Evaluating a natural\-language\-to\-MLIR generation system requires paired \(NL, MLIR\) data that, to our knowledge, is not available in any published benchmark\. Recent NL\-to\-code benchmarks released through different venues such as HumanEvalChenet al\.\([2021](https://arxiv.org/html/2607.18254#bib.bib12)\), MBPPAustinet al\.\([2021](https://arxiv.org/html/2607.18254#bib.bib13)\), CodeContestsLiet al\.\([2022](https://arxiv.org/html/2607.18254#bib.bib14)\), APPSHendryckset al\.\([2021](https://arxiv.org/html/2607.18254#bib.bib15)\), MultiPL\-ECassanoet al\.\([2023](https://arxiv.org/html/2607.18254#bib.bib16)\), pair natural\-language problem statements with programs in general\-purpose programming languages, and none pairs NL with MLIR or any other production compiler intermediate representation\. We therefore construct four benchmarks from scratch, spanning three dialects, summarized in Table[1](https://arxiv.org/html/2607.18254#S4.T1)\.

MLIR\-Spec\-150: 150 hand\-authored NL→\\toMLIR pairs,arith\+func\+memref, difficulty mix 38/44/18% easy/medium/hard, all verify\-clean\.Linalg\-Spec\-30: 30 hand\-authored pairs for the 12 linalg named ops in scope \(matmul, matvec, fill, copy, transpose, broadcast, add, sub, mul, div, exp, abs\) under memref semantics\.StableHLO\-Spec\-30: 30 hand\-authored StableHLOOpenXLA Project \([2024](https://arxiv.org/html/2607.18254#bib.bib4)\)pairs covering 10 op families\.StableHLO\-Held\-Out\-200: 200 programs generated by a parametric sweep over the StableHLO opset \(7 op families×\\times6 dtypes×\\timesmultiple shape ranks; 585 raw candidates filtered to 200iree\-compile\-cleanIREE Project \([2024](https://arxiv.org/html/2607.18254#bib.bib5)\); see §[5](https://arxiv.org/html/2607.18254#S5)\) which is a held\-out corpus that reduces author\-design bias in the StableHLO evaluation\.StableHLO\-Out\-Of\-Grammar\-25: 25 programs using StableHLO ops outside our 10\-op grammar, used to characterize graceful\-degradation behavior\.L3 held\-out: filtered subsamples of the MLIR test corpus, used as prompt fillers\. A separate hand\-authored functional reference set \(n=30n\{=\}30,eval/functional/\) is released as evaluation evidence rather than as part of the test set; see §[7](https://arxiv.org/html/2607.18254#S7)\.

Table 1:Benchmark summary: the four released benchmarks plus the out\-of\-grammar stress set\. Total: 410 in\-scope NL→\\toMLIR pairs across three dialects, with a 25\-program out\-of\-scope supplement\.Reuse scenarios beyond this paper’s protocol are itemized in the datasheet \(Appendix[E](https://arxiv.org/html/2607.18254#A5)\)\.

### 4\.3Statistics

Paired bootstrap \(10 000 resamples, 95% CI percentile method\) aligned by prompt\_id\. All tables reportnnper cell\.

#### Power analysis\.

Atn=200n=200\(arith\+func\) and baseline ratep=0\.55p=0\.55, the minimum detectable effect \(MDE\) atα=0\.05\\alpha=0\.05,1−β=0\.801\-\\beta=0\.80\(two\-proportion normal\-approximation\) is∼9\.8\\sim\\\!9\.8pp\. Our observed\+13\+13pp C3 lift atp<0\.0001p<0\.0001clears this comfortably\. Atn=125n=125\(linalg\) withp=0\.68p=0\.68baseline, MDE is∼11\.4\\sim\\\!11\.4pp; our linalg C3 effect is\+0\.8\+0\.8pp \(below MDE — we report it as null with CI\[0\.0,\+2\.4\]\[0\.0,\+2\.4\]pp rather than “significant”\)\. The paper’s main claims survive a conservative per\-dialect power bound\.

### 4\.430B baseline protocol

C1on Ollama is implemented as rejection sampling against the LARK parse grammar with up to 5 retries \(llama\.cpp does not accept LARK masks\)\. This is weaker than the SLM’s token\-level masked decoding; we document the asymmetry and note that raw 30B free\-decoding rates are much lower \(0\.8% CodeLlamaarith\+func, 17\.0% Granite\)\.

## 5Results

#### Headline metrics\.

Under the fullC1\+C2\+C3C\_\{1\}\+C\_\{2\}\+C\_\{3\}stack at seed\-0, SmolLM2\-1\.7B reaches 67\.5% verify\-valid on arith\+func \(n=200n\{=\}200\) and 72\.8% on linalg \(n=125n\{=\}125\), tracking a constraint\-layer ladder of34\.5→54\.5→54\.5→67\.5%34\.5\\to 54\.5\\to 54\.5\\to 67\.5\\%on arith\+func and49\.6→68\.0→72\.0→72\.8%49\.6\\to 68\.0\\to 72\.0\\to 72\.8\\%on linalg \(Table[2](https://arxiv.org/html/2607.18254#S5.T2)\)\. Under matched five\-retryC1C\_\{1\}rejection sampling, CodeLlama\-34B reaches 82\.0% / 56\.8% and Granite\-Code\-34B reaches 27\.0% / 33\.6% on the same pools\. These are seed\-0 ladder measurements; the three\-seed uniform\-nnapples\-to\-apples comparison is below\.

Table 2:Constraint\-layer progression on SmolLM2\-1\.7B and two 15B/34B baselines, seed\-0 ladder run \(single seed,n=200n\{=\}200arith\+func /n=125n\{=\}125linalg; verify\-valid rate with 95% bootstrap CI in brackets\)\. This view supports the constraint\-layer\-progression analysis in §[6](https://arxiv.org/html/2607.18254#S6)within a single seed; all directional cross\-system claims use the three\-seed uniform\-nnmeans in Table[3](https://arxiv.org/html/2607.18254#S5.T3)and the per\-seed rates in Table[7](https://arxiv.org/html/2607.18254#A4.T7)\.
#### Apples\-to\-apples comparison\.

Table[3](https://arxiv.org/html/2607.18254#S5.T3)reports the matched\-budget five\-retryC1\+C3C\_\{1\}\+C\_\{3\}comparison atn=200n\{=\}200arith\+func andn=125n\{=\}125linalg, three\-seed uniform\-nnwith paired prompts; a Granite\-Code\-8B\-fp16 cell on linalg controls for precision\. On linalg, SmolLM2 attains 80\.0% \(every seed at 80\.0%, half\-range±0\.0\\pm 0\.0pp\), exceeding CodeLlama\-34B \(58\.7%\) by\+21\.3\+21\.3pp, Granite\-34B \(35\.7%\) by\+44\.3\+44\.3pp, and StarCoder2\-15B \(54\.9%\) by\+25\.1\+25\.1pp with non\-overlapping CIs across all four systems; the fp16 8B control trails by 29\.9pp at matched precision, so the gap is not a quantization artifact\. On arith\+func, SmolLM2 \(53\.2%,±1\.8\\pm 1\.8pp\) is within CI of CodeLlama\-34B \(59\.8%\) and Granite\-34B \(51\.5%\), trails StarCoder2\-15B \(66\.8%\) by 13\.6pp with non\-overlapping CIs, and is dominated by Granite\-Code\-8B\-fp16 \(68\.2%, pairedΔ\\Delta\+15\.0\+15\.0pp,p<0\.001p<0\.001\) and we scope arith\+func explicitly as a non\-win cell\. CodeLlama\-34B’s verify\-valid drops 22\.2pp from its parse\-only Table[2](https://arxiv.org/html/2607.18254#S5.T2)rate to itsC3C\_\{3\}\-gated Table[3](https://arxiv.org/html/2607.18254#S5.T3)rate on arith\+func, the largest such delta in the matrix; the corresponding linalg delta is\+1\.9\+1\.9pp within noise \(Appendix[A](https://arxiv.org/html/2607.18254#A1), distribution\-specific zero\-false\-reject remark\)\.

Table 3:Apples\-to\-apples C3 comparison, 3\-seed mean at uniformnn\(n=200n\{=\}200per seed arith\+func;n=125n\{=\}125per seed linalg\); across\-seed half\-range in parentheses\. Granite\-Code\-8B\-fp16 is a same\-family precision control on both dialects \(§[7](https://arxiv.org/html/2607.18254#S7)\)\.
#### Cross\-IR generalization \(StableHLO\)\.

Porting the same pipeline mechanically to StableHLOOpenXLA Project \([2024](https://arxiv.org/html/2607.18254#bib.bib4)\)\(verifier:iree\-compile \-\-iree\-input\-type=stablehlo \-\-compile\-to=inputIREE Project \([2024](https://arxiv.org/html/2607.18254#bib.bib5)\); toolchain status in Appendix[C](https://arxiv.org/html/2607.18254#A3)\) without new constraint\-layer code, SmolLM2 \+C1\+C3C\_\{1\}\+C\_\{3\}verifies at 63\.3% on hand\-curated Spec\-30 \(n=30n\{=\}30\) and 61\.5% on the parametric Held\-Out\-200 \(n=200n\{=\}200\)\. The two corpora diverge sharply for the 15B/34B baselines \(Table[4](https://arxiv.org/html/2607.18254#S5.T4)\): on Spec\-30, SmolLM2 leads the 34B baselines by\+26\.6\+26\.6to\+30\.0\+30\.0pp and sits within bootstrap CI of StarCoder2\-15B; on Held\-Out\-200 the same baselines saturate at 98–100% and SmolLM2 trails by−36\.5\-36\.5to−38\.5\-38\.5pp with paired\-bootstrap CIs excluding zero\. We read this as a benchmark\-design finding: hand\-curated Spec\-30 prompts stress the baselines while parametric Held\-Out\-200 templates do not, so Spec\-30 is the discriminating corpus and Held\-Out\-200 is most useful as a within\-model robustness probe; the SLM\-vs\-baseline lead is retained on Spec\-30 and not extended to Held\-Out\-200\. On Out\-Of\-Grammar\-25,C1\+C3C\_\{1\}\+C\_\{3\}correctly emits 0/25 \(the grammar cannot produce ops it does not model which is the system’s intended failure mode\), while free decoding produces 3/25, reflecting pretraining leakage rather than a property of the constrained system\.

Table 4:StableHLO cross\-system comparison\. SmolLM2\-1\.7B at full stack \(C1\+C3C\_\{1\}\+C\_\{3\}\) vs the three Ollama baselines under matchedC1\+C3C\_\{1\}\+C\_\{3\}with 5\-retry rejection, on the three released StableHLO benchmarks\. SmolLM2 constraint\-ladder on StableHLO:26\.7→63\.3→63\.3%26\.7\\to 63\.3\\to 63\.3\\%\(Spec\-30\) and44\.0→57\.0→61\.5%44\.0\\to 57\.0\\to 61\.5\\%\(Held\-Out\-200\) for free→\\toC1C\_\{1\}→\\toC1\+C3C\_\{1\}\+C\_\{3\}; the\+C2\+C\_\{2\}layer is silent on StableHLO because operand types are constrained structurally rather than by named domain split\.
#### Verify\-valid vs functional correctness\.

The headline metric is structural; we report the functional gap directly in the body rather than only as a limitation\.

Table 5:Verify\-valid vs functional correctness\. Verify\-valid is the 3\-seed mean on the primary corpus \(n=200n\{=\}200for arith\+func,n=125n\{=\}125for linalg\+memref,n=30n\{=\}30for StableHLO\)\. Output\-match is on the hand\-authored functional set \(n=30n\{=\}30total, 10 per dialect\)\.The signed gap is interpretable per\-dialect\. On arith\+func the functional rate exceeds the structural rate because then=30n\{=\}30functional pool selects easier prompts than then=200n\{=\}200evaluation pool\. On linalg the−60\-60pp gap is dominated by a wrapper\-shape artifact rather than a correctness failure: 8/10 linalg generations are verify\-valid but only 4/10 lower under then=30n\{=\}30set’s static\-shape wrapper convention, and only 2/10 of those match output\. The verifier\-clean\-but\-wrong\-output rate on the executable subset is 2/4 \(50%\), comparable to the StableHLO and arith\+func rates; the rest is a wrapper\-convention artifact of then=30n\{=\}30set, not a property of the model or constraint stack\. We disclose both numbers because either alone is misleading: 80% verify\-valid alone overstates capability, and 20% output\-match alone conflates wrapper\-shape mismatches with semantic errors\.

#### Efficiency frontier\.

SmolLM2C1\+C2\+C3C\_\{1\}\+C\_\{2\}\+C\_\{3\}runs at 1\.65–1\.86 s/gen on M4 Max vs≈16\{\\approx\}16s \(CodeLlama\-34B \+C1C\_\{1\}\) and≈40\{\\approx\}40s \(Granite\-34B \+C1C\_\{1\}\) under the same 5\-retry budget which is 8–25×\\timesfaster, at higher verify\-valid on linalg and lower on arith\+func\. Full frontier \(Fig\.[4](https://arxiv.org/html/2607.18254#A4.F4)\), qualitative example, and summary\-of\-claims \(Table[8](https://arxiv.org/html/2607.18254#A4.T8)\) are in Appendix[D](https://arxiv.org/html/2607.18254#A4)\.

## 6Ablations

![Refer to caption](https://arxiv.org/html/2607.18254v1/x2.png)Figure 2:SmolLM2\-1\.7B verify\-valid vs constraint level\. Different layers dominate on different dialects: C3 drives the arith\+func lift \(\+13\.0\+13\.0pp,p<0\.0001p<0\.0001\); C2 drives the linalg lift \(\+4\.0\+4\.0pp,p=0\.006p=0\.006\)\. Error bars are 95% bootstrap CIs\.Supporting figures \(error\-category progression, paired\-bootstrap deltas, HCS replication\) and the per\-error\-category table are in Appendix[D](https://arxiv.org/html/2607.18254#A4)\.

#### C1→\\toC1\+C2 onlinalg:\+4\.0\+4\.0pp verify

\(paired bootstrap, CI\[\+0\.8,\+8\.0\]\[\+0\.8,\+8\.0\],p=0\.0061p=0\.0061\)\. First statistically meaningful C2 effect: linalg’s ins/outs structural typing benefits from C2 splits\.

#### C1\+C2→\\toC1\+C2\+C3 onarith\+func:\+13\.0\+13\.0pp verify

\(paired bootstrap, CI\[\+8\.5,\+18\.0\]\[\+8\.5,\+18\.0\],p<0\.0001p<0\.0001\)\. OnlinalgC3 adds only\+0\.8\+0\.8pp because the target error class \(cross\-SSA type\) is already near\-zero after C2\.

#### Hidden Cost of Structure \(HCS\)\.

We replicate the RANLP 2025 setup\. In our stack \(3\-shot priming \+ bounded\-identifier grammar \+ type\-domain splits\),HCS reversal is not observed: C1 is monotone beneficial on both SmolLM2 \(\+20\.0\+20\.0pp vs free,p<0\.0001p<0\.0001\) and Phi\-3\.5\-mini \(\+7\.5\+7\.5pp,p<0\.0001p<0\.0001\)\. The phenomenon appears setup\-conditional; modern constraint engineering absorbs it\.

## 7Limitations

#### 30B “C1” is rejection sampling, not token\-level masked decoding\.

llama\.cpp does not accept LARK grammars, so our 15B/34B baselines \(CodeLlama, Granite\-Code, StarCoder2 via Ollama\) generate freely and accept the first of 5 retries that parses under the LARK coverage grammar which is a weaker constraint enforcement than SmolLM2’s true token\-maskedC1C\_\{1\}via Outlines/llguidance\. Closing this would require integrating llguidance into llama\.cpp or running a 15B/30B model through MLX, neither of which is on the single\-laptop budget for this paper\.

#### Verify\-valid≠\\neqfunctional correctness\.

Table[5](https://arxiv.org/html/2607.18254#S5.T5)gives per\-dialect verify\-vs\-functional rates on then=30n\{=\}30hand\-authored functional reference set\. The set is small and bounds the ratio on this dialect mix rather than substituting for at\-scale random\-input testing; the linalg gap is dominated by a static\-shape wrapper artifact \(4/10 verify\-valid generations rejected at lowering\), not by computational error\. Closing this gap which is a larger functional benchmark plus a signature\-conformance constraint layer \(provisionalC4C\_\{4\}\), is the headline open problem \(§[8](https://arxiv.org/html/2607.18254#S8)\)\.

#### arith\+funcis parity\-to\-loss; StableHLO is corpus\-conditional\.

At three\-seed uniform\-nn\(Table[7](https://arxiv.org/html/2607.18254#A4.T7)\), linalg is robust \(all three seeds at 80\.0%,±0\.0\\pm 0\.0pp;\+21\+21–4444pp over baselines with non\-overlapping CIs\), arith\+func is parity\-to\-loss \(within CI of the 34B baselines, trailing StarCoder2\-15B by 13\.6pp non\-overlapping\), and StableHLO holds only on Spec\-30 \(baseline saturation on Held\-Out\-200, §[5](https://arxiv.org/html/2607.18254#S5)Table[4](https://arxiv.org/html/2607.18254#S5.T4)\)\. The headline is dialect\- and corpus\-specific\.

#### Single SLM family, single hardware, single version pin\.

Primary results use SmolLM2\-1\.7B\-Instruct \(Phi\-3\.5\-mini appears only in the §[6](https://arxiv.org/html/2607.18254#S6)HCS replication\); we do not sweep the broader SLM landscape\. All numbers are collected on a single Apple M4 Max laptop with SmolLM2 at fp16 and the 15B/34B baselines at Q4\_K\_M; reproducibility on CUDA, CPU\-only, or larger Apple Silicon is untested\. The verifier toolchain is pinned to LLVMllvmorg\-19\.1\.7andiree\-compiler 20241104\.1068; verify rates may shift across MLIR\-core versions and we do not characterize that drift\.

#### Quantization asymmetry, controlled\.

A same\-family Granite\-Code\-8B\-fp16 control bounds the fp16\-vs\-Q4 gap at\+14\.4\+14\.4pp linalg /\+16\.7\+16\.7pp arith\+func\. The linalg lead survives \(8B\-fp16 still trails SmolLM2 by 30pp\); on arith\+func the 8B\-fp16 baseline beats SmolLM2 by\+15\.0\+15\.0pp paired \(p<0\.001p<0\.001\), strengthening the non\-win scoping\. A 30B\-fp16 cell does not fit the laptop budget\.

#### Grammar coverage\.

The released grammars coverarith\+func\+memref, linalg \(12 named ops\), and StableHLO core \(∼40\{\\sim\}40ops\); other dialects \(scf, affine, gpu, async, transform, tensor, vector\) are not covered, though the samellvm\-tblgen→\\togrammar pipeline applies\. Out\-of\-grammar prompts return no output rather than malformed IR \(§[5](https://arxiv.org/html/2607.18254#S5)\)\.

#### In\-line coupled decoder\.

Theorem[A](https://arxiv.org/html/2607.18254#A1.SSx4)establishes equivalence to post\-hoc rejection sampling, but our attempted in\-line implementation reachesmax\_tokensbefore grammar accept on every prompt; all reported numbers use post\-hoc rejection sampling \(§[8](https://arxiv.org/html/2607.18254#S8)\)\.

## 8Future Work

The most consequential gap is the structural\-vs\-functional distinction \(§[7](https://arxiv.org/html/2607.18254#S7)\)\. Closing it requires two pieces: an automated lowering harness driving generated MLIR through the canonical pass pipeline \(mlir\-optforarith\+func,iree\-compileforlinalg/StableHLO\) into an executable, and a reference\-output oracle; C/PyTorch implementations run on shared inputs, or property\-based comparators for shape\-polymorphic prompts\. The releasedn=30n\{=\}30functional reference set is a partial step \(Table[5](https://arxiv.org/html/2607.18254#S5.T5)\); a larger benchmark with reference implementations and random\-input testing, a strict superset of the current verify\-valid corpus, is the most important next release\.

A second thread isC4C\_\{4\}, a shape\-inference\-aware constraint layer\. The per\-op linalg breakdown \(Fig\.[9](https://arxiv.org/html/2607.18254#A4.F9)\) shows SmolLM2 \+C1C\_\{1\}\+C2C\_\{2\}\+C3C\_\{3\}approaches 100% on elementwise ops \(fill,copy,exp,abs\) but trails on shape\-reasoning ops \(transpose,broadcast\), where the residual “other” error bucket \(Table[6](https://arxiv.org/html/2607.18254#A4.T6)\) is dominated by rank/shape mismatches that pass type\-domain and SSA\-scope checks but fail the verifier’s shape\-inference pass\.C4C\_\{4\}would condition the next operand’s tensor type on the partial program’s shape function \(declared in ODS viaInferShapedTypeOpInterface, extractable by the sametblgenpipeline asC2C\_\{2\}\); we have a sketch but not an implementation, and identifyC4C\_\{4\}as the most direct way to push the linalg ceiling above 80\.0%\.

Two smaller threads: \(i\) the in\-line coupled decoder hitmax\_tokenson every prompt in our pilot \(§[7](https://arxiv.org/html/2607.18254#S7)\), leaving the empirical\-decoder gap as future work for anyone aiming to remove the 5\-retry budget; \(ii\) extending the grammar to scf, affine, gpu, async, transform, tensor, vector is a few\-day derivation per dialect on the existing pipeline, not a research question\.

## 9Conclusion

On dialects whose verifier semantics are dominated by structural constraints, a schema\-derived three\-layer constraint stack lifts a 1\.7B\-parameter SLM to verify\-valid rates that match or exceed 15B/34B open\-weight code baselines onlinalg\(three\-seed mean 80\.0%,\+21\.3\+21\.3to\+44\.3\+44\.3pp over baselines with non\-overlapping CIs, surviving a same\-family fp16 precision control by 30 pp\) and on hand\-curated StableHLO\-Spec\-30 \(63\.3%,\+26\.6\+26\.6to\+30\.0\+30\.0pp over the 34B baselines, within CI of StarCoder2\-15B\)\. The StableHLO win is corpus\-conditional: the same baselines saturate at 98–100% on the templated parametric Held\-Out\-200 \(61\.5% SmolLM2\), so we retain the lead only on Spec\-30\. Onarith\+functhe result is parity\-to\-loss, which we scope as the boundary of training\-free constrained decoding rather than a uniformity claim\. The construction is mechanical: everyCiC\_\{i\}is derived from MLIR ODS through one tooling chain, so the procedure applies unchanged to any future dialect that ships the schema\. We release four NL→\\toMLIR benchmarks, the StableHLO\-Out\-Of\-Grammar\-25 stress set, and then=30n\{=\}30functional reference set under Apache\-2\.0 with Gebru datasheets, Croissant metadata, and a frozen reproducibility archive\.

## References

- \[1\]L\. B\. Allal, A\. Lozhkov, E\. Bakouch, G\. M\. Blakeney, H\. Zheng, G\. Penedo, L\. von Werra, H\. Kydlíček, N\. Bruggeman,et al\.\(2025\)SmolLM2: when smol goes big – data\-centric training of a small language model\.Note:Primary small\-model candidate in this paper: SmolLM2\-1\.7B\-Instruct\.External Links:2502\.02737Cited by:[NeurIPS Paper Checklist](https://arxiv.org/html/2607.18254#Ax2.I1.ix36.p1.1),[§1](https://arxiv.org/html/2607.18254#S1.p3.6),[§4\.1](https://arxiv.org/html/2607.18254#S4.SS1.p1.1)\.
- \[2\]J\. Austin, A\. Odena, M\. Nye, M\. Bosma, H\. Michalewski, D\. Dohan, E\. Jiang, C\. Cai, M\. Terry, Q\. Le, and C\. Sutton\(2021\)Program synthesis with large language models\.Note:MBPP benchmark for basic Python synthesis from natural\-language prompts\.External Links:2108\.07732Cited by:[§4\.2](https://arxiv.org/html/2607.18254#S4.SS2.p1.1)\.
- \[3\]F\. Cassano, J\. Gouwar, D\. Nguyen, S\. Nguyen, L\. Phipps\-Costin, D\. Pinckney, M\. Yee, Y\. Zi, C\. J\. Anderson, M\. Q\. Feldman,et al\.\(2023\)MultiPL\-E: a scalable and polyglot approach to benchmarking neural code generation\.IEEE Transactions on Software Engineering49\(7\),pp\. 3675–3691\.Note:MultiPL\-E; HumanEval and MBPP translated into additional programming languages, widely used as a polyglot code\-generation benchmark\.External Links:2208\.08227,[Link](https://arxiv.org/abs/2208.08227)Cited by:[§4\.2](https://arxiv.org/html/2607.18254#S4.SS2.p1.1)\.
- \[4\]M\. Chen, J\. Tworek, H\. Jun, Q\. Yuan, H\. P\. de Oliveira Pinto, J\. Kaplan, H\. Edwards, Y\. Burda, N\. Joseph, G\. Brockman,et al\.\(2021\)Evaluating large language models trained on code\.Note:HumanEval benchmark for NL\-to\-Python code generation\. Cited as a reference point in our discussion of benchmarks for code\-and\-IR generation\.External Links:2107\.03374Cited by:[§4\.2](https://arxiv.org/html/2607.18254#S4.SS2.p1.1)\.
- \[5\]\(2023\)Baldur: whole\-proof generation and repair with large language models\.InProceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering \(ESEC/FSE\),Note:Whole\-proof synthesis for Isabelle; cited as a representative LM\-for\-formal\-targets baseline outside the MLIR setting\.External Links:2303\.04910Cited by:[§2](https://arxiv.org/html/2607.18254#S2.SS0.SSS0.Px3.p1.1)\.
- \[6\]T\. Gebru, J\. Morgenstern, B\. Vecchione, J\. W\. Vaughan, H\. Wallach, H\. Daumé III, and K\. Crawford\(2021\)Datasheets for datasets\.Communications of the ACM64\(12\),pp\. 86–92\.Note:Template for dataset documentation\. Every benchmark released with this paper ships with a Datasheet following this template\.Cited by:[Appendix E](https://arxiv.org/html/2607.18254#A5.p1.1),[§1](https://arxiv.org/html/2607.18254#S1.p4.4)\.
- \[7\]D\. Hendrycks, S\. Basart, S\. Kadavath, M\. Mazeika, A\. Arora, E\. Guo, C\. Burns, S\. Puranik, H\. He, D\. Song, and J\. Steinhardt\(2021\)Measuring coding challenge competence with APPS\.InNeurIPS Datasets and Benchmarks Track,Note:APPS benchmark; 10,000 Python programming problems at varying difficulty levels\.External Links:2105\.09938,[Link](https://arxiv.org/abs/2105.09938)Cited by:[§4\.2](https://arxiv.org/html/2607.18254#S4.SS2.p1.1)\.
- \[8\]IREE Project\(2024\)IREE: an end\-to\-end MLIR\-based compiler and runtime framework\.Note:Source of the StableHLO verify gate \(iree\-compile \-\-iree\-input\-type=stablehlo \-\-compile\-to=input\)\.External Links:[Link](https://iree.dev/)Cited by:[Appendix C](https://arxiv.org/html/2607.18254#A3.p1.1),[§4\.2](https://arxiv.org/html/2607.18254#S4.SS2.p2.4),[§5](https://arxiv.org/html/2607.18254#S5.SS0.SSS0.Px3.p1.8)\.
- \[9\]C\. Lattner, M\. Amini, U\. Bondhugula, A\. Cohen, A\. Davis, J\. Pienaar, R\. Riddle, T\. Shpeisman, N\. Vasilache, and O\. Zinenko\(2020\)MLIR: A compiler infrastructure for the end of Moore’s Law\.External Links:2002\.11054,[Link](https://arxiv.org/abs/2002.11054)Cited by:[§1](https://arxiv.org/html/2607.18254#S1.p1.1)\.
- \[10\]L\. Li, S\. Rahili, and Y\. Zhao\(2025\)Correctness\-guaranteed code generation via constrained decoding\.InConference on Language Modeling \(COLM\),Note:Couples a context\-sensitive Tree of Parsers with token\-level decoding so generated programs are guaranteed parseable\. Related in spirit to our coupled\-decoder construction \(Appendix[A](https://arxiv.org/html/2607.18254#A1)\) but applied to general programming languages rather than schema\-derived MLIR dialects\.External Links:2508\.15866,[Link](https://arxiv.org/abs/2508.15866)Cited by:[§2](https://arxiv.org/html/2607.18254#S2.SS0.SSS0.Px2.p1.1)\.
- \[11\]Y\. Li, D\. Choi, J\. Chung, N\. Kushman, J\. Schrittwieser, R\. Leblond, T\. Eccles, J\. Keeling, F\. Gimeno, A\. Dal Lago,et al\.\(2022\)Competition\-level code generation with AlphaCode\.Science378\(6624\),pp\. 1092–1097\.Note:Introduces the CodeContests benchmark for competition\-level code generation\.External Links:2203\.07814,[Link](https://arxiv.org/abs/2203.07814)Cited by:[§4\.2](https://arxiv.org/html/2607.18254#S4.SS2.p1.1)\.
- \[12\]M\. Liu, N\. Pinckney, B\. Khailany, and H\. Ren\(2023\)VerilogEval: evaluating large language models for verilog code generation\.InIEEE/ACM International Conference on Computer\-Aided Design \(ICCAD\),Note:Verilog HDL evaluation benchmark; cited as a representative LM\-for\-formal\-targets baseline outside the MLIR setting\.External Links:2309\.07544Cited by:[§2](https://arxiv.org/html/2607.18254#S2.SS0.SSS0.Px3.p1.1)\.
- \[13\]A\. Lozhkov, R\. Li, L\. B\. Allal, F\. Cassano, J\. Lamy\-Poirier, N\. Tazi, A\. Tang, D\. Pykhtar, J\. Liu, Y\. Wei,et al\.\(2024\)StarCoder 2 and the stack v2: the next generation\.Note:Baseline model in our experiments: StarCoder2\-15B:instruct under Q4\_K\_M quantization; the most recent 15B open\-weight code model in our matrix\.External Links:2402\.19173Cited by:[NeurIPS Paper Checklist](https://arxiv.org/html/2607.18254#Ax2.I1.ix36.p1.1),[§1](https://arxiv.org/html/2607.18254#S1.p3.6),[§4\.1](https://arxiv.org/html/2607.18254#S4.SS1.p1.1)\.
- \[14\]M\. Mishra, M\. Stallone, G\. Zhang, Y\. Shen, A\. Prasad, A\. M\. Soria, M\. Merler, P\. Selvam, S\. Surendran, S\. Singh,et al\.\(2024\)Granite code models: a family of open foundation models for code intelligence\.Note:Baseline model in our experiments: Granite\-Code\-34B\-Instruct under Q4\_K\_M quantization\.External Links:2405\.04324Cited by:[NeurIPS Paper Checklist](https://arxiv.org/html/2607.18254#Ax2.I1.ix36.p1.1),[§1](https://arxiv.org/html/2607.18254#S1.p3.6),[§4\.1](https://arxiv.org/html/2607.18254#S4.SS1.p1.1)\.
- \[15\]MLCommons Croissant Working Group\(2024\)Croissant: a metadata format for ML\-ready datasets \(v1\.0\)\.Note:Core fields plus Responsible\-AI extensions \(rai:dataBiases,rai:dataLimitations, provenance\); used for per\-benchmark metadata records in this paper\.External Links:[Link](https://mlcommons.org/croissant/)Cited by:[Appendix E](https://arxiv.org/html/2607.18254#A5.SS0.SSS0.Px7.p1.1),[§1](https://arxiv.org/html/2607.18254#S1.p4.4)\.
- \[16\]N\. Mündler, I\. Tymchenko, Y\. He, M\. N\. Mueller, and M\. Vechev\(2025\)Type\-constrained code generation with language models\.InProceedings of the ACM on Programming Languages \(PLDI\),Note:Integrates a static type\-checker into per\-step constrained decoding for statically\-typed languages; demonstrates large reductions in type\-error rate on 1B\-scale models\. Our C3 coupled state machine is the same class of idea applied to MLIR’s SSA\-scope rules instead of a general\-purpose language type system\.External Links:2504\.09246Cited by:[§2](https://arxiv.org/html/2607.18254#S2.SS0.SSS0.Px2.p1.1)\.
- \[17\]OpenXLA Project\(2024\)StableHLO: A portable operation set for ML models\.Note:Dialect specification used for the cross\-dialect generalization experiments\. Benchmark programs for §[5](https://arxiv.org/html/2607.18254#S5)were verified with iree\-compile –compile\-to=input\.External Links:[Link](https://openxla.org/stablehlo)Cited by:[§4\.2](https://arxiv.org/html/2607.18254#S4.SS2.p2.4),[§5](https://arxiv.org/html/2607.18254#S5.SS0.SSS0.Px3.p1.8)\.
- \[18\]K\. Park, J\. Wang, T\. Berg\-Kirkpatrick, N\. Polikarpova, and L\. D’Antoni\(2024\)Grammar\-aligned decoding\.Note:Identifies the sampling\-distribution drift under naive token\-level masking\. We cite their formal framing; our work differs in that the CFG is mechanically derived from ODS rather than hand\-written\.External Links:2405\.21047,[Link](https://arxiv.org/abs/2405.21047)Cited by:[§2](https://arxiv.org/html/2607.18254#S2.SS0.SSS0.Px1.p1.1)\.
- \[19\]G\. Poesia, A\. Polozov, V\. Le, A\. Tiwari, G\. Soares, C\. Meek, and S\. Gulwani\(2022\)Synchromesh: reliable code generation from pre\-trained language models\.InInternational Conference on Learning Representations \(ICLR\),Note:Constrained Semantic Decoding \(CSD\) framework: per\-step token\-mask construction using target\-language static analyzers for SQL and Python synthesis\. Closest prior work on context\-sensitive constrained decoding for formal targets\.External Links:2201\.11227Cited by:[§2](https://arxiv.org/html/2607.18254#S2.SS0.SSS0.Px2.p1.1)\.
- \[20\]B\. Rozière, J\. Gehring, F\. Gloeckle, S\. Sootla, I\. Gat, X\. E\. Tan, Y\. Adi, J\. Liu, R\. Sauvestre, T\. Remez,et al\.\(2023\)Code Llama: open foundation models for code\.Note:Baseline model in our experiments: CodeLlama\-34B\-Instruct under Q4\_K\_M quantization\.External Links:2308\.12950Cited by:[NeurIPS Paper Checklist](https://arxiv.org/html/2607.18254#Ax2.I1.ix36.p1.1),[§1](https://arxiv.org/html/2607.18254#S1.p3.6),[§4\.1](https://arxiv.org/html/2607.18254#S4.SS1.p1.1)\.
- \[21\]M\. Schall and G\. de Melo\(2025\)The hidden cost of structure: how constrained decoding affects language model performance\.InProceedings of the 15th International Conference on Recent Advances in Natural Language Processing — Natural Language Processing in the Generative AI Era \(RANLP\),G\. Angelova, M\. Kunilovskaya, M\. Escribe, and R\. Mitkov \(Eds\.\),Varna, Bulgaria,pp\. 1074–1084\.Note:Observes that constrained decoding can degrade small\-model pass\-rate; we replicate in a controlled setting and show it does not reproduce under 3\-shot priming with a type\-domain\-aware grammar\.External Links:[Link](https://aclanthology.org/2025.ranlp-1.124/)Cited by:[§2](https://arxiv.org/html/2607.18254#S2.SS0.SSS0.Px1.p1.1)\.
- \[22\]B\. T\. Willard and R\. Louf\(2023\)Efficient guided generation for large language models\.Note:Basis for the Outlines CFG\-guided decoding library used as one of our C1 backends\.External Links:2307\.09702,[Link](https://arxiv.org/abs/2307.09702)Cited by:[§2](https://arxiv.org/html/2607.18254#S2.SS0.SSS0.Px1.p1.1),[§3](https://arxiv.org/html/2607.18254#S3.SS0.SSS0.Px3.p1.2),[§4\.1](https://arxiv.org/html/2607.18254#S4.SS1.p1.1)\.
- \[23\]K\. Yang, A\. M\. Swope, A\. Gu, R\. Chalamala, P\. Song, S\. Yu, S\. Godil, R\. Prenger, and A\. Anandkumar\(2023\)LeanDojo: theorem proving with retrieval\-augmented language models\.InAdvances in Neural Information Processing Systems Datasets and Benchmarks Track \(NeurIPS D&B\),Note:Lean tactic generation; cited as a representative SLM\-for\-formal\-targets baseline outside the MLIR setting\.External Links:2306\.15626Cited by:[§2](https://arxiv.org/html/2607.18254#S2.SS0.SSS0.Px3.p1.1)\.

## Appendix

## Appendix ASoundness and coverage of the coupled decoder

We formalize the two key properties of the in\-line C3 coupled decoder \(§[3](https://arxiv.org/html/2607.18254#S3)\): \(i\) every generation it accepts passes the post\-hoc scope validator, and \(ii\) every generation passing the scope validator is reachable by some token\-oracle trajectory\.

### Definitions

Let𝒢\\mathcal\{G\}denote the LALR\-compiled generation grammar over terminal alphabetΣ\\Sigma, and letTTdenote the set of terminals partitioned into literal and regex\-matched classes\. LetVVdenote the BPE token vocabulary of the language model\. Each decode step producesv∈Vv\\in V;text​\(v\)\\mathrm\{text\}\(v\)denotes the vocab string\.

A*decoder state*σ=\(q,Λ,ϕ,p\)\\sigma=\(q,\\Lambda,\\phi,p\)is a tuple of:

- •qq: an LALR interactive\-parser state \(position in𝒢\\mathcal\{G\}’s item\-set lattice\)\.
- •Λ\\Lambda: a symbol table mapping SSA names to type stubs\.
- •ϕ∈Φ=\{Outer, Param, FuncBody, OpStart, AfterEq, RetVal, Closed\}\\phi\\in\\Phi=\\\{\\textsc\{Outer, Param, FuncBody, OpStart, AfterEq, RetVal, Closed\}\\\}: an op\-phase marker\.
- •p∈Σ∗p\\in\\Sigma^\{\*\}: the accumulated partial text since the last closed terminal\.

The decoder’s token\-level mask at stateσ\\sigmais

mask​\(σ\)=⋃t∈legal​\(q\)prefix​\(t,p\)∩scope​\(t,ϕ,Λ\)\\mathrm\{mask\}\(\\sigma\)=\\bigcup\_\{t\\in\\mathrm\{legal\}\(q\)\}\\mathrm\{prefix\}\(t,p\)\\cap\\mathrm\{scope\}\(t,\\phi,\\Lambda\)wherelegal​\(q\)\\mathrm\{legal\}\(q\)enumerates shift\-legal terminals at parser stateqq,prefix​\(t,p\)\\mathrm\{prefix\}\(t,p\)is the set ofv∈Vv\\in Vwhose text extendspptoward a valid completion of terminaltt, andscope​\(t,ϕ,Λ\)\\mathrm\{scope\}\(t,\\phi,\\Lambda\)narrows the set for SSA\-typed terminals based on the scope predicate:

scope​\(t,ϕ,Λ\)=\{Vt∉\{SSA\}prefix​\(Λ,p\)t=SSA,ϕ∈\{AfterEq, RetVal\}prefix​\(ΣSSA,p\)∖prefix​\(Λ,p\)t=SSA,ϕ∈\{Param, OpStart\}Votherwise\.\\mathrm\{scope\}\(t,\\phi,\\Lambda\)=\\begin\{cases\}V&t\\not\\in\\\{\\mathrm\{SSA\}\\\}\\\\ \\mathrm\{prefix\}\(\\Lambda,p\)&t=\\mathrm\{SSA\},\\phi\\in\\\{\\textsc\{AfterEq, RetVal\}\\\}\\\\ \\mathrm\{prefix\}\(\\Sigma\_\{\\mathrm\{SSA\}\},p\)\\setminus\\mathrm\{prefix\}\(\\Lambda,p\)&t=\\mathrm\{SSA\},\\phi\\in\\\{\\textsc\{Param, OpStart\}\\\}\\\\ V&\\text\{otherwise\.\}\\end\{cases\}ΣSSA\\Sigma\_\{\\mathrm\{SSA\}\}denotes the SSA regex character class\.

State transitionsσ→𝑣σ′\\sigma\\xrightarrow\{v\}\\sigma^\{\\prime\}are defined operationally: appendtext​\(v\)\\mathrm\{text\}\(v\)topp; greedily close zero or more terminals whose regex fullmatches the accumulatedpp; each closure advances the LALR state, possibly updatesΛ\\Lambda\(on DEF\) or checksΛ\\Lambda\(on USE\), and transitionsϕ\\phiper the phase table\.

### Theorem 1 \(Soundness\)

If the decoder reaches a final stateσf=\(qf,Λf,ϕf,pf\)\\sigma\_\{f\}=\(q\_\{f\},\\Lambda\_\{f\},\\phi\_\{f\},p\_\{f\}\)withqfq\_\{f\}an accept state andpf=εp\_\{f\}=\\varepsilon, then the emitted stringsssatisfies:

1. 1\.ssparses under𝒢\\mathcal\{G\}\(and therefore undermlir\.lark\\mathrm\{mlir\.lark\}, since𝒢\\mathcal\{G\}is a subset by grammar inclusion\)\.
2. 2\.The post\-hoc validatorc3\_scope\.validate\(s\)returns accept\.

#### Proof sketch\.

\(i\) follows from LALR closure: the interactive parser guaranteesqfq\_\{f\}accepts iff the consumed terminal sequence is a𝒢\\mathcal\{G\}\-derivation ofss, and the reduce actions thatqfq\_\{f\}must have taken are exactly the leftmost derivation steps\.

\(ii\) The symbol\-tableΛ\\Lambdais updated monotonically at each SSA DEF \(onϕ∈\{Param, OpStart∪AfterEq\-transition\}\\phi\\in\\\{\\textsc\{Param, OpStart\}\\cup\\textsc\{AfterEq\-transition\}\\\}\) and checked at each SSA USE \(ϕ∈\{AfterEq, RetVal\}\\phi\\in\\\{\\textsc\{AfterEq, RetVal\}\\\}\)\. Because the maskscope​\(SSA,ϕ,Λ\)\\mathrm\{scope\}\(\\mathrm\{SSA\},\\phi,\\Lambda\)restricts USE tokens toprefix​\(Λ,p\)\\mathrm\{prefix\}\(\\Lambda,p\), any USE that closes does so with a name inΛ\\Lambda\. Thereforesshas no out\-of\-scope SSA references: every use is matched by a prior definition in the same function\. This is the definition ofc3\_scopeaccept\.□\\square

### Theorem 2 \(Coverage, BPE\-refined\)

For any MLIR fragments∗s^\{\*\}that parses under𝒢\\mathcal\{G\}*and*passesc3\_scope\.validate, there exists an oracle token sequence\(v1,…,vn\)∈Vn\(v\_\{1\},\\ldots,v\_\{n\}\)\\in V^\{n\}such that the decoder state machine reaches a final accept state with emitted strings∗s^\{\*\}\.

We strengthen the earlier proof by handling BPE\-boundary misalignment explicitly\. The subtlety is that the BPE tokenization ofs∗s^\{\*\}taken as a whole need not respect terminal boundaries — a single token may decode to text spanning two terminals \(e\.g\. “module” in the SmolLM2 vocabulary carries MODULE plus a trailing WS\), and the per\-terminal tokenization of a substring may not be a subsequence of the whole\-string BPE\.

#### Proof\.

We construct an oracle trajectory character\-by\- character and then show it factors into at least one BPE tokenization compatible with the vocab\.

Lets∗=c1​c2​⋯​cNs^\{\*\}=c\_\{1\}c\_\{2\}\\cdots c\_\{N\}\(over the character alphabet\) and let\(t1,…,tm\)\(t\_\{1\},\\ldots,t\_\{m\}\)be the leftmost LALR\-derivation terminals with textwiw\_\{i\}, so thats∗=w1​w2​⋯​wms^\{\*\}=w\_\{1\}w\_\{2\}\\cdots w\_\{m\}\. Define the*character oracle*as a sequence of single\-character vocab tokens\. Our vocabularyVVcovers all printable ASCII characters individually \(this is true for all BPE tokenizers considered in §[4](https://arxiv.org/html/2607.18254#S4)— a standard property\)\. Feedingc1,…,cNc\_\{1\},\\ldots,c\_\{N\}through the decoder advancesppone character at a time; at each character boundary, the close\-terminals procedure commits a terminal iff the accumulatedppis a maximal match for some legal terminal\. Because the LALR derivation is unambiguous over𝒢\\mathcal\{G\}, the closures fire exactly at the boundaries betweenwiw\_\{i\}andwi\+1w\_\{i\+1\}, so the decoder advances the parser state in lockstep with the leftmost derivation\. At each SSA USE step, the scope\-predicatescope​\(SSA,ϕ,Λ\)\\mathrm\{scope\}\(\\mathrm\{SSA\},\\phi,\\Lambda\)requires the next token’s text to start some name inΛ\\Lambda; becauses∗s^\{\*\}passesc3\_scope, that name is present by construction, and the single\-character tokenccat the start of a SSA\-USE terminal is a prefix of some name inΛ\\Lambda\. Therefore the character oracle reaches an accept state\.

To lift this to the whole\-string BPE setting, observe that if the character oracle is accepted, any*coarser*tokenization — i\.e\., a tokenization where some consecutive characters are merged into a multi\-character tokenvvsuch thattext​\(v\)=ci​ci\+1​⋯​cj\\mathrm\{text\}\(v\)=c\_\{i\}c\_\{i\+1\}\\cdots c\_\{j\}andv∈Vv\\in V— is also accepted,*provided*the decoder’s per\-step mask admitsvvas a legal next token at the corresponding state\. The multi\-character case is handled by “carry\-over”: the decoder’s close\-terminals loop consumes complete terminals from the start ofppand preserves leftover text as the newpp, so a token whose text spans two terminals \(saywi​wi\+1′w\_\{i\}w\_\{i\+1\}^\{\\prime\}withwi\+1′w\_\{i\+1\}^\{\\prime\}a prefix ofwi\+1w\_\{i\+1\}\) results inwiw\_\{i\}being closed andwi\+1′w\_\{i\+1\}^\{\\prime\}remaining as the leftoverpp\. The per\-step mask under the resulting post\-close state must admit tokens that extendpptowardwi\+1w\_\{i\+1\}; this is guaranteed by the two\-component mask construction \(§[3](https://arxiv.org/html/2607.18254#S3)and the earliermask​\(σ\)\\mathrm\{mask\}\(\\sigma\)definition in this appendix\), which unions \(a\)prefix​\(t′,p\)\\mathrm\{prefix\}\(t^\{\\prime\},p\)for each legalt′t^\{\\prime\}under the post\-close state and \(b\) the*lookahead*contribution: ifppcompletely matches some post\-close legal terminal, the mask also includesprefix​\(t′′,ε\)\\mathrm\{prefix\}\(t^\{\\prime\\prime\},\\varepsilon\)fort′′t^\{\\prime\\prime\}legal in the*next*state\. Therefore any whole\-string tokenization ofs∗s^\{\*\}that is factorizable into vocab tokens is a valid oracle\.□\\square

#### On the “vocab\-covers\-ASCII” assumption\.

All tokenizers used in the paper \(SmolLM2/Phi family, StarCoder2, CodeLlama, Granite\) include single\-character tokens for every printable ASCII character in their vocabularies\. If a tokenizer*did not*include some single characterccused by𝒢\\mathcal\{G\}’s terminal alphabet, the character\-oracle step of the proof would fail and coverage would be subject to tokenizer\-specific conditions\. We do not observe this failure mode in practice; the lemma as stated suffices for all configurations reported in §[5](https://arxiv.org/html/2607.18254#S5)\.

### Theorem 3 \(Equivalence to post\-hoc rejection sampling\)

LetDinD\_\{\\mathrm\{in\}\}be the in\-line coupled decoder andDpostD\_\{\\mathrm\{post\}\}be the post\-hoc rejection\-sampled decoder \(generate under C1\+C2 freely; accept iff parse \+c3\_scope\.validate\)\. Both decoders induce the same set of*acceptable*output strings:

Accept​\(Din\)=Accept​\(Dpost\)\.\\mathrm\{Accept\}\(D\_\{\\mathrm\{in\}\}\)=\\mathrm\{Accept\}\(D\_\{\\mathrm\{post\}\}\)\.
#### Proof sketch\.

Forward inclusion is Theorem 1\. Reverse inclusion is Theorem 2: everys∗s^\{\*\}accepted byDpostD\_\{\\mathrm\{post\}\}is reachable byDinD\_\{\\mathrm\{in\}\}via the oracle trajectory built from the BPE tokenization ofs∗s^\{\*\}, sos∗∈Accept​\(Din\)s^\{\*\}\\in\\mathrm\{Accept\}\(D\_\{\\mathrm\{in\}\}\)\.□\\square

### Remark: efficiency

Soundness \+ coverage ensure correctness parity, but the decoders differ in sampling efficiency:DinD\_\{\\mathrm\{in\}\}achieves 1 sample per output, whileDpostD\_\{\\mathrm\{post\}\}requires an expected1/Pr​\[accept\]1/\\mathrm\{Pr\}\[\\text\{accept\}\]samples\. Onarith\+funcwith SmolLM2 and a 5\-retry budget, the observed mean attempts forDpostD\_\{\\mathrm\{post\}\}is 1\.83 \(Day 5\); the in\-line decoder reduces this to 1\.0 deterministically\. The theorems above do not bound sampling quality \(temperature, mode collapse\), only the reachable support\.

### Remark: the “zero\-false\-reject” property of C3 is distribution\-specific

The C3 confusion matrix \(Fig\.[1](https://arxiv.org/html/2607.18254#S3.F1)\) reports zero cases wherec3\_scoperejects butmlir\-optaccepts*on the SmolLM2 output distribution*\. This is a stronger operational property than Theorem 1 \(which is stated in terms ofc3\_scopeagreement\): it says the post\-hoc filter refines the set of accepted strings without introducing false rejections relative to the downstreammlir\-optverifier on the programs SmolLM2 tends to emit\.

However, the zero\-false\-reject property does*not*generalize uniformly across generators\. On CodeLlama\-34B \(§[5](https://arxiv.org/html/2607.18254#S5)\), C1\+C3*drops*verify\-pass by−22\.2\-22\.2pp relative to C1 alone in the apples\-to\-apples ladder \(Table[3](https://arxiv.org/html/2607.18254#S5.T3)\)\. Since C3 is a strict additional rejection gate, a drop can only arise if C3 rejects programs thatmlir\-optwould accept\. In other words: CodeLlama’s output distribution contains programs with SSA naming patterns thatc3\_scope’s heuristics \(name\-recognition via regex, definition\-site bookkeeping\) reject but thatmlir\-optaccepts as well\-formed MLIR\. Inspection of the first 10 such CodeLlama rejects shows two recurring patterns: \(i\) SSA names introduced by operations our tracker does not recognize as DEF\-sites \(e\.g\., block arguments of a nestedscf\.if\), and \(ii\) numeric SSA names like%0used across redefinitions thatmlir\-optaccepts within block scope but C3 flags as redefinition\.

This is a real limitation, not an error in the theorems\. Theorem 1 establishes agreement between the in\-line decoder and thec3\_scopepost\-hoc filter\. The operational guarantee of “zero false rejects againstmlir\-opt” is an additional empirical claim that holds on the distributions we measured \(SmolLM2 at 1\.7B\) but not universally\. We therefore state this in the paper as: “c3\_scopehas zero false rejects againstmlir\-opton SmolLM2 outputs; on 34B models with different output distributions, the false\-reject rate becomes non\-zero, visible in the−22\.2\-22\.2pp CodeLlama C3 drop \(§[5](https://arxiv.org/html/2607.18254#S5)\)\.” Reducing the false\-reject rate for larger models is future work; our contribution stands on the pairing \{1\.7B SLM \+ C3\}≥\\geq\{34B baseline\}, which holds regardless of whether 34B models see a C3 false\-reject penalty\.

### Empirical gap of the in\-line construction

We implement the in\-line decoder with 82 unit tests and end\-to\-end parse\-valid MLIR on a canonical prompt, and release it alongside the rejection sampler\. On a pairedn=10n\{=\}10test against rejection sampling, the greedy in\-line variant reaches parse\-valid on only 20% of prompts and runs roughly44×44\\timesslower per generation; the remaining 80% of runs hitmax\_tokensbefore the grammar reaches its accept state\. Temperature\-annealed retries did not close the gap\. The gap is a sampling\-coverage issue rather than a soundness issue: accepted strings remain a subset of those admitted by post\-hoc rejection sampling, consistent with Theorem 3\.

#### Diagnosis\.

The per\-step mask is the intersection of C1’s shift\-legal terminals and C3’s in\-scope name trie, which has nonzero probability of becoming empty after a long prefix has committed to a partial BPE token that no in\-scope name can complete\. In those states the decoder is forced into low\-probability tail tokens to recover, and the resulting sequences exceedmax\_tokensbefore reaching an accept state\. A future variant that backtracks past the BPE\-boundary commit point rather than sampling forward from it would close the gap; we leave this to future work and report all empirical results from the post\-hoc form\.

## Appendix BReproducibility, Datasheet, and Responsible Release

#### Artifacts\.

The reproducibility archive \(submission\_artifact\.tar\.gz; built from the public repository at[https://github\.com/plawanrath/slm\-to\-mlir\-constrained\-emitter](https://github.com/plawanrath/slm-to-mlir-constrained-emitter); benchmarks mirrored as HuggingFace Datasets under theplawanrathnamespace\) contains: \(i\) the four primary benchmarks plus the StableHLO\-Out\-Of\-Grammar\-25 stress set, totaling 435 instances \(150\+30\+30\+200\+25150\+30\+30\+200\+25\), and the hand\-authored functional reference set ateval/functional/references\.json\(n=30n\{=\}30, 10 prompts per dialect; released as an evaluation artifact for bounding the verify\-valid→\\tofunctional gap, not as a training or fine\-tuning set\); \(ii\) the constrained\-decoder source with frozenrequirements\.lock\.txt; \(iii\) the verifier wrappers \(verify\_mlir\.py,verify\_stablehlo\.py\); \(iv\) seed\-locked random\-state files and bootstrap scripts that regenerate every figure and table from raw per\-prompt\.jsonlrows; \(v\) per\-benchmark Croissant records ateval/benchmarks/<name\>/croissant\.jsonand a single Gebru\-style datasheet atdocs/datasheets/datasheet\.md\. License is Apache\-2\.0 \(SPDX: Apache\-2\.0\) for both code and data\. The release is intentionally test\-only: we explicitly disallow use as fine\-tuning material to prevent benchmark contamination; this restriction is recorded both in the datasheet’s “uses not supported” field and in the Croissantrai:dataLimitationsfield per benchmark\.

#### Hosted benchmark URLs\.

#### Reproducibility pins\.

All numbers are pinned to LLVMllvmorg\-19\.1\.7and iree\-compiler 20241104\.1068; both pins live inscripts/env/requirements\.lock\.txtalong with every other host\-side dependency at exact versions\. The paired bootstrap \(10,000 resamples, 95% percentile CI\) is deterministic undernumpy\.random\.default\_rng\(0\); runningpython scripts/make\_paper\_figures\_final\.pyfrom the archive reproduces every figure byte\-identically given the same input\.jsonl\. One verifier gotcha worth flagging up\-front:iree\-compile \-\-compile\-to=inputaccepts empty stdin as a valid emptymodule \{\}and returns success, which means a constrained decoder that emits the empty string is silently scored as verify\-valid\. Our wrapperscripts/env/verify\_stablehlo\.pyrequires afunc\.func @substring in the input before invokingiree\-compile\. We recommend any reuser of the StableHLO benchmarks apply the same guard\. The verifier\-tool substitution itself is independently validated:iree\-compile \-\-compile\-to=inputand upstreamstablehlo\-opt v1\.4\.0agree on 50/50 instances on a stratifiedn=50n\{=\}50sample across six op families \(build commands and per\-instance log in Appendix[C](https://arxiv.org/html/2607.18254#A3)\), so reusers comparing against an in\-treestablehlo\-optenvironment should not see material drift\.

#### Datasheet summary\.

Each instance is a \(natural\-language description, reference MLIR program, dialect, difficulty tag, source provenance\) tuple\. All reference MLIR programs are verifier\-clean at release time\. Spec\-\* benchmarks were author\-curated against public ODS specs and filtered through the verifier; Held\-Out\-200 was generated by a parametric sweep \(585 raw candidates to 200 verifier\-clean kept, sweeping 7 op families×\\times6 dtypes×\\times3 shape ranks\); Out\-Of\-Grammar\-25 was hand\-authored against StableHLO ops the grammar does not cover\. There is no human\-subject data, no PII, no crowdsourced labor, no offensive content; the data domain is technical MLIR code and English descriptions of numerical operations\. The datasheet \(§[E](https://arxiv.org/html/2607.18254#A5)\) covers every Gebru\-template field including the explicit “uses the dataset does not support” \(fine\-tuning and functional\-correctness testing\) for reuser clarity\. Splits: not pre\-split\. All instances are released as a test set; users running methods that require a training set are expected to hold programs out themselves\.

#### Role of the verify\-valid metric\.

We adopt verify\-valid pass rate as the primary metric for three reasons\. First, it is mechanical: no human judgment is required, so the benchmarks are reproducible without grader drift\. Second, it is well\-defined per dialect and each MLIR dialect ships its own verifier in\-tree, so the metric extends to any future dialect with no methodological redesign\. Third, it is a necessary condition for downstream usefulness: a program that fails the verifier cannot be lowered, optimized, or executed regardless of any other property\. We deliberately do not adopt soft or token\-level metrics \(BLEU, exact\-match\) because they conflate stylistic differences with semantic ones in the IR setting, where two textually different programs can be equivalent \(e\.g\., differing only in SSA\-name choice\) and two textually similar programs can differ in verify status \(e\.g\., a single mismatched dtype\)\.

#### Ethical considerations\.

The benchmark task is technical IR generation; we do not see direct dual\-use risk from a verify\-valid evaluation\. Two indirect considerations are worth recording\. \(i\) The pretraining corpora of all evaluated models \(SmolLM2, CodeLlama, Granite\-Code, StarCoder2\) include substantial open\-source code, and there is no auditable line between “MLIR seen during pretraining” and “verify\-valid\-cleared MLIR generated at inference”; reviewers should read absolute verify rates as artifacts of the pretraining\-plus\- constraint\-stack composition rather than as model\-intrinsic capability measurements\. \(ii\) We evaluate only limited open\-weight models\. We disclose this as a deliberate scope\-of\-evaluation rather than an ethical claim about the excluded families; a future replication that includes them requires no methodological change, only additional compute\.

## Appendix CStableHLO toolchain and verifier substitution

The canonical structural verifier for StableHLO isstablehlo\-optfrom the in\-treeopenxla/stablehlorepository\. We useiree\-compile \-\-iree\-input\-type=stablehlo \-\-compile\-to=input\[[8](https://arxiv.org/html/2607.18254#bib.bib5)\]as the verifier in our pipeline; it runs StableHLO’s in\-tree verification \(the samemlir::stablehlo::registerAllDialectsandverify\(\)machinerystablehlo\-optinvokes\) as the first stage of the IREE compile pipeline and exits before any lowering\. We useiree\-compilerather thanstablehlo\-optthroughout the body of the paper because the vendoredmlir\-optin our reproducibility container does not ship the StableHLO dialect\.

#### Verifier\-tool concordance \(n=50n\{=\}50\)\.

To validate the substitution against the canonical verifier quantitatively, we builtstablehlo\-opt v1\.4\.0from source against our reproducibility container’s LLVM 19\.1\.7 \(openxla/stablehloHEAD requires a more recent LLVM than our pin; v1\.4\.0 at LLVM SHA9ddfe62f5c11configures cleanly and builds in∼\\sim3 min via Ninja\) and ran both verifiers on a stratifiedn=50n\{=\}50sample drawn fromStableHLO\-Held\-Out\-200∪\\cupStableHLO\-Spec\-30, covering six op families \(elementwise\-binary 26, transpose 6, dot\_general 4, broadcast 3, reshape 3, other 8\)\.Result: 50/50 concordant accepts, 0/50iree\-compile\-accepts\-stablehlo\-opt\-rejects, 0/50 reverse direction\.The substitution is empirically sound on the released benchmarks\. Build commands and the per\-instance log are inscripts/verify\_concordance\.pyandresults/day51/verify\_concordance\_n50\.json\.

#### Build recipe \(for reviewers reproducing the canonical verifier locally\)\.

gitclonehttps://github\.com/openxla/stablehlo\.git&&cdstablehlo

gitsubmoduleupdate\-\-init\-\-recursive

\#pinLLVMrevisiontestedbyopenxla/stablehloCI:

LLVM\_COMMIT=$\(catbuild\_tools/llvm\_version\.txt\)

cmake\-GNinja\-Bbuild\-DCMAKE\_BUILD\_TYPE=Release\\

\-DLLVM\_TARGETS\_TO\_BUILD="X86;ARM"\\

\-DLLVM\_EXTERNAL\_PROJECTS=stablehlo\\

\-DLLVM\_EXTERNAL\_STABLEHLO\_SOURCE\_DIR=$PWD

ninja\-Cbuildstablehlo\-opt

Once built,stablehlo\-opt \-\-verify\-diagnostics input\.mliris a drop\-in replacement for the IREE wrapper\.

#### Grammar tooling caveats for reusers\.

Two reuser\-facing caveats are worth recording, because the same setup will reproduce both\. First, four StableHLO grammar productions \(op\_transpose,op\_broadcast\_in\_dim,op\_reshape,op\_dot\_general\) must avoid\\\-line\-continuation tokens for splitting long rules across source lines\. LARK parses these correctly, but the llguidance backend used by Outlines does not: it raises a silentLLMatcherlexer error and emits zero tokens, producing 100% empty\-string generations\. The released grammars use single\-line productions; any reuser editing the grammars should verify that their lark\-parser and outlines\+llguidance versions agree on every multi\-line rule before reporting verify rates\. Second,iree\-compile \-\-iree\-input\-type=stablehlo \-\-compile\-to=inputaccepts empty stdin and returns success with stdoutmodule \{\}\. This is a property ofiree\-compile’s input handling, not a bug in our code, but it interacts catastrophically with the first caveat: a constrained decoder that produces empty output is silently scored as verify\-valid\. Symptom: a “100% verify\-valid” reading that is in fact “100% empty\-string accepted as empty module\.” Fix: our wrapperscripts/env/verify\_stablehlo\.pyrequires afunc\.func @substring in the input before invokingiree\-compile; empty ormodule \{\}\-only inputs return a non\-success error code\. We recommend any reuser of the StableHLO benchmarks adopt the same guard regardless of whether they use Outlines\.

## Appendix DExtended figures and tables

This appendix provides extended quantitative results referenced from the main text: the headline cross\-dialect comparison \(Fig\.[3](https://arxiv.org/html/2607.18254#A4.F3)\), the efficiency frontier \(Fig\.[4](https://arxiv.org/html/2607.18254#A4.F4)\), the seed\-0 ladder run with 95% bootstrap CIs \(Table[2](https://arxiv.org/html/2607.18254#S5.T2)\), apples\-to\-apples paired comparisons \(Fig\.[5](https://arxiv.org/html/2607.18254#A4.F5)\), per\-dialect error\-category progression \(Fig\.[6](https://arxiv.org/html/2607.18254#A4.F6), Table[6](https://arxiv.org/html/2607.18254#A4.T6)\), paired\-bootstrap deltas \(Fig\.[7](https://arxiv.org/html/2607.18254#A4.F7)\), the HCS replication \(Fig\.[8](https://arxiv.org/html/2607.18254#A4.F8)\), the per\-op residual\-error breakdown \(Fig\.[9](https://arxiv.org/html/2607.18254#A4.F9)\), three\-seed uniform\-nnverify rates \(Table[7](https://arxiv.org/html/2607.18254#A4.T7)\), the empirical\-claims summary \(Table[8](https://arxiv.org/html/2607.18254#A4.T8)\), and a numerical\-consistency note reconciling the seed\-0 ladder with the three\-seed protocol\.

![Refer to caption](https://arxiv.org/html/2607.18254v1/x3.png)Figure 3:Headline:mlir\-opt/iree\-compileverify\-valid rates on the two dialects where we report a win \(linalg, StableHLO\)\. SmolLM2\-1\.7B \+C1C\_\{1\}\+C2C\_\{2\}\+C3C\_\{3\}attains a higher rate than each 15B/34B baseline under the same 5\-retry rejection budget\. Linalg bars are three\-seed means at uniformn=125n\{=\}125with across\-seed range whiskers; the SmolLM2 cell is 80\.0% \(range 0pp\)\. The StableHLO panel is corpus\-conditional and reports the seed\-0*Spec\-30*corpus \(n=30n\{=\}30\); the larger*Held\-Out\-200*corpus saturates the 15B/34B baselines \(verify rate≈\\approx1\.0\) and is therefore reported in a separate table rather than in the headline\.arith\+funcis intentionally omitted here and reported in Table[7](https://arxiv.org/html/2607.18254#A4.T7)as a non\-win cell \(three\-seed mean 53\.2%±\\pm1\.8pp for SmolLM2 \+C1C\_\{1\}\+C2C\_\{2\}\+C3C\_\{3\}\); “verify\-valid” is a structural property, not functional correctness \(§[7](https://arxiv.org/html/2607.18254#S7)\)\.![Refer to caption](https://arxiv.org/html/2607.18254v1/x4.png)Figure 4:Efficiency frontier: wall\-clock per generation \(log scale\) vs verify\-valid rate \(three\-seed mean at uniformnn\)\. Five systems×\\timestwo dialects, including a Granite\-Code\-8B\-fp16 same\-family precision control\. The SmolLM2 \+C1C\_\{1\}\+C2C\_\{2\}\+C3C\_\{3\}linalgpoint sits at 1\.86 s / 80\.0% \(top\-left, ours\) and thearith\+funcpoint at 1\.65 s / 53\.2%; onlinalgthe SmolLM2 cell is Pareto\-dominant by both axes against every other cell\. The 15B/34B Q4\_K\_M baselines run 6–24×\\timesslower per generation; the Granite\-Code\-8B\-fp16 control runs 7×\\timesslower onarith\+funcand 25×\\timesslower onlinalg\. Color = system, marker = dialect \(circles = arith\+func, squares = linalg\)\.![Refer to caption](https://arxiv.org/html/2607.18254v1/x5.png)Figure 5:Apples\-to\-applesC3C\_\{3\}comparison, three\-seed mean at uniformnnwith across\-seed half\-range whiskers\. Five systems×\\timestwo dialects, including a Granite\-Code\-8B\-fp16 precision control on*both*dialects\.linalg: SmolLM2\-1\.7B \+C1C\_\{1\}\+C2C\_\{2\}\+C3C\_\{3\}\(red border, “ours”\) = 80\.0%, leading CodeLlama\-34B \(58\.7%\) by\+21\.3\+21\.3pp, Granite\-34B \(35\.7%\) by\+44\.3\+44\.3pp, StarCoder2\-15B \(54\.9%\) by\+25\.1\+25\.1pp, and the Granite\-Code\-8B\-fp16 control \(50\.1%±\\pm1\.6pp\) by\+29\.9\+29\.9pp; CIs non\-overlapping across all five systems\.arith\+func: SmolLM2 \(53\.2%±\\pm1\.8pp\) trails CodeLlama\-34B \(59\.8%\) by−6\.6\-6\.6pp \(within CI\), narrowly leads Granite\-34B \(51\.5%\) by\+1\.7\+1\.7pp \(within CI\), trails StarCoder2\-15B \(66\.8%\) by−13\.6\-13\.6pp, and trails the Granite\-Code\-8B\-fp16 control \(68\.2%±\\pm3\.0pp\) by−15\.0\-15\.0pp\.n=200n\{=\}200per seed for arith\+func,n=125n\{=\}125per seed for linalg, three seeds each\.![Refer to caption](https://arxiv.org/html/2607.18254v1/x6.png)Figure 6:Error\-category progression across constraint levels, SmolLM2\-1\.7B\. Each layer specifically collapses its target bucket\.arith\+func:C3C\_\{3\}collapsestype\_ssa56→1756\\to 17\(−70%\-70\\%\)\.linalg:C2C\_\{2\}eliminatessyntax22→022\\to 0;type\_ssais already<5<5because linalg’sins\(\.\.\.\) outs\(\.\.\.\)re\-declares types at each use\-site\.![Refer to caption](https://arxiv.org/html/2607.18254v1/x7.png)Figure 7:Paired bootstrapΔ\\Deltaverify with 95% CIs\.C1C\_\{1\}\+C2C\_\{2\}\+C3−C1C\_\{3\}\-C\_\{1\}\+C2C\_\{2\}onarith\+funcis\+13\.0\+13\.0pp with CI\[\+8\.5,\+18\.0\]\[\+8\.5,\+18\.0\]; the same comparison onlinalgis near\-null \(\+0\.8\+0\.8pp, CI\[0\.0,\+2\.4\]\[0\.0,\+2\.4\]\) because linalg’s target error bucket is already empty afterC2C\_\{2\}\.![Refer to caption](https://arxiv.org/html/2607.18254v1/x8.png)Figure 8:Hidden Cost of Structure replication with null result\.C1C\_\{1\}is monotonically beneficial on both SLMs \(\+20\.0\+20\.0pp SmolLM2,\+7\.5\+7\.5pp Phi, bothp<0\.0001p<0\.0001\)\. Under 3\-shot priming with a type\-domain\-aware grammar and bounded identifiers, the RANLP 2025 HCS reversal does not reproduce\.Table 6:Error categorization across constraint levels\. Arity and dialect\-misuse buckets are 0 across every SmolLM2 cell and are omitted\.![Refer to caption](https://arxiv.org/html/2607.18254v1/x9.png)Figure 9:Per\-op verify rate under SmolLM2 \+C1C\_\{1\}\+C2C\_\{2\}\+C3C\_\{3\}onlinalg\(seed\-0 ladder run at uniformn=125n\{=\}125\)\. Element\-wise ops approach 100%; shape\-reasoning ops \(transpose,broadcast\) show the residual gap motivating a futureC4C\_\{4\}shape\-inference layer\.Table 7:Per\-seed verify\-valid rates across the apples\-to\-apples cells\. Four systems×\\timestwo dialects, plus a Granite\-Code\-8B\-fp16 same\-family precision control on both dialects, atn=200n\{=\}200\(arith\+func\) orn=125n\{=\}125\(linalg\) per seed, seeds\{0,1,2\}\\\{0,1,2\\\}\. Mean is the across\-seed average;±\\pmhalf\-range is\(max−min\)/2\(\\max\-\\min\)/2across the three seeds\. Where seed\-0 differs from Table[2](https://arxiv.org/html/2607.18254#S5.T2)\(e\.g\., SmolLM2 \+C1C\_\{1\}\+C2C\_\{2\}\+C3C\_\{3\}onarith\+func: 52\.0% vs 67\.5%\), Table[7](https://arxiv.org/html/2607.18254#A4.T7)is authoritative and the two come from different runs \(single\-seed ladder vs three\-seed uniform\-nn\)\.Cells0s1s2mean±\\pmhrSmolLM2 \+C1C\_\{1\}\+C2C\_\{2\}\+C3C\_\{3\}, arith\+func52\.0%52\.0%55\.5%53\.2%±1\.8\\pm 1\.8ppSmolLM2 \+C1C\_\{1\}\+C2C\_\{2\}\+C3C\_\{3\}, linalg80\.0%80\.0%80\.0%80\.0%±0\.0\\pm 0\.0ppGranite\-Code\-34B\-Q4 \+C1C\_\{1\}\+C3C\_\{3\}, arith\+func49\.5%54\.5%50\.5%51\.5%±2\.5\\pm 2\.5ppGranite\-Code\-34B\-Q4 \+C1C\_\{1\}\+C3C\_\{3\}, linalg34\.4%40\.8%32\.0%35\.7%±4\.4\\pm 4\.4ppCodeLlama\-34B\-Q4 \+C1C\_\{1\}\+C3C\_\{3\}, arith\+func60\.5%59\.0%60\.0%59\.8%±0\.8\\pm 0\.8ppCodeLlama\-34B\-Q4 \+C1C\_\{1\}\+C3C\_\{3\}, linalg59\.2%60\.8%56\.0%58\.7%±2\.4\\pm 2\.4ppStarCoder2\-15B\-Q4 \+C1C\_\{1\}\+C3C\_\{3\}, arith\+func68\.0%65\.0%67\.5%66\.8%±1\.5\\pm 1\.5ppStarCoder2\-15B\-Q4 \+C1C\_\{1\}\+C3C\_\{3\}, linalg53\.6%55\.2%56\.0%54\.9%±1\.2\\pm 1\.2ppGranite\-Code\-8B\-fp16 \+C1C\_\{1\}\+C3C\_\{3\}, arith\+func \(qtz\. control\)67\.5%71\.5%65\.5%68\.2%±3\.0\\pm 3\.0ppGranite\-Code\-8B\-fp16 \+C1C\_\{1\}\+C3C\_\{3\}, linalg \(qtz\. control\)49\.6%48\.8%52\.0%50\.1%±1\.6\\pm 1\.6ppTable 8:Summary of empirical claims and supporting evidence\.#### Qualitative example \(Linalg\-Spec\-30 prompt 14, “transpose a 3x5xf32 memref”\)\.

SmolLM2 \+C1C\_\{1\}\+C2C\_\{2\}\+C3C\_\{3\}emits:

module\{func\.func@t\(%A:memref<?x?xf32\>,%B:memref<?x?xf32\>\)\{

linalg\.transposeins\(%A:memref<?x?xf32\>\)

outs\(%B:memref<?x?xf32\>\)permutation=\[1,0\]

return

\}\}

which passesmlir\-opt \-\-verify\. CodeLlama\-34B \+C1C\_\{1\}instead invents a hand\-rolledlinalg\.genericwith malformed indexing maps \(\(d0, d1\)\[s0 \-\> s0 \* 5 \+ d1\]\) that fails parse\. This illustratesC2C\_\{2\}’s role: the grammar restrictslinalg\.\*to the 12 named ops in scope, so SmolLM2 cannot emitlinalg\.genericeven by few\-shot imitation\.

#### Numerical\-consistency note \(Tables[2](https://arxiv.org/html/2607.18254#S5.T2)vs[7](https://arxiv.org/html/2607.18254#A4.T7)\)\.

Table[2](https://arxiv.org/html/2607.18254#S5.T2)is the seed\-0 ladder run, retained for the within\-seed constraint\-layer\-progression view it gives\. Table[7](https://arxiv.org/html/2607.18254#A4.T7)reports per\-seed verify\-valid rates under the uniform\-n=200n\{=\}200\(arith\+func\) / uniform\-n=125n\{=\}125\(linalg\) protocol used for all three\-seed directional claims in this paper\. On arith\+func, Table[2](https://arxiv.org/html/2607.18254#S5.T2)’s seed\-0 SmolLM2 \+C1C\_\{1\}\+C2C\_\{2\}\+C3C\_\{3\}cell reads 67\.5%\[61\.0,74\.0\]\[61\.0,74\.0\]; Table[7](https://arxiv.org/html/2607.18254#A4.T7)’s seed\-0 cell under the same configuration reads 52\.0% \(three\-seed mean 53\.2%±1\.8\\pm 1\.8pp\)\. The two cells differ because they were collected under different protocols across the paper’s two evaluation runs; Table[7](https://arxiv.org/html/2607.18254#A4.T7)is authoritative for all directional cross\-system claims\.

## Appendix EDatasheet for Datasets

We follow the Gebru et al\.\[[6](https://arxiv.org/html/2607.18254#bib.bib10)\]Datasheet\-for\-Datasets template\. The full datasheet ships in the reproducibility archive \(docs/datasheets/\); a condensed version follows\.

#### Motivation\.

Natural\-language\-to\-MLIR \(“NL→\\toMLIR”\) is an under\-represented task in existing code\-LM benchmarks\. Existing MLIR corpora \(e\.g\., the LLVM in\-treemlir/test/\) are designed for compiler regression testing, not NL pairing; HumanEval/MBPP target general\-purpose code\. Our four benchmarks fill this gap; their composition is summarized in Table[9](https://arxiv.org/html/2607.18254#A5.T9)\.

Table 9:Per\-benchmark composition\. Spec\-\* benchmarks were author\-written against public ODS specs and verifier\-filtered; Held\-Out\-200 was generated by a parametric sweep and verifier\- filtered; Out\-Of\-Grammar\-25 was hand\-authored against StableHLO ops the grammar does not cover; Functional\-Reference\-30 is the hand\-authored functional set used to bound the verify\-valid→\\tooutput\-match gap\.
#### Composition\.

MLIR\-Spec\-150: 150 NL→\\toMLIR pairs,arith\+func\+memref, difficulty mix 38/44/18% easy/medium/hard\. All reference MLIR verify\-clean undermlir\-opt \-\-verify\-diagnostics\.Linalg\-Spec\-30: 30 pairs covering the 12 linalg named ops in scope under memref semantics\.StableHLO\-Spec\-30: 30 author\-curated pairs covering 10 op families with tensor semantics\.StableHLO\-Held\-Out\-200: 200 programs constructed by a parametric sweep over 7 op families×\\times6 dtypes×\\timesmultiple shape ranks, filtered to iree\-compile\-clean \(585 candidates→\\to200 kept\)\.

#### Collection \+ preprocessing\.

Pairs are hand\-authored \(Spec\-30/150\) or parametrically generated and filtered \(Held\-Out\-200\)\. Each JSON contains\{id, nl, mlir, difficulty, dialect, notes\}\. No human\-subject data; no PII\.

#### Intended uses\.

Evaluating NL→\\toMLIR generation systems \(constrained or unconstrained\) under a verifier\-based pass\- rate metric\.Not suitable forfunctional\-correctness evaluation without an additional lowering \+ execution harness; the benchmarks measure structural validity only\.

#### Distribution \+ license\.

All four benchmarks, generated outputs, grammars, and code released underApache License 2\.0\(SPDX: Apache\-2\.0\)\. The Dockerfile pins LLVM, IREE, and llama\.cpp to their respective upstream licenses\.

#### Maintenance\.

Releases are version\-tagged in the reproducibility archive; corrections land in the next tag\. Issue tracker and contact point are in the archive’sCONTACT\.md\.

#### Croissant metadata\.

Each benchmark ships with acroissant\.jsonateval/benchmarks/<name\>/croissant\.jsoncontaining both core and Responsible\-AI fields \(per MLCommons Croissant 1\.0\[[15](https://arxiv.org/html/2607.18254#bib.bib11)\]\+ RAI extensions\):cite\-as,license,distribution,recordSet,annotationswith difficulty labels, and therai:dataBiases/rai:dataLimitationsfields describing the “author\-curated” and “parametric\-sweep” sampling biases explicitly\.

#### Reuse scenarios\.

Beyond evaluating the constraint stack proposed in this paper, we anticipate four uses for these benchmarks\. \(i\)*Evaluating new SLMs on MLIR generation\.*A researcher with a new small open\-weight code model can run the released decoder against MLIR\-Spec\-150 and Linalg\-Spec\-30 to obtain directly comparable verify\-valid rates; the test\-only license precludes fine\-tuning on these pairs but does not preclude evaluation\. \(ii\)*Evaluating retrieval\-augmented MLIR generation\.*The pairs are short and self\-contained, making them suitable as targets for retrieval\-augmented decoding studies that condition on dialect\-specific reference programs\. \(iii\)*Evaluating fine\-tuned MLIR models trained on external corpora\.*StableHLO\-Held\-Out\-200’s parametric construction provides resistance to memorization through its templated\-sweep generation procedure; researchers releasing fine\-tuned MLIR models can use it as a held\-out evaluation set, subject to the test\-only license\. \(iv\)*Evaluating future constraint\-decoding methods\.*The Out\-Of\-Grammar\-25 stress set and then=30n\{=\}30functional reference set together let a future method demonstrate \(a\) graceful out\-of\-grammar degradation and \(b\) closing of the verify\-to\- functional gap, both of which the present paper leaves open\.

## Appendix FReproducibility\-protocol Details

This appendix documents the full reproducibility protocol including code, data, experimental setup, statistics, metric validation, and per\-prompt artifacts, that the NeurIPS Paper Checklist’s reproducibility questions point to for evidence\.

#### Code release\.

All code is released under Apache\-2\.0 in the reproducibility archive \(submission\_artifact\.tar\.gz; built from[https://github\.com/plawanrath/slm\-to\-mlir\-constrained\-emitter](https://github.com/plawanrath/slm-to-mlir-constrained-emitter)\)\.scripts/env/requirements\.lock\.txtpins every host\-side dependency at exact versions and is the single source of truth\. Single\-command end\-to\-end reproduction from the archive:docker build \-t mlir\-emit \. && docker run mlir\-emit python scripts/make\_paper\_figures\_final\.pyregenerates every figure and table byte\-identically\. The soundness\-test wrapperscripts/env/check\_sanity\.pycertifies that a fresh environment will reproduce the paper’s numbers\.

#### Data release\.

All four primary benchmarks \(MLIR\-Spec\-150, Linalg\-Spec\-30, StableHLO\-Spec\-30, StableHLO\-Held\-Out\-200\) plus the StableHLO\-Out\-Of\-Grammar\-25 stress set and the hand\-authoredn=30n\{=\}30functional reference set are released\. The functional set is released as evaluation evidence \(10 prompts per dialect; not a training or fine\-tuning set\)\. Each benchmark ships with a per\-instance JSON schema ateval/benchmarks/<name\>/schema\.jsonand a Croissant 1\.0 metadata record ateval/benchmarks/<name\>/croissant\.jsonwith MLCommons Responsible\-AI extension fields \(rai:dataBiases,rai:dataLimitations, provenance\) populated\. The Datasheet for Datasets atdocs/datasheets/datasheet\.mdcovers every Gebru\-template field, including explicit “uses the dataset does not support” \(fine\-tuning, functional\-correctness testing\); the full datasheet is in §[E](https://arxiv.org/html/2607.18254#A5)\. License is Apache\-2\.0 \(SPDX\) for both code and data; the test\-only restriction is recorded in the datasheet’suses\_not\_supportedfield and in the per\-benchmark Croissantrai:dataLimitationsfield\.

#### Experimental protocol\.

SmolLM2\-1\.7B\-Instruct served via MLX\-LM 0\.31\.2 on Apple Silicon \(M4 Max, 128 GB unified memory\) at fp16\. Outlines 1\.2\.12 with the llguidance backend for C1 \(CFG\-guided decoding\) and C2 \(type\-domain splits\); rejection\-sampling wrapper for C3 \(5\-retry budget, post\-hocc3\_scope\.validatefilter\)\. Decoding parameters: first try greedy attemperature=0\.0, retries attemperature=0\.8;max\_tokens=600for the SmolLM2 cell,max\_tokens=256for the 15B/34B baseline cells\. Three\-shot in\-context priming with the format<\|im\_start\|\>user\.\.\.<\|im\_end\|\>\\n<\|im\_start\|\>assistant\.\.\.<\|im\_end\|\>; example selection is fixed per benchmark and stored in the archive\. Baselines \(CodeLlama\-34B\-Instruct, Granite\-Code\-34B\-Instruct, StarCoder2\-15B:instruct\) served via Ollama at Q4\_K\_M quantization under the same priming protocol; Granite\-Code\-8B\-Instruct served via MLX at fp16 as the precision control\. All seeds reported: 0, 1, 2 for three\-seed apples\-to\-apples cells; bootstrap seednumpy\.random\.default\_rng\(0\)\. Verifier toolchain pinned: LLVMllvmorg\-19\.1\.7\(mlir\-opt\), iree\-compiler 20241104\.1068; both pinned inscripts/env/requirements\.lock\.txt\.

#### Statistical reporting\.

95% paired\-bootstrap percentile CIs on every cell \(10,000 resamples\), paired byprompt\_idso each resample preserves per\-prompt pairing across constraint conditions\. One\-sided paired\-bootstrap p\-values on every directional claim\. Multi\-seed apples\-to\-apples cells use three seeds\{0,1,2\}\\\{0,1,2\\\}; “mean” reports the arithmetic mean across seeds and “±\\pmhalf\-range” reports\(max−min\)/2\(\\max\-\\min\)/2\. Power\-analysis statement: at expected baseline pass\-ratep=0\.55p\{=\}0\.55,n=200n\{=\}200yields 95% bootstrap CI half\-width below±8\\pm 8pp; atp=0\.5p\{=\}0\.5,n=125n\{=\}125below±9\\pm 9pp; atp=0\.5p\{=\}0\.5,n=30n\{=\}30below±18\\pm 18pp\.

#### Metric validation\.

Verifier\-tool substitution validated:iree\-compile \-\-compile\-to=input50/50 concordant against upstreamstablehlo\-opt v1\.4\.0on a stratifiedn=50n\{=\}50sample across six op families\. Build commands and per\-instance log in Appendix[C](https://arxiv.org/html/2607.18254#A3)\. Empty\-input verifier gotcha disclosed and guarded:iree\-compile \-\-compile\-to=inputaccepts empty stdin as a valid emptymodule \{\}and returns success, so our wrapper requires afunc\.func @substring before invokingiree\-compile\. We recommend any reuser apply the same guard\.

#### Per\-prompt artifacts\.

Every per\-prompt generation is released as\.jsonl\(one line per prompt×\\timesseed, with raw decoder output, retry log, verifier verdict\)\. Bootstrap artifacts released:results/day52/layer\_delta\_bootstrap\.json\(paired\-bootstrap CIs and one\-sided p\-values for the §[6](https://arxiv.org/html/2607.18254#S6)layer\-deltas\),results/day51\_seed0\_n200/apples\_to\_apples\.json\(the §[5](https://arxiv.org/html/2607.18254#S5)apples\-to\-apples cells with their per\-prompt pairing\)\.

## NeurIPS Paper Checklist

1. 1\.Claims
2. Question: Do the main claims made in the abstract and introduction accurately reflect the paper’s contributions and scope?
3. Answer:\[Yes\]
4. Justification: The abstract and §[1](https://arxiv.org/html/2607.18254#S1)frame the headline as dialect\-specific: training\-free constrained decoding lifts SmolLM2\-1\.7B to verify\-valid rates that match or exceed 15B/34B baselines onlinalg\(robust across three seeds\) and on hand\-curated StableHLO\-Spec\-30 \(corpus\-conditional; the templated parametric Held\-Out\-200 saturates 15B/34B baselines\), while onarith\+funcwe report parity\-to\-loss\. The scope is restated in §[5](https://arxiv.org/html/2607.18254#S5)and §[7](https://arxiv.org/html/2607.18254#S7)to prevent over\-reading\.
5. 2\.Limitations
6. Question: Does the paper discuss the limitations of the work performed by the authors?
7. Answer:\[Yes\]
8. Justification: §[7](https://arxiv.org/html/2607.18254#S7)enumerates: 30B “C1C\_\{1\}” is rejection sampling rather than token\-level masked decoding; the structural\-vs\-functional verification gap \(verify\-valid is necessary but not sufficient for correctness, bounded by ann=30n\{=\}30functional reference set with 50% output\-match overall\);arith\+funcis a parity\-to\-loss cell at multi\-seed mean; the StableHLO claim is corpus\-conditional \(the templated Held\-Out\-200 saturates 15B/34B baselines\); single SLM family, single hardware platform, single LLVM/iree\-compiler version pin, with a Granite\-Code\-8B\-fp16 quantization\-asymmetry control onlinalgruling out the precision\-vs\-quantization confound; grammar coverage limited to the released dialects; the in\-line coupled decoder is currently a theoretical companion rather than an empirical contribution\.
9. 3\.Theory assumptions and proofs
10. Question: For each theoretical result, does the paper provide the full set of assumptions and a complete \(and correct\) proof?
11. Answer:\[Yes\]
12. Justification: Appendix[A](https://arxiv.org/html/2607.18254#A1)gives Theorem 1 \(soundness\), Theorem 2 \(BPE\-refined coverage\), and Theorem 3 \(equivalence between in\-line and rejection\-sampled decoders on the accepted\-string set\)\. Each carries an explicit proof and a remark on the “vocab\-covers\-ASCII” assumption needed for Theorem 2’s character\-oracle construction\.
13. 4\.Experimental result reproducibility
14. Question: Does the paper fully disclose all the information needed to reproduce the main experimental results of the paper to the extent that it affects the main claims and/or conclusions of the paper \(regardless of whether the code and data are provided or not\)?
15. Answer:\[Yes\]
16. Justification: §[B](https://arxiv.org/html/2607.18254#A2)and Appendix[F](https://arxiv.org/html/2607.18254#A6)document the decoder configuration \(MLX\-LM 0\.31\.2 with Outlines 1\.2\.12 \+ llguidance for SmolLM2; Ollama for the 15B/34B baselines; 5\-retry rejection budget; first try greedy attemperature=0\.0, retries attemperature=0\.8;max\_tokens=600for the SmolLM2 cell andmax\_tokens=256for the 15B/34B baseline cells; 3\-shot priming format\), the verifier toolchain pins \(LLVMllvmorg\-19\.1\.7,iree\-compiler 20241104\.1068\), and the bootstrap protocol \(10,000 resamples, percentile 95% CI,numpy\.random\.default\_rng\(0\)\)\. The lock filescripts/env/requirements\.lock\.txtis the single source of truth for environment versions\.
17. 5\.Open access to data and code
18. Question: Does the paper provide open access to the data and code, with sufficient instructions to faithfully reproduce the main experimental results, as described in supplemental material?
19. Answer:\[Yes\]
20. Justification: Released assubmission\_artifact\.tar\.gz; sources at[https://github\.com/plawanrath/slm\-to\-mlir\-constrained\-emitter](https://github.com/plawanrath/slm-to-mlir-constrained-emitter); benchmarks at the sixhuggingface\.co/datasets/plawanrath/\.\.\.URLs in Appendix[B](https://arxiv.org/html/2607.18254#A2)\. Apache\-2\.0 license for both code and data\. Runningpython scripts/make\_paper\_figures\_final\.pyfrom the archive regenerates every figure and table byte\-identically given the input\.jsonlfiles\.
21. 6\.Experimental setting/details
22. Question: Does the paper specify all the training and test details \(e\.g\., data splits, hyperparameters, how they were chosen, type of optimizer\) necessary to understand the results?
23. Answer:\[Yes\]
24. Justification: §[4](https://arxiv.org/html/2607.18254#S4)\(Experimental Setup\) and §[B](https://arxiv.org/html/2607.18254#A2)cover model choices \(SmolLM2\-1\.7B\-Instruct primary; CodeLlama\-34B, Granite\-Code\-34B, StarCoder2\-15B baselines under Q4\_K\_M quantization via Ollama\), the prompt template, in\-context example selection, evaluation protocol per dialect, and the 5\-retry rejection\-sampling budget\. No training is involved \(the work is training\-free\); all configurations are inference\-time\.
25. 7\.Experiment statistical significance
26. Question: Does the paper report error bars suitably and correctly defined or other appropriate information about the statistical significance of the experiments?
27. Answer:\[Yes\]
28. Justification: All cell\-level results are reported with paired bootstrap 95% percentile CIs \(10,000 resamples\)\. Apples\-to\-apples comparisons \(Table[7](https://arxiv.org/html/2607.18254#A4.T7)\) use 3\-seed full\-nnmulti\-seed protocol with mean±\\pmacross\-seed range\. Per\-layer deltas \(§[6](https://arxiv.org/html/2607.18254#S6)\) include CIs that explicitly exclude or include zero, and we test against a pre\-registered\+10\+10pp threshold\.
29. 8\.Experiments compute resources
30. Question: For each experiment, does the paper provide sufficient information on the computer resources \(type of compute workers, memory, time of execution\) needed to reproduce the experiments?
31. Answer:\[Yes\]
32. Justification: §[5](https://arxiv.org/html/2607.18254#S5)reports SmolLM2 wall\-clock as 1\.65–1\.86 s/generation; baselines 16–40 s/generation\. All experiments run on a single Apple M4 Max laptop \(no GPU cluster\)\. The longest single experimental run \(3\-seed baselinelinalgmulti\-seed, 750 samples across three 34B/15B models\) took 5\.4 hours wall\-clock\. Total compute budget for the paper is reproducible on a single 64GB\-RAM Apple Silicon machine,∼20\{\\sim\}20days of wall\-clock inference time across all systems; no cluster\-scale training runs and no pre\-training or fine\-tuning\.
33. 9\.Code of ethics
35. Answer:\[Yes\]
36. Justification: No human subjects, no PII, no crowdsourced labor, no offensive content\. The benchmark domain is technical MLIR code and English descriptions of numerical operations\. All evaluated models are open\-weight and accessed via their published licenses\.
37. 10\.Broader impacts
38. Question: Does the paper discuss both potential positive societal impacts and negative societal impacts of the work performed?
39. Answer:\[Yes\]
40. Justification:*Intended use and positive impact\.*NL→\\toMLIR generation is a productivity tool for compiler engineers; the released benchmarks enable laptop\-scale constrained code generation for compiler infrastructure and are intended for method evaluation, not as training data for safety\-critical model deployment\.*Foreseeable risks\.*\(i\)*False\-pass risk*: a verify\-valid generation may still compute the wrong function; users should not treat verify\-valid output as correctness\-certified \(§[7](https://arxiv.org/html/2607.18254#S7), Table[5](https://arxiv.org/html/2607.18254#S5.T5)\)\. \(ii\)*Benchmark contamination*: MLIR\-Spec prompts are short NL descriptions of common ops; if memorized by a pretrained model, verify\-valid rates would rise without reflecting generalization\. \(iii\)*Pretraining\-provenance ambiguity*: there is no auditable line between “MLIR seen during pretraining” and verify\-valid generation at inference; absolute rates should be read as artifacts of pretraining plus the constraint stack, not as model\-intrinsic capability\.*Responsible release\.*Benchmarks contain only public MLIR programs derived from public dialect specs; no PII and no human\-subject data\. We evaluate only a few open\-weight models on a deliberate scope\-of\-evaluation basis, not as an ethical claim about excluded families; the method transfers to any open\-weight model with an MLX or llama\.cpp implementation\.
41. 11\.Safeguards
42. Question: Does the paper describe safeguards that have been put in place for responsible release of data or models that have a high risk for misuse \(e\.g\., pre\-trained language models, image generators, or scraped datasets\)?
43. Answer:\[N/A\]
44. Justification: The released artifacts are MLIR benchmarks and a constrained\-decoding wrapper around publicly available open\-weight models\. No new pretrained model weights are released\. We assess the misuse risk of structurally\-valid IR generation as low\.
45. 12\.Licenses for existing assets
46. Question: Are the creators or original owners of assets \(e\.g\., code, data, models\), used in the paper, properly credited and are the license and terms of use explicitly mentioned and properly respected?
47. Answer:\[Yes\]
48. Justification: All four evaluated models \(SmolLM2\[[1](https://arxiv.org/html/2607.18254#bib.bib17)\], CodeLlama\[[20](https://arxiv.org/html/2607.18254#bib.bib18)\], Granite\-Code\[[14](https://arxiv.org/html/2607.18254#bib.bib19)\], StarCoder2\[[13](https://arxiv.org/html/2607.18254#bib.bib20)\]\) are accessed via their published open\-weight licenses through Hugging Face Hub or Ollama\. Phi\-3\.5\-mini \(used in §[6](https://arxiv.org/html/2607.18254#S6)only\) likewise\. MLIR \(Apache\-2\.0\), StableHLO \(Apache\-2\.0\), IREE \(Apache\-2\.0\), Outlines \(Apache\-2\.0\), and llguidance \(MIT\) are all properly cited and license\-compatible with our Apache\-2\.0 release\.
49. 13\.New assets
50. Question: Are new assets introduced in the paper well documented and is the documentation provided alongside the assets?
51. Answer:\[Yes\]
52. Justification: A Gebru\-style datasheet for the released benchmarks lives atdocs/datasheets/datasheet\.mdand is summarized in §[B](https://arxiv.org/html/2607.18254#A2)and the Datasheet section\. Per\-benchmark Croissant 1\.0 metadata records ship ateval/benchmarks/<name\>/croissant\.jsonwithrai:dataBiasesandrai:dataLimitationsfields populated\. License: Apache\-2\.0 \(SPDX: Apache\-2\.0\)\.
53. 14\.Crowdsourcing and research with human subjects
54. Question: For crowdsourcing experiments and research with human subjects, does the paper include the full text of instructions given to participants and screenshots, if applicable, as well as details about compensation \(if any\)?
55. Answer:\[N/A\]
56. Justification: No crowdsourcing was used\. All benchmark prompts and reference MLIR programs were authored or generated by the submitting author and verifier\-filtered\.
57. 15\.Institutional review board \(IRB\) approvals or equivalent for research with human subjects
58. Question: Does the paper describe potential risks incurred by study participants, whether such risks were disclosed to the subjects, and whether Institutional Review Board \(IRB\) approvals \(or an equivalent approval/review based on the requirements of your country or institution\) were obtained?
59. Answer:\[N/A\]
60. Justification: No human\-subjects research\.
61. 16\.Declaration of LLM usage
62. Question: Does the paper describe the usage of LLMs if it is an important, original, or non\-standard component of the core methods in this research? Note that if the LLM is used only for writing, editing, or formatting purposes and does*not*impact the core methodology, scientific rigor, or originality of the research, declaration is not required\.
63. Answer:\[Yes\]
64. Justification: Language models are the subject of evaluation, not an unstated tool: the paper proposes a constrained\-decoding scaffold around SmolLM2\-1\.7B\-Instruct \(primary\), Phi\-3\.5\-mini\-Instruct \(HCS replication only\), and three baselines \(CodeLlama\-34B, Granite\-Code\-34B, StarCoder2\-15B\) under Q4\_K\_M quantization\. All decoder configurations, prompting formats, and rejection\-sampling budgets are specified in §[4](https://arxiv.org/html/2607.18254#S4)and Appendix[F](https://arxiv.org/html/2607.18254#A6)\. No LLM\-generated text appears in the released benchmarks; all reference MLIR programs are author\-curated and verifier\-filtered\.