SERIAL-7: Deriving, Realizing, and Preserving Machine-Verifiable Outputs Across Representations

Youngkyung Seo; MiHyeon Kim; Jisoo Lee; Hwijung Ryu

cs.AIOct 30, 2026

SERIAL-7: Deriving, Realizing, and Preserving Machine-Verifiable Outputs Across Representations

Authors: Youngkyung Seo, MiHyeon Kim, Jisoo Lee, Hwijung Ryu

Organizations: KT Corporation

Abstract

Large language models increasingly generate structured outputs consumed by programs and downstream systems, where semantic correctness alone does not guarantee reliable execution. We introduce SERIAL-7, a Korean-English benchmark built around an executable verification framework for machine-verifiable generation across seven representations. Using 177 validated canonical artifacts, SERIAL-7 separates semantic derivation (Derive), constrained artifact generation (Realize), and cross-representation preservation (Preserve). Its 43 atomic representation constraints are paired with executable checks over format, structure, and task-specific semantics, enabling progressively stricter verification from representation compliance to full artifact validity. Across ten models, REALIZE-L3 HSR ranges from 42.0% to 93.9%, while Full Compliance exposes additional artifact-level failures beyond correct final answers and valid representations. These results show that reliable structured generation requires explicit, executable verification of how artifacts are realized and preserved across representations.

Figures & tables

Figure 1: Model performance on SERIAL-7. $\bigstar$ and $\bigstar$ denote the best global and Korean-developed models, respectively.

Figure 2: Evaluation settings for machine-verifiable generation in SERIAL-7 . The same semantic artifact is evaluated through semantic derivation, verified realization under explicit representation contracts, and cross-representation artifact preservation. Realize uses a shared base representation contract, with L1, L2, and L3 additionally activating one, two, and three independently sampled atomic constraints, respectively. For structured conditions, executable predicates verify representation, structure, and task-specific semantic requirements.

Benchmark	Multiple	Paired	Fixed semantic	Compositional	Deterministic	Failure
	representations	representations	target	constraints	verification	localization
FoFo [ 23 ]	$\blacktriangle$	✗	✗	✗	✗	$\blacktriangle$
VFF [ 22 ]	✗	✗	✗	✓	✓	$\blacktriangle$
AgentIF [ 15 ]	✗	✗	✗	✓	$\blacktriangle$	✓
StructEval [ 24 ]	✓	$\blacktriangle$	$\blacktriangle$	✗	$\blacktriangle$	$\blacktriangle$
ReCode [ 19 ]	✗	✗	✓	✗	✓	$\blacktriangle$

Table 1: Comparison with closely related evaluation frameworks. ✓ = explicitly evaluated,

\blacktriangle

= partially or indirectly covered, and ✗ = not explicitly targeted. Paired representations denotes controlled evaluation of the same underlying semantic target under multiple output representations.

Figure 3: Construction pipeline of Serial-7 . Source problems from four reasoning benchmarks are normalized into Canonical-IR candidates, mechanically validated, and, when necessary, repaired and revalidated before inclusion. Korean and English evaluation instances are constructed from the same validated canonical artifact through LLM translation followed by bilingual review.

Representation	#	Atomic constraints
JSON	6	inputs_as_map , steps_as_map , args_as_objects , answer_object , numeric_as_string , key_order
XML	5	args_as_attribute , namespace , sibling_order , value_as_attribute , answer_last
Markdown	7	inputs_as_table , steps_as_table , fence , inline_code_ids , heading_depth , blockquote_answer , bold_names
HTML	6	table_for_inputs , table_for_steps , dl_for_answer , semantic_element , strong_answer , heading_hierarchy
L a T e X	6	tabular_inputs , enumerate_steps , siunitx , math_mode , texttt_ids , bold_ids
YAML	7	inputs_as_map , steps_as_map , answer_object , numeric_as_string , key_order , args_as_objects , flow_args

Table 2: Atomic representation constraints in Serial-7 . Constraints modify the representation of a shared canonical artifact without changing its semantic content.

Panel of Figure 5 — Figure 5: Executable atomic-rule diagnostics for constrained realization. (a) Representation-wise atomic-rule accuracy, computed only over instances in which the corresponding rule is active. (b) Cross-configuration accuracy distributions for the ten most difficult atomic constraints, ranked by mean accuracy across configurations.

Figure 7: Pooled source–target Preservation HSR. Rows denote source representations and columns denote targets. Each cell pools only artifacts for which the corresponding transfer was sampled; opposite transfers therefore need not contain identical artifact sets.

