arXiv:2609.14808v1 [physics.comp-ph] 13 Sep 2026
Transformed in Translation: Two-Stage Structural Uncertainty in LLM-Based Scientific Autoformalization Andre Panossian ORCID: 0009-0001-1925-4858
Abstract Scientific autoformalization turns verbal accounts into executable mathematics, but executable code does not settle which model has been constructed. We examine two sources of structural uncertainty: the formalizer that generates a response law, and the recurrence that turns that law into trajectories. In secondary analyses of an openly archived crossed experiment, we studied 320 response maps generated by two pinned language-model formalizers from five engineered cognitive accounts within one sparse quadratic grammar and 16 randomized blocks. With whole blocks held out, source-account identity was recovered at 78.8% accuracy (chance 20.0%) and formalizer identity at 96.3% (chance 50.0%; both p < 0.001). Program size was the stronger single feature family; a pre-specified exploratory comparison found no stable source-account predictive gain from local geometry beyond size. Holding every response map fixed, we then evaluated five recurrence families spanning 33 configurations and 1,013,760 finite-horizon trajectories. Added feedback, projection and leak produced sharply different outcome distributions. The consequential distinction was which comparisons survived: median cross-recurrence rank concordance was 0.73 for endpoint magnitude but 0.05 for settling, among the configuration pairs with defined rankings. Thus a common mathematical language did not erase translation provenance, and robust ordering under one observable did not transfer to another. Scientific autoformalization is usefully studied as model-space construction: the generated ensemble and its dynamical embedding are both part of the specification supporting a scientific claim.
Keywords: scientific autoformalization; LLM-based model construction; structural uncertainty; automated theory translation; dynamical systems; model discrimination
1
Introduction
A theory that says feedback makes a cognitive state persistent has not yet specified what persists, how feedback acts or what happens at a boundary. Those choices become visible when the account is formalized. Variables, scales, equations and update rules turn an explanation into a model that can make quantitative predictions (Farrell and Lewandowsky, 2010; Smaldino, 2020; van Rooij and Blokpoel, 2020; Guest and Martin, 2021). More than one mathematical construction may be compatible with the same verbal account (Muelder and Filatova, 2018); even models with similar predictive performance can remain underspecified in scientifically important ways (D’Amour et al., 2022). The question is not whether modelling involves choices, but which choices change the conclusions one can draw. Language models make repeated formalization practical at a new scale. We use scientific autoformalization for the LLM-mediated construction of executable scientific models from verbal accounts. Cognitive applications already include executable sorting programs conditioned on 1
participants’ strategy reports (Xie et al., 2024), iterative refinement of candidate models against behavioural data in GeCCo (Rmus et al., 2025), and symbolic program search in CogFunSearch (Castro et al., 2025). Related work addresses natural-language physics problems (Kabra et al., 2025) and engineering models (Rupprecht et al., 2025). These systems make it possible to construct and compare many mathematical hypotheses rather than formalize only one by hand. Three neighbouring literatures help frame the resulting uncertainty. Autoformalization research evaluates validity, symbolic equivalence and semantic consistency (Wu et al., 2022; Li et al., 2024; Mo et al., 2026). Grammar-based uncertainty measures assess when generated formal programs are likely to be wrong (Ganguly et al., 2025). Code-attribution research detects signatures of the generating language model (Bisztray et al., 2025). Our question is complementary: when all candidates use one restricted mathematical language, does the formalizer still leave a recoverable signature in the structure and responses of the scientific models themselves? A shared grammar controls which equations are permitted, not which of them will be chosen. A formalizer can select different variables, interactions or levels of mathematical complexity while satisfying exactly the same syntactic contract. GeCCo’s reported base-model differences in selectedmodel performance already show that generator choice can matter (Rmus et al., 2025). Here we examine that dependence before selection against observations: which source-account and formalizer identities can be recovered from independently generated mathematics, and how much of that signal is carried by program size? For long-run claims, a second choice is equally important. A response law says what a model emits at a given state; a recurrence says how that response changes the next state. Feedback, timing, damping, noise and boundaries enter at this stage. A program that produces large responses need not be the program that settles most reliably once those assumptions change. This gives two experimentally separable sources of structural uncertainty (Draper, 1995; Kennedy and O’Hagan, 2001): construction of the response-map ensemble, and construction of its dynamical embedding. We make that space explicit. Let T denote a source account, F a formalizer, G a mathematical grammar and P the translation protocol. Automated formalization is represented not as a deterministic function but as a conditional model generator, M ∼ Q(M | T, F, G, P ),
(1)
where M is an executable response map and Q denotes the protocol-conditioned generation distribution, not a posterior over scientifically correct theories. Recovering source identity from M tests whether the ensemble retains source-dependent information; recovering formalizer identity tests whether the translation system also leaves a mathematical signature. Neither recovery task substitutes for a fidelity assessment against the source theory. The formalization channel determines which response map enters the analysis. It does not yet determine a trajectory. If rM (x, a) is the response emitted by program M , state evolution exists only after a recurrence is supplied, xt+1 = Φ(xt , at , rM (xt , at ), ξt ) .
(2)
In computational-physics terms, rM acts like a local constitutive response, whereas Φ supplies the evolution rule and boundary treatment. An autoformalizer could generate both together; here they are separated by experimental design. The shared grammar contains response maps but no recurrence, so variation introduced during translation can be distinguished from the dynamical assumptions supplied afterwards. We conduct two linked secondary analyses of the openly archived SPECFORM corpus (Panossian, 2026a). Five engineered, literature-inspired cognitive accounts were crossed with two pinned 2
formalizers, two presentation-format arms and 16 randomized blocks, yielding 320 response maps. First, held-out phenotyping tests recoverable provenance and the incremental predictive contribution of local geometry beyond size. Second, all maps are held fixed while recurrences vary, testing the robustness of finite-horizon outcomes and program rankings. The cognitive accounts provide a controlled test domain; the scientific target is the chain from verbal theory to executable hypotheses and from those hypotheses to comparative dynamical claims. WHAT AUTOMATED FORMALIZATION ALREADY DOES
GENERATE
CHECK
ATTRIBUTE
SCIENTIFIC GAP
multiple formal candidates
validity and consistency
which model wrote it
Does the formalizer help determine the mathematical hypothesis science will test?
1 FORMALIZE
same theory + shared grammar; translation repeated
VERBAL THEORY 5 mechanism accounts 16 randomized blocks
FORMALIZER
FA
FB
RESPONSE-MAP ENSEMBLE
FINGERPRINT TEST
∼ Q( ∣ T, F, G, P)
Can account and formalizer be recovered?
n = 320 programs
2 pinned models
held-out blocks
hold every response map fixed
2 MAKE DYNAMICAL
the response map contains no native update rule
IMPOSE A RECURRENCE Φ
ONE-STEP MAP
rM(z) state + action → response not a trajectory
FINITE-HORIZON DYNAMICAL OUTCOMES
Immediate
xt + 1 = xt + h rM(xt)
Projected
xt + 1 = Π[xt + h rM(xt)]
schematic · not data
xt + 1 = xt + h rM(xt) − λ(xt − x0) Leaky 5 families · 33 configurations · 600 updates
escape
boundary pinning
convergence
Which outcomes—and which rankings—survive the recurrence Φ?
Figure 1. Two stages of scientific model construction. Five controlled accounts were repeatedly translated by two pinned formalizers under a shared grammar, yielding 320 response maps. Held-out phenotyping tests which source and formalizer signatures remain in those maps. In the second stage, every map is held fixed while five declared recurrence families generate 33 dynamical configurations. Comparing outcomes and rankings across those configurations tests which conclusions survive the additional assumptions. State-space glyphs are qualitative schematics, not empirical trajectory projections.
2
Results
2.1
Automated formalization produces a structured model ensemble
Each generated program mapped a current state and proposed action to 11 response coordinates. All programs used the same vocabulary of 40 features and the same sparse quadratic grammar, which
3
admitted 823 linear and quadratic monomials and at most 6 active terms per response coordinate. This common grammar held programming language and permitted monomials fixed, substantially restricting surface variation while preserving genuine choices about which variables and interactions enter the equations. For program Mi , we measured a local mathematical phenotype Zi = ψ(Mi ) = (Si , Gi ) ,
(3)
where Si ∈ R15 summarizes program size and occupancy, and Gi ∈ R221 summarizes responses, derivatives and local spectral structure over 120 fixed contexts. Identity fields, provenance labels, constants and exact linear dependencies were excluded. The retained phenotype contained 236 columns. The phenotype measures the generated mathematical objects, rather than free-form code style. Its size and response-derived components let us ask whether provenance is carried by the amount of structure, by its local behaviour, or by their combination.
2.2
Source and formalizer leave recoverable signatures
The source account was recovered from held-out programs at 78.8% accuracy against 20.0% chance (p < 0.001 under design-respecting label permutations; Fig. 2a). Local geometry alone reached 73.4%, and program size alone reached 75.6%. At the matched-pair unit, account accuracy was 80.0%. Errors were distributed across the five classes rather than arising from the failure of one account alone (Fig. 2b). Formalizer identity was recovered at 96.3% against 50.0% chance (p < 0.001). Local geometry alone reached 93.8%, program size alone 94.7%, and all 32 block-by-formalizer units were classified correctly. The two prediction tasks have different class counts, so their absolute accuracies are not directly comparable effect sizes. A third target, wording identity (R1/R2), was weakly recoverable at 55.0% and did not improve on its size-only baseline. R1/R2 denotes the scheduled wording variants, not the narrative-versus-causal-invariants format arms; the latter were not classifier targets (Supplementary Section S1). The formalizer left a detectable signature in held-out mathematics after source account and grammar were controlled. The predictive signal is multivariate. In a separate whole-corpus decomposition, source account, formalizer and block explained mean shares of 7.6%, 6.9% and 4.4% across local-geometry features; 81.2% remained residual. High classification accuracy can therefore coexist with small, coordinated shifts across many features.
2.3
Size carries a strong signature; geometry adds no stable predictive gain
Program size alone recovered both source and formalizer more accurately than local geometry alone (Fig. 2a). Much of the easiest-to-recover structure therefore concerns how much mathematical machinery a translation uses: occupied coefficients, active terms and related size summaries. These quantities are properties of the compiled equations, not whitespace or prose length. Representational economy is part of the generated model distribution. We then asked whether local geometry provided stable source-account predictive information beyond size. Starting from the established feature sets, a size-only classifier and a size-plus-geometry classifier were fit on identical grouped folds, with fitting transformations and regularization selected inside the training data. For held-out observation i, the primary paired contrast was di = ℓ(pbS , yi ) − ℓ(pbS+G , yi ) , 4
(4)
Held-out provenance recovery
b
78.8% 75.6% 73.4%
chance 20%
chance 50%
55.0% 57.8% 57.8%
Wording identity (R1/R2)
Circular
51
1
2
7
3
Comparator
3
45
3
1
12
Threshold
4
3
52
2
3
Precision
3
3
3
53
2
Source
1
9
1
2
51
ar ul
r to
ld ho
n sio ci
40
40
60
80
100
Held-out accuracy (%) All features
Program size
30 20 10 0
chance 50%
20
60 50
96.3% 94.7% 93.8%
Formalizer
Account confusion matrix
Programs
Source account
Source account
a
Local geometry
rc Ci
m Co
pa
ra
Th
s re
e Pr
ce ur So
Predicted account
Figure 2. Source account and formalizer identity are recoverable from held-out mathematics. a, Accuracy using all retained features, program size alone and local geometry alone. The third target is wording identity R1/R2, not presentation-format arm. Grey vertical marks denote target-specific chance rates; numbers are percentages. b, Source-account confusion matrix for the all-feature classifier. Whole randomized blocks were held out from fitting.
so positive values favour the addition of geometry. Differences were aggregated to the 16 randomized blocks before inference. The primary log-loss contrast was -0.019 (exploratory 95% block t-interval -0.150 to 0.111); 9 of 16 blocks favoured size plus geometry and the exhaustive block-sign calibration was 0.754 (Fig. 3a). Accuracy moved in the opposite direction. Row accuracy rose from 75.3% to 80.6%, with a block-mean contrast of +0.053 (interval -0.003 to 0.109; calibration 0.081; Fig. 3b). Only 8 blocks favoured the larger model, and fold-level directions were inconsistent. These nested fits differ from the fixed-estimator provenance analysis above; the two sets of accuracy figures describe different fitted procedures. On average, adding geometry improved class decisions while worsening probability assignment to the observed class. None of the four pre-specified primary conditions for an incrementalutility statement held. A dimension-reduced geometry control also failed to yield a stable gain (Supplementary Section S5). Geometry alone contains account information, but this comparison does not establish a reliable additional benefit beyond size for source-account prediction on this corpus.
2.4
Recurrence changes finite-horizon outcomes
The provenance analyses establish variation over response maps before state evolution is imposed. We next fixed those maps and varied only the rule that turns them into trajectories. The generated programs contain no native state-update rule, so a dynamical interpretation requires an additional construction. Five recurrence families varied immediate feedback, frozen action, delayed feedback, leak, noise and projection. Step, leak and boundary choices produced 33 configurations, each evaluated for 600 updates on the same programs, contexts and initial-state bank. The step parameter multiplies response strength; varying it changes the recurrence gain at a fixed number of updates. This is a sensitivity experiment over dynamical specifications, not a solver-convergence test at a common physical duration. 5
Primary · held-out log-loss
a
Outer fold 1 Outer fold 2 Outer fold 3 Outer fold 4 Overall
D = -0.019 [-0.150, +0.111] 9/16 blocks; 1/4 folds share sign · calibration 0.754
−0.4
−0.3
−0.2
−0.1
0.0
0.1
0.2
0.3
paired block contrast (positive favours size + geometry)
Secondary · held-out accuracy
b
Outer fold 1 Outer fold 2 Outer fold 3 Outer fold 4 Overall
D = +0.053 [-0.003, +0.109] 8/16 blocks; 3/4 folds share sign · calibration 0.081
−0.10 ● blocks
−0.05
◇ fold means
0.00
0.05
0.10
0.15
0.20
paired block contrast (positive favours size + geometry)
◆ overall mean + interval
|
metrics disagree; pre-specified utility rule not met
Figure 3. The predictive contribution of local geometry is metric- and fold-dependent. Each coloured dot is a randomized-block mean, grouped by the outer fold whose fitted model generated it; open diamonds are fold means and black diamonds show overall means with exploratory 16-block t-intervals. Positive values favour size plus geometry. Log-loss was primary. The metrics disagree in sign, both displayed intervals include zero and the pre-specified four-condition rule is not met. Supplementary Section S5 reports bootstrap and dimension-reduction sensitivity.
After substituting a deterministic action rule C, let gM,C (x) denote the eight-dimensional state response induced by map M . Three representative constructions expose what the analyst adds: unb FM,C,h (x) = x + h gM,C (x), proj FM,C,h (x) = ΠG [x + h gM,C (x)] ,
(5)
leak FM,h,λ (x; x0 ) = x + h gM,mirror (x) − λ(x − x0 ),
where ΠG projects into the declared guard set. Delayed feedback instead augments the state to (xt , xt−1 ), and bounded stochastic feedback defines a transition kernel rather than a deterministic phase portrait. The fixed-point conditions already separate the mechanisms: the unbounded map requires gM,C (x⋆ ) = 0; the projected map may satisfy x⋆ = ΠG [x⋆ + hgM,C (x⋆ )] while gM,C (x⋆ ) ̸= 0; and the leaky map requires h x⋆ = x0 + gM,mirror (x⋆ ). (6) λ The last equation is indexed by the run-specific anchor x0 : leak does not uncover one equilibrium equation belonging to the response map. 6
Across 1,013,760 finite-horizon trajectory evaluations, operational outcomes changed sharply while the compiled response maps remained fixed (Fig. 4). Under immediate unbounded feedback, increasing the step parameter from 0.25 to 1 raised the escape fraction from 56.2% to 90.7%. Under the same feedback with projection, boundary pinning rose from 29.9% to 69.4%. Among configurations with pinning, the smallest median response norm at a pinned endpoint was 0.058. Stationarity of the projected process can therefore coexist with a nonzero response. The boundary treatment is part of the mechanism producing the plateau, not evidence of an intrinsic equilibrium of the response map. Leak changed the fixed-point equation in a different way. Across the declared grid, h/λ ranged from 1.25 to 20, while the median response-induced displacement ranged from 5.9% to 140.3% of the initial-state spread. Operational convergence ranged from 40.7% to 100.0%, and escape reached 26.6%. Stable-looking behaviour under leak was therefore jointly determined by the generated response law, the analyst-selected ratio h/λ and the run-specific anchor x0 ; it was not a property of the response map alone. Recurrence changes finite-horizon dynamical outcomes
same response maps · same initial-state bank · horizon 600
a
b
UNBOUNDED IMMEDIATE
xt + 1 = xt + h rM(xt)
xt + 1 = Π[xt + h rM(xt)]
h = 0.25
LEAKY IMMEDIATE
xt + 1 = xt + h rM(xt) − λ(xt − x0)
h = 0.25
56%
schematic not data
c
PROJECTED IMMEDIATE
λ = 0.05 55%
schematic not data
h=1
98%
schematic not data
h=1
91%
λ = 0.20
69%
escape under unbounded extrapolation
100%
pinning can occur with rM(x) ≠ 0
Escaped
Converged
Boundary-pinned
fixed points satisfy hrM(x) = λ(x − x0)
Contracting
Drifting
Figure 4. Recurrence changes the finite-horizon outcome distribution. The same response-map ensemble and initial-state bank were evaluated for 600 updates. Exact recurrence forms are paired with qualitative two-dimensional schematics and empirical aggregate outcome bars for six illustrative configurations. The schematics are not trajectory projections. Unbounded immediate feedback promotes escape as step size rises; projection can pin a state without gM,C (x) = 0; leak changes the fixed-point equation to hgM,mirror (x) = λ(x − x0 ). (O)
To ask what nevertheless survives recurrence, let Yik denote observable O for program i under recurrence configuration k. For each observable we computed
(O)
(O)
320 ρO (k, k ′ ) = corrS {Yik }320 i=1 , {Yik′ }i=1 ,
(7)
the Spearman correlation between program rankings under two configurations. The rank-concordance summaries differed markedly by observable (Fig. 5). Endpoint magnitude had median ρ = 0.73 across all 528 configuration pairs, with 38.1% above 0.8. Median concordance 7
was 0.58 for escape, 0.38 for guard contact and 0.05 for settling. These latter medians use 66, 325 and 253 pairs, respectively: constant rankings make some correlations undefined. The comparison is therefore descriptive and conditional on each observable’s usable pairs. Cycle fraction was zero under the finite-horizon detector in every configuration, leaving no ranking to correlate. With the initial-state bank held fixed across configurations, the experiment tests whether comparisons between formalizations survive changes in dynamical assumptions. Endpoint-based and settling-based comparisons give different answers. Rank concordance therefore depends on both the recurrence set and the observable. Rank order depends on recurrence and on the observable
a
Full range and median
b High-concordance fraction 0.73
Endpoint magnitude
38.1% · n=528
0.58
Escape fraction
28.8% · n=66
0.38
Guard contact
10.8% · n=325
0.05
Settling −0.50 −0.25
0.00
0.25
5.9% · n=253
0.50
0.75
Spearman rank correlation, ρ
1.00
0
10
20
30
40
50
usable pairs above ρ > 0.8 (%) Observable-specific denominators reflect ties and undefined ranks.
Figure 5. Rank order depends on recurrence and observable. a, Median (coloured point) and full range (line) of cross-configuration Spearman rank correlations; the dashed line marks ρ = 0.8. b, Fraction of usable configuration pairs above that threshold, with the observable-specific denominator shown. A constant ranking makes its correlations undefined and removes those configuration pairs; ordinary ties do not by themselves make a correlation undefined.
3
Discussion
The controlled ensemble reveals two distinct contributions to a scientific model. Source account and formalizer left signatures that generalized across held-out blocks, even under a common restricted grammar. Once the maps were embedded in recurrences, the robustness of program rankings depended on what was measured. These results locate uncertainty both in the construction of candidate mathematics and in the assumptions connecting that mathematics to a long-run claim. The first finding complements data-driven model discovery. A selected program can predict observations well while retaining structural choices traceable to its generator. The present design measures that dependence before selection against data, rather than treating predictive performance as a proxy for structural invariance. It motivates comparing generated ensembles, not only selected winners, and recording the formalizer snapshot and translation protocol as part of model provenance. Size is an important part of that provenance. Accounts and formalizers were more recoverable from occupied mathematical structure than from the present geometry summaries alone, and the nested comparison did not establish a stable incremental contribution from geometry. This makes complexity budget a concrete experimental variable. Prospectively matching the number of active 8
terms would test whether formalizer signatures persist when the amount of mathematical machinery is held fixed; the current data do not answer that question. The second finding connects autoformalization to a familiar concern in complexity science. Update schedules can change emergent behaviour while local rules are retained (Huberman and Glance, 1993; Schönfisch and de Roos, 1999), and projected systems have boundary-dependent stationary conditions (Nagurney et al., 1995). Our recurrence analysis asks a more specific comparative question: which orderings of a generated model ensemble survive a declared set of those choices? Endpoint magnitude and settling give very different robustness summaries. A ranking that is useful for one question is not automatically useful for another. This distinction can be written as a chain of mathematical objects, Mi ∼ Q( · | T, F, G, P ), (i,k) Xt+1 ∼ KMi ,Φk (O)
Yik
(i,k)
= O X0:H
(i,k)
· | Xt
,
(8)
,
where X includes any augmented state required by the recurrence and is initialized from the declared initial-state design. The kernel K is a point mass for deterministic recurrences and a transition kernel for stochastic feedback. The response map M , evolution rule Φ, initial-state design, horizon H and observable O jointly specify the reported quantity. This is a practical reporting structure: it identifies which modelling commitment must be supplied before a proposed conclusion can be evaluated. The next scientific step is to connect such ensembles to discriminating observations. Sourcefidelity review should first establish which candidate formalizations are defensible interpretations of the account. One can then freeze the candidates and dynamical assumptions, choose interventions on which their predictions differ, and test those predictions on untouched evidence. Optimal experimental design provides the logic (Myung and Pitt, 2009). Such a test would turn measured formalization uncertainty into an empirically constrained model space. Computational psychiatry is a useful domain for this programme because it seeks mechanistic links among cognitive theory, formal models and behaviour (Huys et al., 2016). The engineered accounts used here provide controlled inputs, not patient models. The contribution is to scientific formalization more broadly: provenance can remain in executable mathematics, and claims about its dynamics require an explicit, testable embedding.
3.1
Scope and limitations
The five engineered accounts, two pinned formalizers and narrow quadratic grammar define the population studied. The results do not establish source fidelity, a prevalence of underspecification across scientific theories, or superiority of either formalizer. The high-dimensional geometry comparison cannot distinguish absent incremental information from limited estimation power; its intervals and sign calibration are exploratory because held-out blocks share fitted models. Recurrence results concern the declared configurations, initial-state bank, finite horizon and operational detectors. They are neither global attractor classifications nor numerical-convergence results, and rank summaries condition on observable-specific usable pairs. The supplementary distance bridge is exploratory and stage-specific.
9
3.2
Conclusion
Automating formalization does not remove model construction; it makes that construction repeatable and measurable. Here, source account and formalizer remained recoverable from held-out mathematics, while alternative recurrences changed which comparisons among the same maps were robust. A useful scientific record therefore describes not just a generated equation, but the ensemble that produced it and the dynamical assumptions under which its predictions are made.
4
Methods
4.1
Source experiment and corpus
The 320-program corpus was produced by SPECFORM, a preregistered randomized experiment in theory-to-program translation, and released with its stage-specific response tensors (Panossian, 2026a). The source experiment’s registered renderer-format hypotheses—SPECFORM-H1, SPECFORM-H2 and their conjunction—were not supported. The present paper reports distinct secondary analyses of the shared corpus. Five anonymous cognitive accounts were represented in two registered presentation-format arms—narrative and causal invariants—and translated by two OpenAI model snapshots, gpt-4. 1-2025-04-14 and gpt-5.4-2026-03-05, across 16 randomized blocks. Calls used temperature 1.0, top-p = 1.0, zero frequency and presence penalties, and medium output verbosity. Each request was independent and stateless and exposed only one account. The complete factorial design contained 5 accounts × 2 formalizers × 2 format arms × 16 blocks = 320 programs.
(9)
The accounts were designed to express circular inference, comparator processing, threshold decisions, precision weighting and source monitoring. They serve as controlled mechanism families, not canonical implementations of their literatures. Separately recorded R1/R2 wording variants were allocated by block and formalizer. The supplementary design table distinguishes these wording identities from the two format arms; only R1/R2 was used as a wording-classification target in the present analysis.
4.2
Shared mathematical grammar
Every program specified 11 response coordinates as sparse polynomials of degree at most two over 40 named features. For output j, rM,j (z) = βj0 +
X
βju zu +
u
X
βjuv zu zv ,
(10)
u≤v
with at most 6 active non-constant terms. The grammar contained 823 legal monomials. Compilation combined duplicate terms and removed exact cancellations deterministically. Recurrence, delays, stochastic terms, arbitrary code and transcendental functions were excluded from the language. The reference compiler, canonical feature construction, probe definitions and evaluator were taken from the archived SPECFORM version 1.0.0 software release (Panossian, 2026b).
4.3
Local phenotype
Compiled maps were evaluated over 120 fixed contexts. The phenotype contained coefficient occupancy, response summaries, analytic Jacobian summaries and context-aggregated spectral 10
quantities. Analytic derivatives were checked by finite differences. Provenance fields, class labels, constants and exact linear dependencies were removed before prediction, leaving 221 geometry features and 15 size features.
4.4
Grouped provenance recovery
Four outer folds held out every block whose index shared the same remainder modulo four. Consequently no sample, matched pair or randomized block crossed a train–test boundary. Scaling and regularized multinomial logistic regression were fit on training rows only. The same estimator was used for every target and feature family. Accuracy was evaluated on concatenated out-of-fold predictions and on the target-specific grouped unit: matched pairs for source account and blockby-formalizer cells for formalizer identity. Null distributions used 1,000 design-respecting label permutations and the finite-draw correction.
4.5
Conditional geometry comparison
The size-only and size-plus-geometry classifiers used identical outer folds and the established corpuslevel feature sets. Training-constant-column removal, scaling, dimension reduction when used, and regularization were fitted or selected within grouped training folds. Paired out-of-fold differences were aggregated to randomized-block means; log-loss was primary and accuracy secondary. A favourable result required a positive mean, an interval excluding zero, block-sign calibration below 0.05, and directionally consistent fold diagnostics without single-fold dependence. The 65,536 sign assignments were exhaustively enumerated, but not treated as an exact statistical test: blocks sharing a fitted outer-fold model are not jointly exchangeable. Intervals and calibration are exploratory; nominal interval coverage is not claimed. Supplementary Section S5 reports the sensitivity analyses.
4.6
Recurrence sensitivity
Five declared recurrence families implemented immediate state feedback, frozen action, one-stepdelayed feedback, leaky feedback and bounded stochastic feedback. Step size, leak rate and projection choices generated 33 configurations. Each was evaluated for 600 updates on the same 320 programs, eight evidence contexts and 12 initial states per context. Outcomes were classified as escaped, converged, boundary-pinned, contracting, drifting or cyclic under fixed operational rules. For each scalar program summary, Eq. 7 was evaluated over all configuration pairs for which both rankings varied.
4.7
Exploratory distance bridge
The bridge used the deposit’s two stage-specific response products: SPECFORM-H1 atomic finitedifference tensors and SPECFORM-H2 mixed-interaction tensors (Panossian, 2026a). They share the same 320 programs and were analysed separately, without pooling or a SPECFORM-H1versus-SPECFORM-H2 contrast. Each tensor set was reduced to one-step response matrices for each program. Pairwise Euclidean distances were computed separately for each response stage. Their alignment with distances in the local phenotype and concatenated recurrence summaries was measured by the squared descriptive correlation between vectorized distance matrices (Supplementary Section S7). This distance bridge was not part of the SPECFORM preregistration and is treated as an exploratory secondary analysis; SPECFORM-H1 and SPECFORM-H2 remain separate registered stages.
11
Data and code availability The source programs, provenance records and SPECFORM-H1 single-input and SPECFORM-H2 interaction-response tensors are openly archived under CC BY 4.0 on Zenodo (version 1.0.0; https: //doi.org/10.5281/zenodo.21876518). The reference implementation is archived separately under the MIT License (version 1.0.0; https://doi.org/10.5281/zenodo.21879576). The present analyses were generated from machine-readable aggregate result objects using deterministic scripts. The versioned publication package contains the derived features and result objects, LaTeX source, result macros, vector figures and the scripts that regenerate every table and plot. The analysis inputs, source snapshots and verification script accompany the manuscript as ancillary material.
Use of generative AI tools Claude Code and OpenAI Codex assisted with implementation, debugging, evidence review and manuscript preparation.
Scope of the data The study analyses generated programs and simulated numerical trajectories; it contains no humanparticipant or patient data.
12
Supplementary Information S1
Factorial design and experimental unit
The formalization ensemble is the shared generation corpus released with the SPECFORM-H1 and SPECFORM-H2 datasets, version 1.0.0 (Panossian, 2026a). It was constructed as a randomized factorial experiment in which five anonymous mechanism accounts were crossed with two pinned language-model formalizers and two registered presentation-format arms across 16 randomized blocks: 16 × 5 × 2 × 2 = 320 programs. (S1) Each request was independent and stateless. The formalizer saw one account at a time and did not see competing accounts, target equations, later numerical evidence or other generation calls. Table S1. Factors in the source SPECFORM formalization experiment.
Factor
Levels
Experimental role
Source account
Circular inference, comparator processing, decision threshold, precision weighting, source monitoring gpt-4.1-2025-04-14; gpt-5.4-2026-03-05 Narrative; causal invariants (intervention contract)
Controlled theoretical content
Formalizer Format arm Wording identity
R1; R2, scheduled within the factorial design
Randomized block
16 blocks
Translation system Presentation format; not a provenance-classifier target Wording-classifier target; not an additional crossed factor Holdout and randomization unit
The semantic registry records format arm as arm and R1/R2 wording identity as rendering. The latter is constant within a block-by-formalizer cell, with its allocation across the two formalizers following the four balanced schedules R1/R1, R2/R2, R1/R2 and R2/R1. Wording is therefore not globally equivalent to formalizer, but there is no within-cell R1/R2 contrast. Each of the 160 matched pairs shares account, formalizer and wording identity while containing one request from each format arm; the requests are distinct and stateless. The 55% wording-classification result does not estimate the narrative-versus-causal-invariants arm effect. The accounts are literature-inspired scientific test cases, not canonical mathematical implementations or a representative sample of computational psychiatry. Generation used temperature 1.0, top-p = 1.0, zero frequency and presence penalties, and medium output verbosity.
S2
Mathematical representation
Every generated object contained 11 response coordinates over 40 fixed feature names. Legal expressions were sparse polynomials of degree at most two. The grammar admitted 823 linear and quadratic monomials and at most 6 active terms per coordinate. Compilation, canonical feature construction and reference evaluation used the archived SPECFORM version 1.0.0 implementation
13
(Panossian, 2026b). For response coordinate j, rj (z) = βj0 +
X
βju zu +
u
X
βjuv zu zv .
(S2)
u≤v
Duplicate terms were combined and exact cancellations removed during deterministic compilation. The language was selected for analytic tractability and controlled comparison. It excludes recurrence, arbitrary code, variable denominators, transcendental functions, piecewise operators, delays and stochastic terms.
S3
Local phenotype construction
Each compiled response map was evaluated over 120 fixed contexts. The local phenotype included coefficient occupancy, response summaries, analytic Jacobian summaries and context-aggregated spectral quantities. Analytic derivatives were checked against finite differences. Identity fields, provenance labels, constants and exact linear dependencies were removed before modelling. The final matrix contained 236 predictors: 221 local-geometry variables and 15 program-size variables. The feature sets were disjoint as columns. They were not assumed to carry independent information.
S4
Grouped provenance recovery
Four outer folds held out complete randomized blocks. Every program appeared in test data once, and no sample, matched pair or randomized block crossed a train–test boundary. Scaling was fit on training data. All targets and feature families used the same regularized logistic classifier. Label permutations preserved the relevant design units and used 1,000 draws. Table S2. Held-out classification accuracy.
Target
Chance
All features
Local geometry
Program size
Source account Formalizer Wording identity (R1/R2)
20.0% 50.0% 50.0%
78.8% 96.3% 55.0%
73.4% 93.8% 57.8%
75.6% 94.7% 57.8%
The source-account and formalizer results reached the finite-draw permutation floor, p = 1/1001 < 0.001. Account accuracy at the matched-pair unit was 80.0%. Formalizer accuracy at the block-byformalizer unit was 100.0%.
S4.1
Descriptive feature variance
For each geometry feature, sum-of-squares shares were calculated for source account, formalizer, block and residual terms on the full corpus. Mean shares were 7.6%, 6.9%, 4.4% and 81.2%, respectively. This decomposition is descriptive and does not replace grouped predictive evaluation. Its purpose is to show that the recoverable signature consists of coordinated multivariate shifts rather than wholesale variance explanation.
14
S5
Conditional comparison of geometry and size
The comparison targeted source-account classification. The size-only and size-plus-geometry models were evaluated on identical outer folds, using the feature sets established by the earlier corpus-level screen. Training-constant-column removal, scaling and hyperparameter selection used grouped training folds; the dimension-reduced control additionally selected its PCA dimension there. The primary outcome was paired held-out log-loss; accuracy was secondary. Observation-level differences were aggregated to the 16 randomized blocks. Table S3. Pre-specified predictive comparison. Positive contrasts favour size plus geometry. Intervals are exploratory block t-intervals. The sign quantity is exhaustive calibration, not an exact statistical test, because blocks sharing an outer fold share fitted models.
Metric
Mean
95% interval
Favouring larger model
Calibration
Log-loss Accuracy
-0.019 +0.053
[-0.150, 0.111] [-0.003, 0.109]
9/16 8/16
0.754 0.081
Decision Gain not established Gain not established
Accuracy rose from 75.3% to 80.6%, while the primary log-loss contrast was negative. A favourable interpretation required a positive mean, an interval excluding zero, calibration below 0.05, and directionally consistent fold diagnostics without single-fold dependence. Neither metric met the joint rule. The nested fitted procedures differ from the fixed-estimator provenance classifiers, accounting for the different accuracy figures in Sections S4 and S5. The log-loss fold means were +0.1023, +0.0867, −0.2896 and +0.0233. Omitting the third fold reversed the overall sign to +0.0708. A 10,000-draw block bootstrap gave a primary interval of [−0.1371, 0.0950]. Its secondary accuracy interval, [0.0031, 0.1031], excluded zero although the corresponding t-interval did not. This sensitivity does not satisfy the joint rule or overturn the negative primary result. No significance test was attached to the four fold means. The dimension-reduced geometry control gave a log-loss difference of −0.0037 (block t-interval [−0.0430, 0.0355]; sign calibration 0.849) and an accuracy difference of −0.00625. Thus neither the unreduced comparison nor the declared reduced control established a stable incremental gain. All interval summaries remain exploratory, without a claim of nominal coverage under shared-training dependence.
S6
Declared recurrence families
The response maps did not specify state evolution. Five recurrence families were used as explicit analytical probes. They hold the response map and initial-state bank fixed while changing feedback, timing, damping, noise or boundaries. Step, leak-rate and boundary settings yielded 33 configurations. Each was evaluated for 600 updates on the same programs, eight contexts and 12 initial states per context. The step parameter also scales response strength; physical duration was not held fixed across its values. The grid therefore compares declared recurrence constructions rather than approximations to one continuous-time evolution law.
15
Table S4. Recurrence families and the assumptions they introduce. Family
Evolution rule in words
Immediate feedback Frozen action
Proposed action mirrors the Deterministic map on the current state eight-dimensional state chart Proposed action remains at its Deterministic map on the initial value eight-dimensional state chart Proposed action mirrors the Deterministic companion map on previous state (xt , xt−1 ) ∈ R16 Immediate feedback plus Anchor-indexed deterministic map; restoration toward the initial state equivalently an augmented system with frozen x0 Noisy feedback followed by Constrained random map / Markov projection into the reference guard transition kernel
Delayed feedback Leaky feedback
Bounded stochastic feedback
Dynamical construction
Assumption isolated Direct endogenous feedback No endogenous action feedback One-step timing lag Added damping and a run-specific anchor Noise and hard boundaries
Table S5. Cross-configuration robustness of program rankings. Each row summarizes its own usable subset of the 528 configuration pairs; a constant ranking makes a correlation undefined.
Long-run observable
Median Spearman ρ
Pairs with ρ > 0.8
Usable pairs
Endpoint magnitude Escape fraction Guard contact Settling
0.73 0.58 0.38 0.05
38.1% 28.8% 10.8% 5.9%
528 66 325 253
Under immediate unbounded feedback, escape rose from 56.2% to 90.7% between step sizes 0.25 and 1. With projection, boundary pinning rose from 29.9% to 69.4%. Under the two low-step leaky configurations highlighted in the article, convergence was 97.9% and 100.0%. Cycle fraction was zero under every declared configuration and detector, so no cycle ranking exists.
S7
Exploratory local-to-long-run bridge
The atomic and mixed-interaction response tensors were taken from the deposited SPECFORM-H1 and SPECFORM-H2 stages, respectively (Panossian, 2026a). The stages were analysed separately; no pooled or between-stage estimand was formed. For each response stage, pairwise distances in heldout one-step response matrices were compared with pairwise distances in the local phenotype and recurrence-summary spaces. For response stage s and representation R, the descriptive alignment was As,R = corr2 vec ∆(s) (S3) response , vec ∆R , where ∆ is a pairwise distance matrix. Response stages were not pooled. Because matrix entries share programs and are dependent, As,R is a squared descriptive correlation rather than a variance decomposition. The distance bridge was not part of the SPECFORM preregistration. Both rows are therefore exploratory secondary analyses; SPECFORM-H1 and SPECFORM-H2 remain separate registered stages, and the recurrence summary is not interpreted as a native dynamics. The differing descriptive alignments caution against assuming a single monotone relationship: a representation aligned with one-step evidence in one response regime need not remain aligned after recurrence. 16
Table S6. Squared descriptive correlations between pairwise-distance matrices in the exploratory bridge.
Response stage
Local phenotype
Recurrence summary
29.4% 0.01%
1.1% 1.0%
SPECFORM-H1 atomic response SPECFORM-H2 interaction response
Repaired H2 evidence and historical machine labels. The programs and both response products bind the same attempt-4 manifest. The source record retains a timestamp-verification failure affecting three H2 samples and the subsequent disclosed repair. All 1,280 response tensors match their sidecar digests; the three repaired samples match the repair record byte-for-byte. The H2 data are usable. Historical machine fields still label H2 INVALID and DISCLOSED_POST_HOC, and retain an invalid joint field, whereas the approved scientific interpretation reports the H1, H2 and joint hypotheses as NOT_SUPPORTED. The ancillary bridge report preserves and explains both records rather than silently replacing either. This repair history does not pool the atomic and interaction stages, and neither source-stage registration makes the new distance bridge confirmatory. Evidence alignment changes across response stages
a
Atomic responses
10−4
10−3
b
Interaction responses
local fingerprint
local fingerprint
29.4%
0.01%
1.1%
1.0%
recurrence summary
recurrence summary
10−2
10−1
10−4
squared descriptive distance correlation, r 2
10−3
10−2
10−1
squared descriptive distance correlation, r 2 exploratory · stages separate · descriptive, not a variance decomposition
Figure S1. Evidence alignment depends on response stage and representation. Squared descriptive correlations between vectorized pairwise-distance matrices are shown for the local fingerprint and recurrence summary. The atomic (SPECFORM-H1) and interaction (SPECFORM-H2) stages share the 320-program corpus but remain separate. Because pairwise entries are dependent, r2 is a descriptive squared distancematrix correlation, not a variance decomposition. The analysis is exploratory.
S8
Reach of the fixed mathematical grammar
A frozen repository search recorded 68 published executable psychological-model candidates. None was exactly representable under all criteria of the fixed grammar; after correction of a classificationrule ordering issue, 65 were judged comparable only through an external adapter. Coverage was incomplete for several repositories, and most classifications were provisional because source implementations were not fully inspected. This establishes that the experimental grammar is narrow.
S9
Reproducible publication build
The accompanying ancillary package preserves the original analysis inputs, numerical result objects, figure builders and verification records. The source archive has one compilation entry point, 17
main.tex; the supplementary sections are integrated in this PDF. The result macros and vector figures are derived from the retained scientific result objects. From the extracted source directory, compile with pdflatex main, bibtex main, then pdflatex main twice. Retained analysis and figure regeneration source, including the pinned inputs, is supplied in anc/wp0_evidence.
References Tamás Bisztray, Bilel Cherif, Richard A. Dubniczky, Nils Gruschka, Bertalan Borsos, Mohamed Amine Ferrag, Attila Kovács, Vasileios Mavroeidis, and Norbert Tihanyi. I know which LLM wrote your code last summer: LLM-generated code stylometry for authorship attribution. In Proceedings of the 18th ACM Workshop on Artificial Intelligence and Security, pages 28–39. Association for Computing Machinery, 2025. doi: 10.1145/3733799.3762964. Pablo Samuel Castro, Nenad Tomasev, Ankit Anand, Navodita Sharma, Rishika Mohanta, Aparna Dev, Kuba Perlin, Siddhant Jain, Kyle Levin, Noemi Elteto, Will Dabney, Alexander Novikov, Glenn C. Turner, Maria K. Eckstein, Nathaniel D. Daw, Kevin J. Miller, and Kim Stachenfeld. Discovering symbolic cognitive models from human and animal behavior. In Proceedings of the 42nd International Conference on Machine Learning, volume 267 of Proceedings of Machine Learning Research, pages 6849–6890, 2025. URL https://proceedings.mlr.press/v267/castro25a.html. Alexander D’Amour, Katherine Heller, Dan Moldovan, et al. Underspecification presents challenges for credibility in modern machine learning. Journal of Machine Learning Research, 23(226):1–61, 2022. URL https://jmlr.org/papers/v23/20-1335.html. David Draper. Assessment and propagation of model uncertainty. Journal of the Royal Statistical Society: Series B (Methodological), 57(1):45–70, 1995. doi: 10.1111/j.2517-6161.1995.tb02015.x. Simon Farrell and Stephan Lewandowsky. Computational models as aids to better reasoning in psychology. Current Directions in Psychological Science, 19(5):329–335, 2010. doi: 10.1177/0963721410386677. Debargha Ganguly, Vikash Singh, Sreehari Sankar, Biyao Zhang, Xuecen Zhang, Srinivasan Iyengar, Xiaotian Han, Amit Sharma, Shivkumar Kalyanaraman, and Vipin Chaudhary. Grammars of formal uncertainty: When to trust LLMs in automated reasoning tasks. In Advances in Neural Information Processing Systems, volume 38, 2025. URL https://papers.neurips.cc/paper_files/paper/2025/ hash/30ff6279fb18304d3eac481970157430-Abstract-Conference.html. Olivia Guest and Andrea E. Martin. How computational modeling can force theory building in psychological science. Perspectives on Psychological Science, 16(4):789–802, 2021. doi: 10.1177/1745691620970585. Bernardo A. Huberman and Natalie S. Glance. Evolutionary games and computer simulations. Proceedings of the National Academy of Sciences of the United States of America, 90(16):7716–7718, 1993. doi: 10.1073/pnas.90.16.7716. Quentin J. M. Huys, Tiago V. Maia, and Michael J. Frank. Computational psychiatry as a bridge from neuroscience to clinical applications. Nature Neuroscience, 19(3):404–413, 2016. doi: 10.1038/nn.4238. Aditi Kabra, Jonathan Laurent, Sagar Bharadwaj, Ruben Martins, Stefan Mitsch, and André Platzer. Can large language models autoformalize kinematics? In Proceedings of the 25th Conference on Formal Methods in Computer-Aided Design, pages 78–83. TU Wien Academic Press, 2025. doi: 10.34727/2025/ isbn.978-3-85448-084-6_13. Marc C. Kennedy and Anthony O’Hagan. Bayesian calibration of computer models. Journal of the Royal Statistical Society: Series B, 63(3):425–464, 2001. doi: 10.1111/1467-9868.00294. Zenan Li, Yifan Wu, Zhaoyu Li, Xinming Wei, Fan Yang, Xian Zhang, and Xiaoxing Ma. Autoformalize mathematical statements by symbolic equivalence and semantic consistency. In Advances in Neural Information Processing Systems, volume 37, pages 53598–53625, 2024. doi: 10.52202/079017-1697. Yifan Mo, Xiao Fu, Yue Su, Qingyu Meng, Koen Hindriks, Qingzhi Liu, and Jiahuan Pei. SciText2Eq: Assessing LLMs for explainable equation generation for scientific creativity. arXiv preprint arXiv:2606.16003, 2026.
18
Hannah Muelder and Tatiana Filatova. One theory—many formalizations: Testing different code implementations of the theory of planned behaviour in energy agent-based models. Journal of Artificial Societies and Social Simulation, 21(4):5, 2018. doi: 10.18564/jasss.3855. Jay I. Myung and Mark A. Pitt. Optimal experimental design for model discrimination. Psychological Review, 116(3):499–518, 2009. doi: 10.1037/a0016104. Anna Nagurney, Takashi Takayama, and Ding Zhang. Projected dynamical systems modeling and computation of spatial network equilibria. Networks, 26(2):69–85, 1995. doi: 10.1002/net.3230260203. Andre Panossian. SPECFORM-H1 and SPECFORM-H2: Renderer-format theory-to-program translation datasets (v1.0.0). Dataset, 2026a. URL https://doi.org/10.5281/zenodo.21876518. Andre Panossian. SPECFORM: Software and frozen source inventory for a prospective randomized study of renderer format in LLM theory-to-program translation. Software, 2026b. URL https://doi.org/10. 5281/zenodo.21879576. Milena Rmus, Akshay Kumar Jagadish, Marvin Mathony, Tobias Ludwig, and Eric Schulz. Generating computational cognitive models using large language models. In Advances in Neural Information Processing Systems, volume 38, pages 87796–87833. Curran Associates, Inc., 2025. doi: 10.52202/085713-2935. URL https://papers.nips.cc/paper_files/paper/2025/hash/ 7f14c9df045c5b58893a87079d16d2b3-Abstract-Conference.html. Sophia Rupprecht, Yassine Hounat, Monisha Kumar, Giacomo Lastrucci, and Artur M. Schweidtmann. Text2Model: Generating dynamic chemical reactor models using large language models (LLMs). arXiv preprint arXiv:2503.17004, 2025. Birgitt Schönfisch and André de Roos. Synchronous and asynchronous updating in cellular automata. BioSystems, 51(3):123–143, 1999. doi: 10.1016/S0303-2647(99)00025-8. Paul E. Smaldino. How to translate a verbal theory into a formal model. Social Psychology, 51(4):207–218, 2020. doi: 10.1027/1864-9335/a000425. Iris van Rooij and Mark Blokpoel. Formalizing verbal theories: A tutorial by dialogue. Social Psychology, 51 (5):285–298, 2020. doi: 10.1027/1864-9335/a000428. Yuhuai Wu, Albert Qiaochu Jiang, Wenda Li, Markus N. Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy. Autoformalization with large language models. In Advances in Neural Information Processing Systems, volume 35, pages 32353–32368, 2022. doi: 10.52202/068431-2344. Hanbo Xie, Hua-Dong Xiong, and Robert C. Wilson. From strategic narratives to code-like cognitive models: An LLM-based approach in a sorting task. In Proceedings of the First Conference on Language Modeling, 2024. URL https://openreview.net/forum?id=1Tny4KgGO2.
19