Aligning Faithfulness for Theory-Scale Autoformalization

1 INTRODUCTION

• Faithfulness requires preserving meaning across dependencies and assumptions, yet existing evaluations largely issue item-level scores or verdicts without mapping context to formal dependencies.When context is missing, different interpretations may remain possible, making a definite verdict unsupported.Source: §1 · p. 1
• The proposed context-aware align-then-label task links informal and formal regions, then labels each link to make judgments traceable and errors systematically analyzable.Inputs include an informal target, source context and assumptions, a Lean target, and relevant formal dependencies.Source: §1 · p. 2
• FaithAlign contains 460 items and 4,982 annotated links, while FaithAlign-Gap withholds context and assumptions across 146 items to test recognition of undecidability.The benchmark operationalizes fine-grained correspondence and evaluation of defect and underspecification identification.Source: §1 · p. 2
• 47.8% defect F1 was GPT-6 Astra’s highest score, yet it found every defect in only 34.3% of defective items and recognized 28.2% of undecidable cases.It also failed to align 68.6% of defective context links.Source: §1 · p. 2

2 ILLUSTRATIVE OVERVIEW

• In ProofNet (Azerbayev et al., 2023), the formalization fixes scalars to C and omits R; ProofNet-Verified uses RCLike F to cover both fields.At theory scale, later theorems can depend on this definition, propagating the error and rendering sections unusable.Source: §2 · p. 2
• The example is under-specified in isolation: V, L(V), and the scalar field are not stated, and ProofNet’s accepted formalization was later judged unfaithful by ProofNet-Verified.The account presents this disagreement as evidence that ambiguities can pass expert review.Source: §2 · pp. 2–3
• Across five sources, FaithAlign’s overview buckets eleven samples’ segments as targets, context, or assumptions and marks faithful and unfaithful links distinctly.The annotations aim to capture every unfaithful defect for systematic analysis.Source: Figure 2 · p. 3, §2 · p. 3
• The evaluation conditions judgments on necessary context and links phrase-level segments, localizing the missing R while showing which formal regions remain faithful.This makes clear that one section, rather than the entire item, is the issue.Source: §2 · p. 3

3 PROBLEM FORMULATION

• Faithfulness evaluation becomes an align-then-label task: align informal text with Lean code, then label each link using context that determines meaning.Source: §3 · pp. 3–4

3.1 INPUTS

• Each item pairs informal and formal targets with source context, formal dependencies, and explicit assumptions for interpretive choices left open by either source.Source: §3.1 · p. 4

3.2 LABELED ALIGNMENTS

• Regions are selected character sets linked across informal and formal material; either endpoint may be empty to represent an absent counterpart.Links are implicit, contextual, or target-level according to whether their endpoints include assumptions, context, or only targets.Source: §3.2 · p. 4, Figure 3 · p. 4
• Each link is labeled faithful or unfaithful, while an undecidable label applies when reasonable interpretations yield different judgments and the supplied material cannot settle the choice.Source: §3.2 · pp. 4–5
• Findings pair an alignment with its label, and item verdicts follow a priority rule: any defect makes the item unfaithful, otherwise any undecidable link makes it undecidable.Y denotes reference findings and bY predicted findings.Source: Figure 4 · p. 4, §3.2 · p. 5

3.3 EVALUATION METRICS

• Link-level F1 measures recovery with correct labels using endpoint overlap, with separate scores for all links, defects, and undecidable links.Defect F1@0.5 requires at least half recall and precision at every endpoint for a match.Source: §3.3 · p. 5
• Item-level rates distinguish complete defect recovery from verdict accuracy, with undecidable-item rate measuring verdict accuracy specifically on undecidable items.Source: §3.3 · p. 5

4.1 BENCHMARK CONSTRUCTION

• Five sources supply the target pairs, and four Lean- and mathematics-trained graduate experts annotated contexts and links over about eight person-months, with a second annotator reviewing each item.The completed annotations retain 81.9% alignment-link overlap with initial versions under the evaluation scorer.Source: §4.1 · pp. 5–6

4.2 DATASET STATISTICS