Figure 8: Paired English–Korean performance differences. (a) Aggregate configuration-level gaps; stars denote significance under two-sided paired permutation tests using canonical artifacts as the statistical unit, with Holm correction across models. (b) Condition-specific gaps across Derive , Realize , and Preserve , reported descriptively. Positive values favor English.

Appendix figures & tables27 assets

Supplementary material from the paper’s appendix.

Appendix

Figure 9: Per-model source–target preservation matrices. Rows indicate source representations and columns indicate target representations. Cells report target-side Format Compliance over the sampled instances available for each source–target pair.

Source	JSON	XML	Markdown	HTML	L a T e X	YAML	TOML
JSON	–	34	36	36	40	38	40
XML	40	–	45	39	45	36	45
Markdown	38	42	–	42	44	41	44
HTML	43	44	40	–	36	36	41
L a T e X	43	41	42	42	–	44	38
YAML	44	38	39	39	36	–	38

Appendix

Table 6: Support for sampled Preserve transfers. Each cell reports the number of artifact–language instances per model for which the corresponding directed transfer is evaluated. The same transfer grid is shared across all ten model configurations.

Figure 10: Model-specific pooled source–target asymmetry. $\Delta_{\mathrm{pool},FC}$ is the mean absolute Format Compliance difference between observed opposite transfers of the same representation pair. Opposite transfers may contain different artifact subsets.

Figure 11: Source- and target-side representation profiles. Source scores average Format Compliance over observed outgoing transfers, and target scores average Format Compliance over observed incoming transfers.

Figure 12: Conditional pass rates for atomic representation constraints. Each value is computed only over instances in which the corresponding rule is active. Rule labels additionally report the per-model activation count $n$ ; the same rule assignments are used for all model configurations.

Atomic rule	Support $n$	Mean Acc.
toml.key_order	72	0.743
latex.siunitx	69	0.785
yaml.answer_object	75	0.831
yaml.key_order	71	0.844
latex.math_mode	67	0.869
json.key_order	74	0.871

Appendix

Table 7: Representative difficult atomic constraints. Mean accuracy is computed across the ten evaluated model configurations using only Realize instances in which the corresponding rule is active. Support

n

denotes the number of active benchmark instances per model.

Model	Higher-performing setting	Prominent pattern
GPT-5.4	High constrained-realization HSR with a small descriptive Realize–Preserve gap.	Carrier-specific variation remains despite high aggregate performance.
Gemini-3.7-Flash	Highest observed L3 HSR and high preservation, with similar performance across the independently sampled L1–L3 conditions.	A localized representation weakness remains visible, particularly on L a T e X .
Mi:dm	High Preserve HSR and competitive REALIZE-L1 performance.	HSR is noticeably lower in the independently sampled L3 condition than in L1.
Solar-Pro4	High Preserve HSR and comparatively high HSR on selected carriers such as XML.	Performance is less uniform across representation families.
GPT-5.4-nano	High Preserve HSR despite substantially lower constrained-realization HSR than the top-performing models.	HSR is substantially lower in the independently sampled L3 condition than in L1.
Nemotron-3-Super	Highest observed Preserve HSR among the evaluated models.	Substantially lower L3 HSR, producing a large descriptive Realize–Preserve gap.

Appendix

Table 8: Model-level performance patterns across Serial-7 . The table summarizes relative performance patterns rather than defining an additional aggregate ranking.

Audit	Validation target	Result
Round-trip validation	Whether gold realizations can be serialized, recovered as Canonical IR, and accepted by the corresponding predicates.	Base: 1,239/1,239; Realize : 1,470/1,470; Preserve : 1,695/1,695.
Atomic-rule validation	Whether sampled rule combinations are recoverable and near-miss examples are rejected by the intended checker.	777 combinations, 0 failures; 43/43 rules covered by near-miss tests.
Leakage audit	Whether valid transformations are incorrectly penalized and format predicates remain invariant to semantics-preserving perturbations.	987 valid transformations, 0 false penalties; 29/33 rule types invariant.
Prompt–checker alignment	Whether scored predicates are stated and checked consistently across Korean and English specifications.	0 unstated checks; 0 unmeasured requirements; 0 language-symmetry violations.

Appendix

Table 9: Executable-verifier audits for Serial-7 .

Target	$n$	Sampling	Human–Human	Automatic–Human
Active-constraint compliance	210	$7$ formats $\times$ $3$ conditions $\times$ $2$ languages $\times$ $5$ examples	203/210 (96.7%); $\kappa=0.93$	201/210 (95.7%)
Overall format compliance	210	Same structured sample	204/210 (97.1%); $\kappa=0.94$	202/210 (96.2%)
Derive semantic correctness	90	Stratified by language, model, and judge verdict	89/90 (98.9%); $\kappa=0.97$	88/90 (97.8%)

