Casual as an Anchor: Resolving Supervision Misalignment in Formality Transfer Dataset
- URL: http://arxiv.org/abs/2605.29365v3
- Date: Mon, 01 Jun 2026 06:06:41 GMT
- Title: Casual as an Anchor: Resolving Supervision Misalignment in Formality Transfer Dataset
- Abstract summary: Formality transfer is commonly framed as a symmetric bidirectional task between informal and formal registers.<n>We argue that this framing conceals a supervision design flaw in existing benchmarks such as GYAFC.<n>We quantify this misalignment by re-evaluating benchmark formal labels under a human-aligned definition of formality.
- Score: 22.0608497133374
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Formality transfer is commonly framed as a symmetric bidirectional task between informal and formal registers. We argue that this framing conceals a supervision design flaw in existing benchmarks such as GYAFC: binary human rewrites encode relative stylistic shifts rather than absolute human notions of formality. Consequently, models learn to generate pseudo-formal outputs that satisfy benchmark labels while failing to produce genuinely formal language. We quantify this misalignment by re-evaluating benchmark formal labels under a human-aligned definition of formality, revealing substantial discrepancies that propagate to consistent informal-to-formal failures across model families. To address this issue, we reconceptualize formality transfer as a graded dimension rather than a binary attribute. We introduce a three-level spectrum: informal, casual, and formal, where casual serves as an explicit intermediate state that clarifies supervision signals. Based on this framework, we introduce 3LF, a dataset providing parallel supervision across all three levels. Training on 3LF substantially reduces informal-to-formal failures and improves alignment with human perception. For example, GPT-4.1-nano improves from 0.06 to 0.88 F1 in the informal-to-formal direction despite 3LF being significantly smaller than GYAFC. We further demonstrate that these gains cannot be reproduced through in-context learning alone and provide qualitative analyses of ambiguity-driven errors and meaning distortions. Overall, our findings demonstrate how supervision design shapes stylistic alignment and highlight the importance of alignment-aware benchmark construction in controllable text generation.
Related papers
- Beyond Solver Verdicts: Generative Reward Models for Autoformalization [6.845799966508813]
We introduce Generative Verification (GenV), which distills an offline Z3-equivalence oracle into a reference-free, continuous reference-equivalence score.<n>GenV achieves 0.961 AUROC in reference-equivalence verification, generalizes zero-shot across unseen translators and divergent formal styles.
arXiv Detail & Related papers (2026-09-10T04:47:55Z) - Weave of Formal Thought [51.56484100374058]
We introduce Weave of Formal Thought (WoFT), a paradigm uniting rigorous syntactic validation with learned structural representations.<n>We present a latent-variable fine-tuning method training the language model to interleave non-terminal grammar symbols directly into generation.<n>For Python, fine-tuning StarCoder2-3B with our RWS objective reduces per-token cross-entropy by 14.3% relative to a text-only SFT baseline.
arXiv Detail & Related papers (2026-06-24T15:58:11Z) - Evaluating the Robustness of Proof Autoformalization in Lean 4 [8.029528831501514]
We argue that a robust proof autoformalizer must remain faithful even for informal proofs that diverge from idealized ones.<n>We build a benchmark with both perturbations on miniF2F and MATH-500.<n>We evaluate seven recent models, all of which are sensitive to global perturbations and mostly fail to remain faithful under local perturbations.
arXiv Detail & Related papers (2026-06-12T18:10:21Z) - Reasoning without Gold Standards: A Proxy-Judge Theory of Autoformalization [25.540859911959885]
Autoformalization (AF) asks a model to translate informal mathematical or logical reasoning into a formally checkable object.<n>We introduce a reference-free proxy-judge framework for AF that replaces gold-standard matching with a vector of per-axis property checks.<n>Across seven formalization backbones on miniF2F, ProofNet, e-SNLI, and ProntoQA, refinement consistently lifts Pass Rate over the single-shot ICL baseline.
arXiv Detail & Related papers (2026-06-08T12:57:09Z) - Closing the Alignment-Maturity Gap in Federated Prototype Learning [42.18063554577504]
FedSAP is a framework that stabilises federated representation learning through two complementary mechanisms.<n> Experiments show gains of up to 4 percentage points over the prototype-based baselines evaluated.
arXiv Detail & Related papers (2026-06-01T12:30:53Z) - Beyond Distribution Estimation: Simplex Anchored Structural Inference Towards Universal Semi-Supervised Learning [47.92504362652887]
Semi-supervised learning faces significant challenges in realistic scenarios where labeled data is scarce and unlabeled data follows unknown, arbitrary distributions.<n>We formalize this critical yet under-explored paradigm as Universal Semi-supervised Learning (UniSSL)<n>We introduce a weighting strategy based on distribution-agnostic metrics to prioritize reliable pseudo-labels and an auxiliary branch to isolate potentially erroneous pseudo-labels.
arXiv Detail & Related papers (2026-05-08T10:33:09Z) - Surface Sensitivity in Lean 4 Autoformalization [1.7855077077275565]
We find that the observed paraphrase sensitivity reflects compilation-boundary failures rather than semantic divergence among successful formalizations.<n>Our results suggest that future training-time interventions should target the compile boundary rather than the semantic layer.
arXiv Detail & Related papers (2026-04-25T04:26:19Z) - Character as a Latent Variable in Large Language Models: A Mechanistic Account of Emergent Misalignment and Conditional Safety Failures [70.48661957773449]
Emergent Misalignment refers to a failure mode in which fine-tuning large language models on narrowly scoped data induces broadly misaligned behavior.<n>Across multiple domains and model families, we find that fine-tuning models on data exhibiting specific character-level dispositions induces substantially stronger and more transferable misalignment than incorrect-advice fine-tuning.
arXiv Detail & Related papers (2026-01-30T15:28:42Z) - Refinement Provenance Inference: Detecting LLM-Refined Training Prompts from Model Behavior [58.751981587234916]
This paper formalizes the Refinement Provenance Inference (RPI) audit task as Refinement Provenance Inference (RPI)<n>We propose RePro, a logit-based framework that fuses teacher-forced likelihood features with logit-ranking signals.<n>During training, RePro learns a transferable representation via shadow fine-tuning, and uses a lightweight linear head to infer provenance on unseen victims without training-data access.
arXiv Detail & Related papers (2026-01-05T10:16:41Z) - 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) - Conjecturing: An Overlooked Step in Formal Mathematical Reasoning [10.398167568549924]
Many mathematical problems cannot be formalised directly without first conjecturing a conclusion.<n>We develop ConjectureBench to measure the conjecturing capabilities of Large Language Models.<n>We show that our method achieves the first successful end-to-end autoformalisation of 13 PutnamBench problems with GPT-4.1 and 7 with DeepSeek-V3.1.
arXiv Detail & Related papers (2025-10-13T22:29:49Z) - StepFun-Formalizer: Unlocking the Autoformalization Potential of LLMs through Knowledge-Reasoning Fusion [30.51794514312176]
We identify two key abilities for effective autoformalization.<n>We introduce ThinkingF, a data synthesis and training pipeline that improves both abilities.<n>The resulting 7B and 32B models exhibit both comprehensive formal knowledge and strong informal-to-formal reasoning.
arXiv Detail & Related papers (2025-08-06T13:28:22Z) - Semi-supervised Formality Style Transfer using Language Model
Discriminator and Mutual Information Maximization [52.867459839641526]
Formality style transfer is the task of converting informal sentences to grammatically-correct formal sentences.
We propose a semi-supervised formality style transfer model that utilizes a language model-based discriminator to maximize the likelihood of the output sentence being formal.
Experiments showed that our model outperformed previous state-of-the-art baselines significantly in terms of both automated metrics and human judgement.
arXiv Detail & Related papers (2020-10-10T21:05:56Z)
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.