• FaithAlign contains 460 full-context items and 4,982 links; 25.5% of links involve context or assumptions, and FaithAlign-Gap contains 146 items.Figure 5 summarizes source composition and input lengths, while Figure 6 summarizes endpoint types and links per item.Source: §4.2 · p. 6, Figure 5 · p. 6, Figure 6 · p. 6

4.3 EVALUATION TASKS AND PROTOCOL

• Full-context alignment evaluates recovery of faithful links and defects across 460 items, using targets, context, assumptions, and formal dependencies.Links can represent acceptable one-sided omissions or additions as faithful, while a required missing condition is unfaithful; scoring includes defect F1, defect F1@0.5, joint F1, and all-defects rate.Source: §4.3 · pp. 6–7
• Context-omitted alignment tests whether models recognize insufficient information on 146 items, allowing undecidable labels and comparing 85 triplets with their two full-context versions.The set withholds informal context and assumptions while retaining targets and formal context; it includes undecidable items and decidable controls.Source: §4.1 · p. 6, §4.3 · p. 7

5.1 EXPERIMENTAL SETUP

• The evaluation covers all 460 FaithAlign and 146 FaithAlign-Gap items, with three repetitions of full-context and context-omitted alignment per model.Eight models were evaluated; alignment tasks included text-search and answer-validation tools but no mathematical correctness feedback.Source: §5.1 · p. 7

5.2 RESEARCH QUESTIONS AND FINDINGS

• 15.7 percentage points below the overall score, contextual links have the lowest joint F1, with roughly three quarters of contextual defects never aligned.Defects involving implicit assumptions are omitted in much the same way.Source: Figure 11 · p. 8, §5.2 · p. 8
• 47.8% defect F1 is GPT-6 Astra’s best score, and it finds every defect in only 4.5% of items with two or more defects.Most missed defects are never aligned rather than aligned and mislabeled.Source: §5.2 · p. 8
• In context-omitted alignment, Astra judges both versions correctly in 96.9% of triplets when each reading is explicit, yet gives definite verdicts in every repetition for 52 of 85 triplets.Models often fail to recognize that an absent context leaves the judgment open.Source: §5.2 · pp. 8–9, Table 1 · p. 9, Figure 12 · p. 9
• Roughly 60% of annotated links remain unaligned on average, as predicted-link counts grow more slowly than annotated-link counts.About a third of failures are overmerged predictions that collapse several annotated links into one.Source: Figure 10 · p. 8, Figure 9 · p. 8, §5.2 · p. 9

• Prover-data pipelines use model quality scores, contradiction checks, and whole-statement faithfulness judgments to filter autoformalized statements, but cannot localize unfaithful parts; audits find missing or added hypotheses compilation misses (Meek et al., 2026).Source: §6 · p. 9
• Existing faithfulness evaluations mostly score or judge whole statements, whereas this benchmark targets fine-grained informal–formal links, including missing content and undecidable items.Prior methods include reference-based comparisons, source-based consistency tests, and model-based evaluators.Source: §6 · p. 9
• Fine-grained reasoning, hallucination, and NLP alignment work localize errors or align spans, but align-then-label links paired informal and Lean regions and attaches a faithfulness label to each.A region may contain several disjoint spans, and each link can be labeled.Source: §6 · p. 10
• FaithAlign-Gap asks whether an evaluator recognizes that the supplied material leaves a link’s interpretation open, rather than merely whether the model knows an answer.This treats undecidability as a property of the input, not the model’s own knowledge.Source: §6 · p. 10

• Models frequently miss defects, overlook contextual links, and give definite judgments when essential information is absent.The paper identifies detailed alignment and reasoning about contextual dependencies as central challenges for reliable faithfulness assessment.Source: §7 · p. 10
• Future evaluators should systematically trace dependencies, search for additional defects, and identify missing definitions or assumptions needed to resolve undecidable judgments.Source: §7 · p. 10
• Generative AI assisted with MA-Align span proposals and research tasks including evaluation code, literature search, drafting, and figure preparation; reported numerical summaries were checked against saved results.The authors state that they take responsibility for the final content, claims, and artifacts.Source: AI USE STATEMENT · p. 10
• Researchers with access to the cited sources can request the full annotated context text from the authors.The paper quotes selected excerpts to explain annotated judgments.Source: ETHICS STATEMENT · p. 10, REPRODUCIBILITY STATEMENT · p. 11