Appendix

Table 10: Human validation of Serial-7 . Human–Human reports agreement and Cohen’s

\kappa

before adjudication; Automatic–Human compares the automatic evaluator with final human labels.

	Human judgment
Executable verifier	Pass	Fail
Pass	58	2
Fail	4	56

Appendix

Table 11: Targeted executable-verifier audit. Rows denote verifier decisions and columns denote final human labels.

Model	OpenRouter identifier	Observed provider	Max. tokens
GPT-5.4	openai/gpt-5.4	OpenAI	12,000
GPT-5.4-nano	openai/gpt-5.4-nano	OpenAI	12,000
Gemini-3.7-Flash	google/gemini-3.7-flash	Google; Google AI Studio	12,000
Claude-Sonnet-5	anthropic/claude-sonnet-5	Claude Platform on AWS	16,000
Nemotron-3-Super-120B-A12B	nvidia/nemotron-3-super-120b-a12b	DeepInfra; DigitalOcean	12,000
Solar-Pro4	upstage/solar-pro4	Upstage	12,000

Appendix

Table 12: Configurations of the API-served models used for SERIAL-7.

Model	Weight representation	vLLM	Transformers
Motif-3-Beta	ModelOpt block FP8	0.20.2+motif3.g0b6f55172	5.14.1
A.X-K2	FP8 E4M3, block $128\times 128$	0.23.0	5.18.0.dev0
K-EXAONE-236B-A23B	BF16	0.20.2	5.8.1
Mi:dm K 3.0 Pro	BF16; no explicit quantization override	0.17.0	4.57.6

Appendix

Table 13: Weight and software configurations of the locally hosted models.

Parameter	Motif-3-Beta	A.X-K2	K-EXAONE-236B-A23B	Mi:dm K 3.0 Pro
Maximum context length	262,144	131,072	131,072	131,072
Temperature	1.0	0.6	1.0	0.6
Top- $p$	0.95	0.95	0.95	0.95
GPU-memory utilization	0.85	0.90	0.90	0.90
Tensor parallel size	1	8	4	8
Data parallel size	8	1	1	1

Appendix

Table 14: Inference, sampling, and parallelization settings for the locally hosted models.

Source	Problem structure	Sampling stratum
TabMWP	Table-grounded arithmetic	Question type, table scope, estimated reasoning depth, and operation type.
HRM8K	Korean mathematical reasoning	Predefined benchmark subset.
SciBench	Scientific calculation	Scientific subject.
MMLU-Pro (STEM)	STEM reasoning	Subject.

Appendix

Table 15: Source benchmarks and sampling strata used to construct the initial seed set.

Criterion	Requirement
Source validity	The original problem, supporting materials, and normalized artifact must be well formed and mutually consistent.
Answer consistency	The normalized final answer must be reconcilable with the official benchmark answer.
Grounding and leakage	Required values must be supported by the source record, and auxiliary text must not expose the answer without legitimate grounding.
Representation compatibility	Normalized values must be representable under the supported serialization contracts without introducing construction artifacts into the question.
Redundancy control	Repeated or near-duplicate question templates are canonicalized and capped to avoid over-representation of a single template family.

Appendix

Table 16: Principal criteria used for gold-set validation.

(a) Filtering flow
Stage	Excluded	Remaining
Initial seed set	–	500
Source / normalization validity	72	428
Answer inconsistency	61	367
Grounding or leakage failure	54	313
Representation incompatibility	83	230

Appendix

Table 17: Gold-set construction and retention statistics for SERIAL-7 . Rejection categories are mutually exclusive and assigned to the first unresolved validation failure after repair.

Component	Across KO–EN pair	Validation
Question and source text	Language-specific	Check internal language consistency.
Answer and numeric values	Semantically fixed	Require equivalent answers and preservation of required quantities.
Computation graph	Fixed	Reuse the same operations, dependencies, and constants.
Grounding evidence	Language-specific	Verify that required inputs remain supported in the corresponding language-specific source text.

Appendix

Table 18: Controlled construction of Korean–English benchmark pairs.

	Korean arm	English arm
