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

• URL: http://arxiv.org/abs/2608.10916v1
• Date: Tue, 11 Aug 2026 13:36:52 GMT
• Title: FaithformBench: Benchmarking Faithfulness of Mathematical Chain-of-Thought Autoformalisation
• Abstract summary: Autoformalisation systems map natural language reasoning steps into formal statements in a proof assistant such as Lean.<n>Existing approaches require expensive human-annotated ground truth, or rely on LLM judges or embedding models.<n>We propose a new benchmark for AF faithfulness that is cheap to apply, sound under weak assumptions, and assesses both positive and negative examples.
• Score: 26.089963426404164
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Autoformalisation (AF) systems map natural language reasoning steps into formal statements in a proof assistant such as Lean. We consider how to assess the faithfulness of these systems. Existing approaches require expensive human-annotated ground truth, or rely on LLM judges or embedding models, which come with limited guarantees of accuracy. In addition, these methods typically only consider inputs that are known to be correct, and therefore do not assess whether the AF translates incorrect inputs faithfully. To address these limitations, we propose a new benchmark for AF faithfulness that is cheap to apply, sound under weak assumptions, and assesses both positive and negative examples. Our method is based on automatically generating perturbed reasoning steps that are designed to be invalid, and then measuring validity preservation on unperturbed steps and invalidity preservation on perturbed steps. We apply our method to eight AF systems across four mathematical datasets, and observe pervasive sycophancy: many AFs "silently correct" invalid inputs into provable statements. The most validity-preserving fine-tuned AFs are also the most sycophantic, suggesting a tension between validity and invalidity preservation in current AF systems.

Related papers

• Non-Parametric Rehearsal Learning via Conditional Mean Embeddings [88.89267783967263]
  We propose a non-parametric rehearsal learning approach for textitavoiding undesired future (AUF) problems.<n>Specifically, we use kernel machinery to reformulate the AUF objective into a unified representation that disentangles desirability modeling from action-induced distributional changes.
  arXiv  Detail & Related papers  (2026-05-09T15:30:52Z)
• Confidence-Aware Alignment Makes Reasoning LLMs More Reliable [65.44962502963378]
  We introduce CASPO, a framework that aligns token-level confidence with step-wise logical correctness without training a separate reward model.<n>During inference, we propose Confidence-aware Thought (CaT), which dynamically prunes uncertain reasoning branches with negligible O(V) latency.<n>Experiments across ten benchmarks and multiple model families show that CASPO consistently improves reasoning reliability and inference efficiency.
  arXiv  Detail & Related papers  (2026-05-08T07:08:25Z)
• Draft-and-Prune: Improving the Reliability of Auto-formalization for Logical Reasoning [5.119925615308174]
  Auto-formalization (AF) translates natural-language reasoning problems into solver-executable programs.<n>We propose Draft-and-Prune (D&P), an inference-time framework that improves AF-based logical reasoning via diversity and verification.<n>D&P substantially strengthens AF-based reasoning without extra supervision.
  arXiv  Detail & Related papers  (2026-03-18T00:35:14Z)
• Certainty-Validity: A Diagnostic Framework for Discrete Commitment Systems [0.0]
  "Machine learning evaluation metrics" assume that all errors are equivalent discrete commitment systems.<n>"ConfidentIncorrect" behavior is where models hallucinate structure in ambiguous data.<n>"Good training" for reasoning systems must be defined not by accuracy but by maximizing the Certainty-Validity Score.
  arXiv  Detail & Related papers  (2026-02-10T21:53:02Z)
• Pushing the Boundaries of Natural Reasoning: Interleaved Bonus from Formal-Logic Verification [49.506412445511934]
  Large Language Models (LLMs) show remarkable capabilities, yet their next-token prediction creates logical inconsistencies and reward hacking.<n>We introduce a formal logic verification-guided framework that dynamically interleaves formal symbolic verification with the natural language generation process.<n>We operationalize this framework via a novel two-stage training pipeline that synergizes formal logic verification-guided supervised fine-tuning and policy optimization.
  arXiv  Detail & Related papers  (2026-01-30T07:01:25Z)
• Are Language Models Efficient Reasoners? A Perspective from Logic Programming [109.47572890883248]
  Modern language models (LMs) exhibit strong deductive reasoning capabilities, yet standard evaluations emphasize correctness while overlooking a key aspect of human-like reasoning: efficiency.<n>We propose a framework for assessing LM reasoning efficiency through the lens of logic programming.
  arXiv  Detail & Related papers  (2025-10-29T15:30:31Z)
• 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)
• Improving AEBS Validation Through Objective Intervention Classification Leveraging the Prediction Divergence Principle [0.0]
  This work proposes a rule-based classification approach leveraging the Prediction Divergence Principle ( PDP)<n>The findings suggest that combining this approach with human labeling may enhance the transparency and consistency of classification, thereby improving the overall validation process.
  arXiv  Detail & Related papers  (2025-07-10T15:55:05Z)
• STL: Surprisingly Tricky Logic (for System Validation) [0.04301276597844757]
  Ground-truth validity of a specification, subjects' familiarity with formal methods, and subjects' level of education were found to be significant factors in determining validation correctness. Participants exhibited an affirmation bias, causing significantly increased accuracy on valid specifications, but significantly decreased accuracy on invalid specifications.
  arXiv  Detail & Related papers  (2023-05-26T21:01:26Z)
• Logical Satisfiability of Counterfactuals for Faithful Explanations in NLI [60.142926537264714]
  We introduce the methodology of Faithfulness-through-Counterfactuals. It generates a counterfactual hypothesis based on the logical predicates expressed in the explanation. It then evaluates if the model's prediction on the counterfactual is consistent with that expressed logic.
  arXiv  Detail & Related papers  (2022-05-25T03:40:59Z)

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.