A.1 SOURCES AND ALIGNMENT STRUCTURE

• The 460 full-context items contain 4,982 annotated links, although most items contain a defect while most individual links are faithful.A local discrepancy can make an otherwise aligned statement unfaithful.Source: §A.1 · p. 16, Table 2 · p. 16
• Sources differ in alignment structure: ProofNet-Verified has fewer links, one-sided links are most common in MA-Align and LeanEuclid–Pistis, and LCS-Bench contains most multi-span links.Source: §A.1 · p. 16, Table 3 · p. 16

A.2 INPUT LENGTHS

• Input-length statistics report character counts by component using Unicode codepoints, including whitespace; the length plot clusters nearby lengths in log space.Bubble centers represent group mean target and context lengths, with area proportional to item counts.Source: §A.2 · pp. 16–17, Table 4 · p. 16

A.3 FAITHALIGN-GAP

• FaithAlign-Gap contains 85 undecidable items paired with full-context counterparts, 12 faithful controls, and 49 unfaithful controls; its annotations include 1,481 links.Undecidable links occur in all 85 undecidable items and in 33 unfaithful controls; opposite-verdict counterparts were independently reviewed.Source: §A.3 · p. 17, Table 5 · p. 17

A.4 ANNOTATION PROCESS

• Each item receives construction by one expert annotator and review by a second; this process covers FaithAlign, FaithAlign-Gap, and opposite-verdict counterparts.The four annotators are graduate-level experts in Lean and mathematics, and annotation took about eight person-months.Source: §A.4 · p. 17
• Generative AI proposed spans only for MA-Align, and every proposed span was refined by an annotator; the analysis found no sign of favoring evaluated GPT and Claude models.On MA-Align, those four models averaged 70% of their joint F1 on the other three sources, the same proportion as the other four models.Source: §A.4 · p. 17

B.2 CONTENT AND LINK SCORES

• The scoring framework trims non-mathematical formal spans, matches eligible links one-to-one by overlap, and computes label-specific F1 from weighted credit; defect F1@0.5 requires at least half-overlap at each nonempty endpoint.The evaluation also reports repeated-trial means and sample standard deviations.Source: §B.2 · pp. 18–19

B.3 COMPLETE SETS AND REPEATED ATTEMPTS

• Complete-defect identification requires every annotated defect in an item to have a matched unfaithful prediction; verdict accuracy and undecidable-item rates separately assess item-level judgments.Best-of-three measures select the strongest response per item, while pass@3 records whether any of three responses succeeds.Source: §B.3 · p. 19

B.4 CONTEXT JUDGMENTS

• The paired context analysis compares the same 85 undecidable items with their original full-context versions; Astra is also tested on opposite-verdict full-context interpretations.The full-context parents include 72 faithful and 13 unfaithful items.Source: §B.4 · pp. 19–20

B.5 ALIGNMENT DIAGNOSTICS

• Alignment diagnostics separate unmatched references, partial-overlap loss, and label loss, and classify why links remain unmatched, including overmerging and disconnected endpoints.The categories distinguish missing endpoints from missing connections between selected regions.Source: §B.5 · p. 20

B.6 PREDICTION SPLITTING AND REFERENCE GROUPING

• Prediction splitting lets several predictions describe one reference link, whereas reference grouping lets one prediction cover several; under grouping, 40.7% of links remain unmatched.The alternative scoring methods retain the same content trimming and label-blind overlap assignments.Source: §B.6 · p. 20

C.1 DEFECT IDENTIFICATION ACROSS REPEATED ATTEMPTS

• 40.2% is the highest complete-defect pass@3; even across three attempts, models leave 64.0% of defects unidentified on average, and all-links pass@3 reaches at most 6.1%.The reported rates distinguish complete item diagnosis from link-level F1.Source: Table 7 · p. 21, §C.1 · p. 21

C.2 DEFECTS INVOLVING CONTEXT

• 74.9% of context-link defects lack a matched prediction across models, including 68.6% for Astra; the unmatched share reaches 94.1% for formal-context links to targets or empty endpoints.Missing alignments dominate the reported failures across context groups.Source: §C.2 · p. 21, Figure 13 · p. 22