Question	Emily가 7개의 Caribbean 휴가 패키지를 사려면 돈이 얼마나 필요합니까?	How much money does Emily need to buy 7 Caribbean vacation packages?
Materials	Caribbean 휴가 패키지 $\mid$ $503 Australian 휴가 패키지$ \mid554 Hawaiian 휴가 패키지 $\mid$ $613 European 휴가 패키지$ \mid867	Caribbean vacation package $\mid$ $503 Australian vacation package$ \mid554 Hawaiian vacation package $\mid$ $613 European vacation package$ \mid867
Shared answer	$3521$
Shared computation	R1 $=$ multiply ( caribbean_price , $7$ ) $=3521$

Appendix

Table 19: Example bilingual pair constructed from the same semantic artifact. Question and material surfaces vary by language, while the answer, semantic input values, and computation graph are shared.

IR component	Canonical content
Answer	$3521$
Input	caribbean_price $=503$
Step	R1 $=$ multiply ( caribbean_price , $7$ ) $=3521$

Appendix

Table 20: Example Canonical IR shared across representation conditions.

Condition	Input	Required behavior	Representation requirement
Derive	Question and optional materials	Solve the problem and provide the final answer.	None
Realize	Question and optional materials	Solve the problem and express the result under a target contract.	Base target representation + 1–3 sampled atomic constraints
Preserve	Instantiated source document	Rewrite the same semantic content in a target representation.	Base target representation only; no sampled atomic constraints

Appendix

Table 21: Evaluation prompt organization in SERIAL-7.

Component	When used	Function
Answer realization	All Realize instances	Defines the format-specific answer slot.
Format-specific graph syntax	Graph-bearing instances	Defines how inputs, steps, references, and values are serialized.
Shared graph validity	Graph-bearing instances	Constrains operation validity, dependency order, and consistency with the final answer.
Atomic representation constraints	All Realize L1–L3 instances	Modify local aspects of the base representation while preserving the same semantic artifact.
Common constraints	All constrained instances	Prevent unsupported additions and restrict the output to the requested document.

Appendix

Table 22: Components of the Realize prompt.

Format	Answer realization	Inputs and steps
JSON	A root JSON object containing answer .	inputs and steps are arrays of structured objects containing the corresponding names, identifiers, operations, arguments, and values.
XML	Exactly one <response> root containing one <answer> element.	Inputs appear under <inputs> and steps under <steps> ; references are represented by format-specific elements and attributes.
Markdown	The document begins with # Result and an - Answer: field.	## Inputs and ## Steps contain ordered records with nested fields for values, operations, and arguments.
HTML	Exactly one <main> containing <output id="answer"> .	Inputs and steps are represented under elements identified by inputs and steps , with record values encoded using carrier-specific attributes.
LaTeX	Exactly one response environment containing \Answer{...} .	Inputs and steps are represented by dedicated environments and \Input and \Step macros.
YAML	A root mapping containing answer .	inputs and steps are represented as structured YAML collections.

Appendix

Table 23: Base representation contracts used in Realize and as target contracts in Preserve .

Format	Representative realization
JSON	{"answer": 3521, "inputs": [...], "steps": [...]}
XML	<response><answer>3521</answer> ... </response>
Markdown	# Result; - Answer: 3521; ## Inputs; ## Steps
HTML	<main><output id="answer">3521</output> ... </main>
LaTeX	\begin{response} \Answer{3521} ... \end{response}
YAML	answer: 3521; inputs: ...; steps: ...

Appendix

Table 24: The same Canonical IR rendered in the seven SERIAL-7 representation families. Ellipses abbreviate carrier-specific graph details while preserving the same underlying semantic content.

Figure 13: Serial-7 executable verification pipeline for Realize and Preserve . Representation-specific validators and extractors map model outputs to a shared Canonical IR, after which executable predicates produce machine-checkable compliance verdicts.

Namespace	Atomic checks	Purpose
format.*	clean_boundary , well_formed , native_syntax , root_container , answer_slot , inputs_container , steps_container , escaping	Validate document boundaries, parseability, required slots and containers, native syntax, and escaping under the active representation contract.
format.feature.*	One check per active atomic rule	Validate the sampled atomic representation rule(s) used in Realize .
structure.*	unique_input_names , unique_step_ids , input_fields_present , step_fields_present	Check completeness and uniqueness of extracted input and step records.
semantic.*	answer , input_values , step_consistent	Check final-answer correctness, required input values, and executable graph consistency when applicable.

Appendix

Table 25: Atomic check namespaces used by the executable verifier.

	JSON	XML	Markdown	HTML	L a T e X	YAML	TOML
Answer-only	4	5	5	6	5	5	4
Graph-bearing	6	7	7	8	7	7	6

Appendix

Table 26: Nominal active format.* checks before rule-aware substitution.

