cs.CLOct 13, 2026

Aligning Faithfulness for Theory-Scale Autoformalization

Authors: Yuming Feng, Tadd Mao, Dhruva Arekar, Tianjun Zhong, Jiani Huang, Xujie Si, Ziyang Li

Organizations: Johns Hopkins University · University of Toronto · University of Pennsylvania

Read PDF
Ask AI
Cite

Copy citation

DOINot available for this paper

Abstract

Autoformalization (AF) requires more than compilation: formal statements must preserve the meaning of their informal sources, a property known as faithfulness. An emerging frontier is the automated evaluation of this property, yet most existing methods operate at the statement level and produce whole-item verdicts, failing to reveal how individual expressions correspond or which contextual interpretations support the judgment. This omission is consequential because AF is inherently theory-scale: target statements derive their meaning from surrounding mathematical material and unstated conventions. We formulate faithfulness evaluation as a context-aware align-then-label problem: identifying phrase-level correspondences between informal and formal statements and assigning a faithfulness label to each under explicitly specified contextual interpretations and assumptions. We also introduce FaithAlign, the first theory-scale faithfulness benchmark comprising 460 items and 4,982 annotated phrase-level links, alongside FaithAlign-Gap, a companion set of 146 items with informal context and assumptions withheld. Each FaithAlign item includes the target statement pair, relevant context, formal dependencies, and, where needed, assumptions specifying one given interpretation. Across 8 models, GPT-6 Astra achieves the highest defect F1 at 47.8% and identifies all defects in only 4.5% of items with two or more defects. On FaithAlign-Gap, Astra identifies only 28.2% of undecidable items as such. These results show the difficulty of recovering context-dependent correspondences, establishing FaithAlign as a testbed for fine-grained, context-aware faithfulness evaluation.

Figures & tables

Figure 1: A motivating example from Axler (2015) with the unfaithful formalization drawn from ProofNet ( Azerbayev et al., 2023 ) , and faithful one from ProofNet-Verified ( An et al., 2026 ) .
Figure 2: A bird’s-eye-view illustration of eleven samples (with truncation) from FaithAlign, where each segment from natural language (NL) or formal language is bucketed into Target, Context, or Implicit Assumptions. Segments from both sides are matched or unconnected (connected to ∅\varnothing ): faithful links are indicated by green lines, while unfaithful links are marked in red, implying that the overall Lean formalization is unfaithful to the NL source.
Figure 3: Schematic examples of the six link types. Rows give the label, and columns give which regions the link contains. ∅\varnothing marks an absent counterpart.
Figure 5: Composition and input lengths for LCS-Bench (LCS), ProofNet-Verified (PN-V), MA-Align (MA), and LeanEuclid–Pistis (LE-P). In (c), centers are group means; area ∝\propto count.
Figure 7: Full-context alignment F1 per model.
Figure 6
Figure 11: Alignment scores and outcomes across all models. (a) Joint F1 relative to the pooled 37.6%, in percentage points. Outer rings split outcomes by label in (b), faithful (F) or unfaithful (U), and by role in (c), target (T), context (C), or implicit (I).
Figure 8
Appendix figures & tables14 assets

Supplementary material from the paper’s appendix.

Appendix

 ItemsLinks
SourceTotalFaithfulUnfaithfulTotalFaithfulUnfaithful
LCS-Bench196471492,2181,883335
ProofNet-Verified77314643637462
MA-Align12242801,4701,142328
LeanEuclid–Pistis65442185883325
Total4601642964,9824,232750
Appendix
Table 1: Full-context items and alignment links by source.
 Links per item  
SourceMin.MedianMeanMax.One-sidedMulti-span
LCS-Bench21111.32231281,130
ProofNet-Verified255.66123237
MA-Align210.512.0534359139
LeanEuclid–Pistis51313.2028257192
Total21010.83347761,498
Appendix
Table 2: Alignment density and structure by source.
ComponentLCS-BenchProofNet-VerifiedMA-AlignLeanEuclid–Pistis
Informal target TNT_{N}392 [59, 1,874]114 [46, 377]195.5 [25, 1,661]404 [64, 1,037]
Formal target TFT_{F}854 [152, 3,166]244 [104, 488]299 [96, 1,181]275 [124, 719]
Source context CNC_{N}13,850 [246, 42,316]98 [0, 495]163 [0, 1,829]245 [0, 1,064]
Formal context CFC_{F}6,656.5 [498, 18,641]3,411 [15, 15,800]1,002 [60, 9,138]1,893 [896, 6,691]
Assumptions II0 [0, 2,623]0 [0, 614]0 [0, 844]0 [0, 161]
Appendix
Table 3: Input lengths in characters: median above [minimum, maximum].
 Item verdictsLink labels