C.3 RECOGNIZING UNDERSPECIFICATION

• 55 of FaithAlign-Gap’s 85 undecidable items never receive an undecidable judgment from Astra across three responses; only 20 are recognized as undecidable in all three.For 52 of the 55 never-recognized items, both full-context interpretations are judged correctly in all three repetitions.Source: §C.3 · p. 22

C.3.1 FAITHALIGN-GAP EXAMPLES

• For isosceles triangles, the stated inclusive convention makes equilateral triangles isosceles, while the alternative excludes them; Astra gives faithful judgments with full context but definite unfaithful judgments when context is withheld.The paired full-context versions are judged under their stated assumptions.Source: §C.3.1 · p. 23
• In the matrix example, the source convention allows coefficients in a commutative ring, while the exercise assumption specifies real entries, changing which interpretation is supplied.The example’s target asks to show that a strictly upper triangular matrix raised to the n-th power is zero.Source: §C.3.1 · p. 24
• For the cut-rule example, the context states that predicate symbols are countable, while an implicit assumption marks that condition unfaithful because the source may allow uncountably many.In the displayed FaithAlign-Gap judgments, Astra gives unfaithful verdicts in all three responses.Source: §C.3.1 · p. 24

C.4 FINE-GRAINED ALIGNMENT AND LABELING

• Correcting every matched label raises joint F1 by an average of 4.2 percentage points, while 40.7% of links remain unmatched under reference grouping.The results attribute most missing alignment credit to endpoints and absent links.Source: §C.4 · pp. 25–26, Table 9 · p. 25, Table 12 · p. 26
• 39.2% of defective items have every defect identified by Astra under reference grouping, versus 34.3% under standard scoring; for items with two or more defects, the rates are 9.8% and 4.5%, respectively.Reference grouping permits one prediction to describe several annotated links, but defect identification remains weak.Source: §C.4 · pp. 25–26, Table 11 · p. 26

C.5 SELECTED-REGION COUNTERPART IDENTIFICATION

• Only 24.7% of selected regions have the exact complete counterpart set, and defect F1 averages 32.4%.The task supplies one endpoint, separating counterpart identification from initial region selection; outputs may omit counterparts or place their boundaries imprecisely.Source: §C.5 · p. 26, Table 13 · p. 27

C.6 RESULTS BY SOURCE

• Every model achieves its highest joint F1 on ProofNet-Verified, while defect F1 can rank sources differently, underscoring that overall alignment and defect identification are distinct evaluations.The source groups differ in link structure and the proportion of defective links.Source: Table 14 · p. 27, §C.6 · p. 27

D.1 SHARED FULL-CONTEXT INSTRUCTIONS

• Full-context instructions ask models to preserve mathematical objects, hypotheses, constructions, and relationships, judging representation independently of truth or proof success.They direct models to match coherent contributions first and use context for unmatched contributions or interpretations that require it.Source: §D.1 · p. 28

D.2 FULL-CONTEXT ALIGNMENT

• Full-context alignment links one natural-language contribution to one formal contribution, with target, context, or assumption endpoints; missing required conditions receive an unfaithful label.Meaningful faithful correspondences and unmatched contributions are included, not just defects.Source: §D.1 · p. 28

D.3 SELECTED-REGION COUNTERPART IDENTIFICATION

• Selected-region tasks supply an anchor and ask for every relevant counterpart, with separate links allowed when the same span serves different mathematical purposes.Counterparts may be in targets or context, or may be empty.Source: §D.3 · pp. 29–30

D.4 CONTEXT-OMITTED ALIGNMENT

• In context-omitted alignment, models use faithful, unfaithful, or not-decidable labels; not-decidable applies when reasonable interpretations consistent with the visible wording yield different judgments.An established defect makes the whole item unfaithful even when another contribution has an unresolved interpretation.Source: §D.4 · p. 30

D.5 USER MESSAGE

• Evaluation packets provide document identifiers, sides, roles, and complete texts, while selected-region packets additionally include anchor spans and their selected text.Reference counterparts and labels are withheld from the packets.Source: §D.5 · p. 31