Component	Normalization / scoring rule
Numeric values	Integer gold values require exact equality; non-integers use relative tolerance $10^{-6}$ and absolute tolerance $10^{-9}$ unless overridden. Representation-type errors are charged to format.* .
Text values	Case-fold, trim and collapse whitespace, and remove trailing sentence punctuation where the corresponding semantic field is evaluated by normalized text equality. Identifiers and references used by the preservation predicate remain part of the Canonical IR and are compared source-to-target.
Realize input semantics	Extracted inputs are matched to required gold inputs by value rather than by arbitrary gold identifier. Exact reproduction of gold input names is therefore not required for Realize semantic correctness.
Realize graph consistency	When a graph-bearing output can be recovered, execute the model’s own graph rather than requiring step-by-step equality with the gold decomposition. References must resolve, step values must execute correctly, and the final step must agree with the model’s answer. This predicate is a diagnostic semantic check and is not part of Realize HSR.
Preserve input preservation	The ordered sequence of input identifiers and corresponding values extracted from the target must equal that of the instantiated source artifact. A target that preserves only the values while changing, omitting, or reordering the required identifiers does not satisfy the preservation predicate.
Preserve step preservation	For graph-bearing artifacts, the ordered source and target step records must agree in their step identifiers, operators, argument references, and values. Missing, altered, or reordered required step content causes the preservation predicate to fail.

Appendix

Table 27: Representation-independent normalization and scoring rules.

Structured Output Generation

Structured output generation studies how language models produce machine-readable, schema-compliant responses without sacrificing task accuracy.

See all 66 papers

P $^{3}$ : Joint Program-and-Proof Planning for Verified Code Generation
Aug 10, 2026Zenan Li, Ziran Yang, Peiyang Song +2Code Generation Formal Verification
1Apodex · 2Princeton University · 3Caltech +1
VeriContest: A Competitive-Programming Benchmark for Verifiable Code Generation
May 8, 2026Zichen Xie, Mrigank Pawagi, Yuxin Liu +5Code Generation Formal Verification
University of Virginia · 2Indian Institute of Science · 3Rice University +1
AutoPyVerifier: Learning Compact Executable Verifiers for Large Language Model Outputs
Apr 24, 2026Pouya Pezeshkpour, Estevam HruschkaLLM Evaluation LLM Answer Verification
Megagon Labs

Aug 10, 2026J/K move · Enter open · S save

P $^{3}$ : Joint Program-and-Proof Planning for Verified Code Generation

Zenan Li, Ziran Yang, Peiyang Song, Zhaoyu Li+1

1Apodex · 2Princeton University · 3Caltech+1

Code Generation Formal Verification Agentic Code Generation Code Generation Benchmarks Verified Code Generation

Open paper AskPDF arXiv

Verified code generation asks a large language model (LLM) to generate both an executable program and a machine-checkable proof that the program meets a formal specification, promising software that is correct by construction. The de facto workflow decouples the two halves of the problem: first synthesize a program, then attempt to prove it correct. We observe that this sequential pipeline can be both ineffective and inefficient in practice. A program generated without anticipating its proof can be subtly incorrect or structurally difficult to verify, forcing the LLM into brittle repair loops that alternate between patching the code and patching the proof. Inspired by Dijkstra's view that a program and its correctness argument should be developed hand in hand, we propose

P^3

, an LLM-based agentic workflow that first derives a unified program-and-proof plan from the specification, then elaborates the implementation and proof scaffold under this shared plan. To evaluate verified code generation in realistic settings, we further introduce Lean4Commit0, a repository-derived, library-level benchmark built by extracting core APIs from real-world software repositories and translating their requirements, including relational specifications across APIs, into Lean tasks. Using four frontier LLM backends, we evaluate

P^3

on Verina, AlgoVeri, and our Lean4Commit0 benchmark, where it achieves the highest solve rate in every benchmark--model setting. Compared with the stronger baseline, it improves solve rates by 4.6--11.2 percentage points and reduces per-task API cost by up to roughly 40% and wall-clock time by up to roughly 37% on the difficult subset of each benchmark. A targeted ablation further shows gains of 3.3--8.3 points over implementation-only planning, isolating the benefit of planning the program and proof jointly.

Abstract

Structured Output Generation

Explore similar work

P3^{3}3: Joint Program-and-Proof Planning for Verified Code Generation

VeriContest: A Competitive-Programming Benchmark for Verifiable Code Generation

AutoPyVerifier: Learning Compact Executable Verifiers for Large Language Model Outputs

P $^{3}$ : Joint Program-and-Proof Planning for Verified Code Generation