SourceFUNDFUND
LCS-Bench273934119274
ProofNet-Verified71013951520
MA-Align3322337569115
LeanEuclid–Pistis0010143015
Total124985954103424
Appendix
Table 4: FaithAlign-Gap items and link labels by source (F: faithful; U: unfaithful; ND: undecidable).
ModelBedrock model identifierAPIReasoning
GPT-6 Astraglobal.openai.gpt-6-astraResponses v1Medium
GPT-5.6 Solglobal.openai.gpt-5.6-solResponses v1Medium
Kimi K3global.moonshotai.kimi-k3Responses v1Medium
Opus 5global.anthropic.claude-opus-5ConverseStreamMedium
Opus 4.8global.anthropic.claude-opus-4-8ConverseStreamMedium
DeepSeek V3.2deepseek.v3.2ConverseStreamDefault
Appendix
Table 5: Model identifiers and request settings on Amazon Bedrock. Medium denotes an explicitly requested reasoning effort; default denotes the provider’s reasoning configuration. Both Opus models use adaptive thinking.
 Defect F1Joint F1Complete-item pass@3
ModelSingleBest of 3SingleBest of 3All defectsAll links
GPT-5.6 Sol42.7% ±1.1%42.7\%\,{\scriptstyle\pm\,1.1\%}52.4%45.5% ±0.1%45.5\%\,{\scriptstyle\pm\,0.1\%}51.0%39.5%5.7%
Opus 531.9% ±0.2%31.9\%\,{\scriptstyle\pm\,0.2\%}39.3%44.6% ±0.3%44.6\%\,{\scriptstyle\pm\,0.3\%}49.5%27.7%6.1%
GPT-6 Astra47.8% ±0.5%47.8\%\,{\scriptstyle\pm\,0.5\%}52.6%47.6% ±0.4%47.6\%\,{\scriptstyle\pm\,0.4\%}50.9%37.8%5.4%
Opus 4.826.4% ±0.5%26.4\%\,{\scriptstyle\pm\,0.5\%}33.0%44.3% ±0.1%44.3\%\,{\scriptstyle\pm\,0.1\%}49.0%23.3%5.7%
Kimi K338.7% ±2.3%38.7\%\,{\scriptstyle\pm\,2.3\%}51.4%44.1% ±0.8%44.1\%\,{\scriptstyle\pm\,0.8\%}50.9%40.2%5.9%
Appendix
Table 6: Full-context alignment F1 and complete-item pass@3 (%) across three attempts, with single-attempt F1 reported as mean ±\pm standard deviation.
Figure 14: Defect outcomes by link role and context endpoint.
 FaithAlign-Gap link F1Paired item judgments
