Transformed in Translation: Two-Stage Structural Uncertainty in LLM-Based Scientific Autoformalization

• URL: http://arxiv.org/abs/2609.14808v1
• Date: Sun, 13 Sep 2026 21:47:46 GMT
• Title: Transformed in Translation: Two-Stage Structural Uncertainty in LLM-Based Scientific Autoformalization
• Abstract summary: Autoformalization turns accounts into executable mathematics, but executable code does not settle which model has been constructed.<n>We examine two sources of structural uncertainty: the formalizer that generates a response law, and recurrence that turns that law into trajectories.
• Score: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• 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.

Related papers

• Does the way we write a theory change the program an LLM builds from it? A prospective randomized study of renderer format in LLM theory-to-program translation [0.0]
  A verbal theory does not run: translating it into an executable model requires choices about variables, interventions, and interactions.<n>We tested whether the presentation of otherwise identical theoretical content systematically changes the programs produced by theoretical language models.
  arXiv  Detail & Related papers  (2026-08-10T23:37:47Z)
• Beyond Detection: Evaluating Defensive LLMs Against AI-Generated Social Engineering in Live Turn-by-Turn Interaction [42.06723421277899]
  Generative AI makes social-engineering attacks more fluent, adaptive, and scalable.<n>We formalize trust-chain localization: identifying whether an interaction fails at actor authority, asset control, verification sufficiency, or transaction path.<n>We construct a controlled 300-case online-housing corpus spanning 20 scenario families, legitimate cases, four structural failure modes, and three surface conditions.
  arXiv  Detail & Related papers  (2026-08-10T21:17:03Z)
• Beyond Value Benchmarks: Measuring Value-Structure Alignment in Large Language Models via Symmetric Q-Sorts [47.02978329409663]
  We propose a symmetric human-LLM evaluation framework, grounded in Q methodology, to measure value-structure alignment.<n>Under our protocol, humans and models sort an identical 140-item moral statement set into a shared nine-column forced distribution.<n>We evaluate 12 LLMs across four model families via 240 replicated Q-sorts at two temperature settings.
  arXiv  Detail & Related papers  (2026-06-20T08:15:41Z)
• Automated Proving of Shannon-Type Entropy Inequalities via Fine-Tuned Language Models and Guided Tree Search [50.16356451328644]
  Proving Shannon-type entropy inequalities is a fundamental task in information theory.<n>We investigate whether small-scale large language models, fine-tuned on atomic proof steps, can automate this process.<n>We show that GPT-5.5 solves 1.7% samples under zero-shot prompting while Psitip solves 33.3% samples.
  arXiv  Detail & Related papers  (2026-06-04T05:43:12Z)
• Convergence Theory for Iterative LLM-Based Neural Architecture Search: A Parametric Cross-Entropy Framework with Closed-Form Proxy Reliability [48.83701310501069]
  Large language models (LLMs) are increasingly used as generators in iterative neural architecture search (NAS)<n>We model iterative LLM-NAS as a parametric Cross-Entropy (CE) method over executable programs.<n>We prove six results: (1) iterative LLM fine-tuning on elite architectures is equivalent to the CE update restricted to the LLM family; (2) expected architecture quality is monotonically non-decreasing across cycles; and (3) elite-set probability converges to a fixed point at a geometric rate.
  arXiv  Detail & Related papers  (2026-05-28T15:45:19Z)
• CasualSynth: Generating Structurally Sound Synthetic Data [44.80087038178069]
  Large Language Models (LLMs) generate realistic synthetic data but offer no guarantee that their outputs respect the causal mechanisms governing the target domain.<n>We introduce Causal Synth, a framework that decouples causal structure generation from semantic realization, yielding synthetic data that is both causally valid and linguistically rich.
  arXiv  Detail & Related papers  (2026-05-17T16:21:01Z)
• Reinforcing 3D Understanding in Point-VLMs via Geometric Reward Credit Assignment [45.205992501478256]
  We propose a framework that disentangles holistic supervision into field-specific signals and routes them exclusively to their responsible token spans.<n>Our approach bridges the reliability gap by boosting 3D KPA from 0.64 to 0.93, increasing 3D bounding box intersection over union to 0.686, and raising reprojection consistency scores to 0.852.
  arXiv  Detail & Related papers  (2026-04-23T00:01:40Z)
• ATLAS: Constitution-Conditioned Latent Geometry and Redistribution Across Language Models and Neural Perturbation Data [0.0]
  Constitution-conditioned post-training can be analysed as a structured perturbation of a model's learned representational geometry.<n>We introduce ATLAS, a geometry-first program that traces constitution-induced hidden-state structure across charts, models, and substrates.
  arXiv  Detail & Related papers  (2026-04-19T23:26:02Z)
• Thinking in Different Spaces: Domain-Specific Latent Geometry Survives Cross-Architecture Translation [0.7162422068114824]
  We investigate whether independently trained language models converge to geometrically compatible latent representations.<n>We learn a linear projection matrix that maps activation vectors from a large teacher model into the coordinate system of a smaller student model.<n>We report a near-zero correlation between geometric alignment quality and behavioral correction rate.
  arXiv  Detail & Related papers  (2026-03-20T18:26:23Z)
• Symmetry-Constrained Language-Guided Program Synthesis for Discovering Governing Equations from Noisy and Partial Observations [0.0]
  We introduce SymLang (Symmetry-constrained Language-guided equation discovery), a unified framework that brings together three previously separate ideas.<n>Across 133 dynamical systems SymLang achieves an exact structural recovery rate of 83.7% under 10% observational noise.<n>In all tested regimes the framework correctly identifies structural degeneracy, reporting it explicitly rather than returning a confidently wrong single equation.
  arXiv  Detail & Related papers  (2026-03-06T20:42:36Z)
• The Geometry of Thought: How Scale Restructures Reasoning In Large Language Models [0.0]
  We analyze 25,000+ chain-of-thought trajectories across four domains (Law, Science, Code, Math)<n>We discover that neural scaling laws trigger domain-specific phase transitions rather than uniform capability gains.
  arXiv  Detail & Related papers  (2026-01-19T19:53:37Z)
• ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization [73.0780809974414]
  We propose a Reflective Autoformalization method that integrates semantic consistency evaluation into the autoformalization process.<n>This enables the model to iteratively generate formal statements, assess its semantic fidelity, and self-correct identified errors.<n>Experiments show that ReForm achieves an average improvement of 22.6 percentage points over the strongest baselines.
  arXiv  Detail & Related papers  (2025-10-28T16:22:54Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.