ModelFUNDGap: ND recognizedFull context: correct
GPT-6 Astra49.2% ±0.1%49.2\%\,{\scriptstyle\pm\,0.1\%}34.2% ±0.8%34.2\%\,{\scriptstyle\pm\,0.8\%}17.4% ±0.1%17.4\%\,{\scriptstyle\pm\,0.1\%}28.2% ±2.0%28.2\%\,{\scriptstyle\pm\,2.0\%}96.9% ±0.7%96.9\%\,{\scriptstyle\pm\,0.7\%}
GPT-5.6 Sol47.3% ±0.8%47.3\%\,{\scriptstyle\pm\,0.8\%}32.0% ±2.1%32.0\%\,{\scriptstyle\pm\,2.1\%}11.5% ±0.6%11.5\%\,{\scriptstyle\pm\,0.6\%}16.5% ±1.2%16.5\%\,{\scriptstyle\pm\,1.2\%}93.7% ±1.8%93.7\%\,{\scriptstyle\pm\,1.8\%}
Kimi K345.3% ±2.1%45.3\%\,{\scriptstyle\pm\,2.1\%}31.8% ±1.9%31.8\%\,{\scriptstyle\pm\,1.9\%}5.9% ±0.6%5.9\%\,{\scriptstyle\pm\,0.6\%}8.6% ±0.7%8.6\%\,{\scriptstyle\pm\,0.7\%}94.9% ±1.4%94.9\%\,{\scriptstyle\pm\,1.4\%}
Opus 544.2% ±0.2%44.2\%\,{\scriptstyle\pm\,0.2\%}29.2% ±0.8%29.2\%\,{\scriptstyle\pm\,0.8\%}1.7% ±0.8%1.7\%\,{\scriptstyle\pm\,0.8\%}2.4% ±2.0%2.4\%\,{\scriptstyle\pm\,2.0\%}94.9% ±0.7%94.9\%\,{\scriptstyle\pm\,0.7\%}
Opus 4.844.2% ±0.5%44.2\%\,{\scriptstyle\pm\,0.5\%}26.4% ±2.7%26.4\%\,{\scriptstyle\pm\,2.7\%}0.4% ±0.5%0.4\%\,{\scriptstyle\pm\,0.5\%}1.6% ±0.7%1.6\%\,{\scriptstyle\pm\,0.7\%}91.4% ±0.7%91.4\%\,{\scriptstyle\pm\,0.7\%}
Appendix
Table 7: FaithAlign-Gap scores and paired context judgments (%, mean ±\pm standard deviation across three repetitions).
 AnnotatedPredictedConditional labelingJoint F1
ModelunmatchedmatchedFaithfulUnfaithfulObservedOracle
GPT-5.6 Sol52.4% ±0.1%52.4\%\,{\scriptstyle\pm\,0.1\%}83.8% ±0.5%83.8\%\,{\scriptstyle\pm\,0.5\%}97.4% ±0.3%97.4\%\,{\scriptstyle\pm\,0.3\%}71.3% ±0.6%71.3\%\,{\scriptstyle\pm\,0.6\%}45.5% ±0.1%45.5\%\,{\scriptstyle\pm\,0.1\%}49.2% ±0.1%49.2\%\,{\scriptstyle\pm\,0.1\%}
Opus 552.3% ±0.2%52.3\%\,{\scriptstyle\pm\,0.2\%}82.3% ±0.7%82.3\%\,{\scriptstyle\pm\,0.7\%}98.6% ±0.1%98.6\%\,{\scriptstyle\pm\,0.1\%}50.1% ±1.3%50.1\%\,{\scriptstyle\pm\,1.3\%}44.6% ±0.3%44.6\%\,{\scriptstyle\pm\,0.3\%}49.6% ±0.3%49.6\%\,{\scriptstyle\pm\,0.3\%}
GPT-6 Astra55.2% ±0.3%55.2\%\,{\scriptstyle\pm\,0.3\%}91.4% ±0.2%91.4\%\,{\scriptstyle\pm\,0.2\%}96.7% ±0.2%96.7\%\,{\scriptstyle\pm\,0.2\%}82.2% ±0.1%82.2\%\,{\scriptstyle\pm\,0.1\%}47.6% ±0.4%47.6\%\,{\scriptstyle\pm\,0.4\%}50.5% ±0.3%50.5\%\,{\scriptstyle\pm\,0.3\%}
Opus 4.854.4% ±0.1%54.4\%\,{\scriptstyle\pm\,0.1\%}88.9% ±0.3%88.9\%\,{\scriptstyle\pm\,0.3\%}99.2% ±0.1%99.2\%\,{\scriptstyle\pm\,0.1\%}39.8% ±0.4%39.8\%\,{\scriptstyle\pm\,0.4\%}44.3% ±0.1%44.3\%\,{\scriptstyle\pm\,0.1\%}49.9% ±0.1%49.9\%\,{\scriptstyle\pm\,0.1\%}
Kimi K351.5% ±0.8%51.5\%\,{\scriptstyle\pm\,0.8\%}77.9% ±0.6%77.9\%\,{\scriptstyle\pm\,0.6\%}97.8% ±0.4%97.8\%\,{\scriptstyle\pm\,0.4\%}61.8% ±3.8%61.8\%\,{\scriptstyle\pm\,3.8\%}44.1% ±0.8%44.1\%\,{\scriptstyle\pm\,0.8\%}48.3% ±0.4%48.3\%\,{\scriptstyle\pm\,0.4\%}
Appendix
Table 8: Alignment coverage, conditional labeling accuracy, and observed and label-oracle joint F1 (%), as mean ±\pm standard deviation across three repetitions.
ModelnnBoth missedFormal missedInformal missedDisconnectedOvermerged
GPT-5.6 Sol749314.4%9.6%16.3%14.7%45.0%
Opus 5747420.5%10.9%17.7%21.2%29.7%
GPT-6 Astra789416.5%10.7%20.8%11.1%40.8%
Opus 4.8777625.1%12.6%19.3%12.9%30.1%
Kimi K3737017.9%8.5%15.4%13.7%44.4%
GLM-5903220.7%13.0%22.8%19.1%24.5%
Appendix
Table 9: Unmatched links ( nn ) and failure-type percentages across three repetitions, using the categories in Figure 9(b) .
 StandardPrediction splittingReference grouping
ModelDefectJointDefectJointDefectJoint
GPT-5.6 Sol42.7% ±1.1%42.7\%\,{\scriptstyle\pm\,1.1\%}45.5% ±0.1%45.5\%\,{\scriptstyle\pm\,0.1\%}45.9% ±0.7%45.9\%\,{\scriptstyle\pm\,0.7\%}49.1% ±0.1%49.1\%\,{\scriptstyle\pm\,0.1\%}49.3% ±1.1%49.3\%\,{\scriptstyle\pm\,1.1\%}63.7% ±0.3%63.7\%\,{\scriptstyle\pm\,0.3\%}
Opus 531.9% ±0.2%31.9\%\,{\scriptstyle\pm\,0.2\%}44.6% ±0.3%44.6\%\,{\scriptstyle\pm\,0.3\%}33.1% ±0.2%33.1\%\,{\scriptstyle\pm\,0.2\%}48.2% ±0.3%48.2\%\,{\scriptstyle\pm\,0.3\%}35.7% ±0.3%35.7\%\,{\scriptstyle\pm\,0.3\%}56.5% ±0.3%56.5\%\,{\scriptstyle\pm\,0.3\%}
GPT-6 Astra47.8% ±0.5%47.8\%\,{\scriptstyle\pm\,0.5\%}47.6% ±0.4%47.6\%\,{\scriptstyle\pm\,0.4\%}49.6% ±0.6%49.6\%\,{\scriptstyle\pm\,0.6\%}50.4% ±0.4%50.4\%\,{\scriptstyle\pm\,0.4\%}55.8% ±0.7%55.8\%\,{\scriptstyle\pm\,0.7\%}67.5% ±0.3%67.5\%\,{\scriptstyle\pm\,0.3\%}
Opus 4.826.4% ±0.5%26.4\%\,{\scriptstyle\pm\,0.5\%}44.3% ±0.1%44.3\%\,{\scriptstyle\pm\,0.1\%}27.0% ±0.4%27.0\%\,{\scriptstyle\pm\,0.4\%}47.6% ±0.2%47.6\%\,{\scriptstyle\pm\,0.2\%}29.7% ±0.5%29.7\%\,{\scriptstyle\pm\,0.5\%}57.2% ±0.4%57.2\%\,{\scriptstyle\pm\,0.4\%}
Kimi K338.7% ±2.3%38.7\%\,{\scriptstyle\pm\,2.3\%}44.1% ±0.8%44.1\%\,{\scriptstyle\pm\,0.8\%}41.0% ±2.5%41.0\%\,{\scriptstyle\pm\,2.5\%}47.5% ±0.9%47.5\%\,{\scriptstyle\pm\,0.9\%}45.1% ±2.0%45.1\%\,{\scriptstyle\pm\,2.0\%}60.5% ±0.7%60.5\%\,{\scriptstyle\pm\,0.7\%}
Appendix
Table 10: Full-context alignment F1 (%) under standard scoring, prediction splitting, and reference grouping, as mean ±\pm standard deviation across three repetitions.
ModelTotalUnmatchedMatched, wrongMatched, correct
GPT-5.6 Sol14,3044,123 (28.8%)910 (6.4%)9,271 (64.8%)
Opus 514,3045,257 (36.8%)1,083 (7.6%)7,964 (55.7%)
GPT-6 Astra14,3044,670 (32.6%)642 (4.5%)8,992 (62.9%)
Opus 4.814,3045,437 (38.0%)1,180 (8.2%)7,687 (53.7%)
Kimi K314,3044,097 (28.6%)1,055 (7.4%)9,152 (64.0%)
GLM-514,3046,818 (47.7%)1,480 (10.3%)6,006 (42.0%)
Appendix
Table 11: Link outcome counts (percentages) under reference grouping across three repetitions.
 Informal regionFormal region
ModelDefectJointDefectJoint
GPT-5.6 Sol45.6%66.4%45.6%65.3%
Opus 541.6%67.8%46.8%67.1%
GPT-6 Astra52.2%69.3%56.9%69.0%
Opus 4.833.8%67.2%32.6%64.2%
Kimi K333.2%64.8%38.5%62.5%
Appendix
Table 12: Selected-region counterpart identification F1 (%) in the two directions, with one repetition per model.
 LCS-Bench ( n=196n=196 )ProofNet-Verified ( n=77n=77 )
ModelDefectJointDefectJoint
GPT-5.6 Sol44.0% ±1.9%44.0\%\,{\scriptstyle\pm\,1.9\%}50.9% ±0.5%50.9\%\,{\scriptstyle\pm\,0.5\%}32.9% ±4.3%32.9\%\,{\scriptstyle\pm\,4.3\%}58.2% ±1.0%58.2\%\,{\scriptstyle\pm\,1.0\%}
Opus 529.4% ±0.6%29.4\%\,{\scriptstyle\pm\,0.6\%}49.3% ±0.2%49.3\%\,{\scriptstyle\pm\,0.2\%}30.9% ±2.5%30.9\%\,{\scriptstyle\pm\,2.5\%}57.5% ±0.9%57.5\%\,{\scriptstyle\pm\,0.9\%}
GPT-6 Astra50.1% ±1.0%50.1\%\,{\scriptstyle\pm\,1.0\%}55.8% ±0.5%55.8\%\,{\scriptstyle\pm\,0.5\%}44.4% ±2.5%44.4\%\,{\scriptstyle\pm\,2.5\%}56.7% ±0.6%56.7\%\,{\scriptstyle\pm\,0.6\%}
Opus 4.822.2% ±0.9%22.2\%\,{\scriptstyle\pm\,0.9\%}49.1% ±0.5%49.1\%\,{\scriptstyle\pm\,0.5\%}29.5% ±1.6%29.5\%\,{\scriptstyle\pm\,1.6\%}61.4% ±1.5%61.4\%\,{\scriptstyle\pm\,1.5\%}
Kimi K338.8% ±5.5%38.8\%\,{\scriptstyle\pm\,5.5\%}48.4% ±1.6%48.4\%\,{\scriptstyle\pm\,1.6\%}36.8% ±1.2%36.8\%\,{\scriptstyle\pm\,1.2\%}57.8% ±0.9%57.8\%\,{\scriptstyle\pm\,0.9\%}
Appendix
Table 13: Full-context alignment F1 (%) by source, as mean ±\pm standard deviation across three repetitions.
More in this topic

Contextual Faithfulness

Contextual faithfulness measures whether language models ground answers and reasoning in supplied evidence rather than unsupported prior knowledge.

See all 11 papers

Explore similar work

CardsList

  1. FaithformBench: Benchmarking Faithfulness of Mathematical Chain-of-Thought Autoformalisation

    Aug 11, 2026Rob Cornish, Iacopo Ghinassi, Po-Hung Yeh +7CoT FaithfulnessLLM Sycophancy

    Nanyang Technological University, Singapore · University of Oxford, United Kingdom · The University of Edinburgh, United Kingdom

  2. The Faithfulness Gap: Certifying Semantic Equivalence Between Natural-Language and Formal Mathematical Statements

    Jun 15, 2026Noor Islam S. Mohammad, Tamim SheikhFormal VerificationLean Theorem Proving

    Department of Computer Science, Informatics Institute, Istanbul Technical University, Istanbul, Türkiye · Department of Computer Science and Engineering, Jashore University of Science and Technology, Bangladesh.

  3. Beyond Compilation: Evaluating Faithful Natural-Language-to-Lean Statement Formalization

    Jun 30, 2026Ke Zhang, Patricio Gallardo Candela, Sudhir Murthy +3LLM-as-a-JudgeLean Theorem Proving

    University of California, Riverside · University of Arizona · University of California, San Diego