Faithful Autoformalization of Natural Language Assertions

• URL: http://arxiv.org/abs/2607.13303v2
• Date: Thu, 16 Jul 2026 21:38:03 GMT
• Title: Faithful Autoformalization of Natural Language Assertions
• Abstract summary: We present Monty: an autoformalization framework for assertions.<n>Our techniques are based on filtering formalizations using a novel conformance score metric.<n>We show that our technique produces the ground truth more reliably than when using LLMs naively to translate assertions.
• Score: 2.8921494813790094
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Formal contracts are essential for software testing and verification, yet writing them remains labor-intensive and error-prone. LLMs offer a promising path toward autoformalization: synthesizing executable assertions from natural-language specifications and thereby bridging the gap between informal developer intent and formal executable specifications. We present Monty: an autoformalization framework for assertions that tackles the challenges of expectations of validity of assertions and ambiguity in natural-language. Our techniques are based on filtering formalizations using a novel conformance score metric and validity scores obtained from testing the code against formalized assertions. We evaluate our approach on 541 assertion-generation tasks derived from 22 collection-like Java classes, and show that our technique produces the ground truth more reliably (improving upto 20 points in precision on average) than when using LLMs naively to translate assertions.

Related papers

• Beyond Compilation: Evaluating Faithful Natural-Language-to-Lean Statement Formalization [10.775710068605006]
  We study faithful statement formalization as both an evaluation problem and a bottleneck-attribution problem.<n>A full tool-augmented agent reaches 89.5% compilation but only 60.5% consensus faithfulness, exposing a 29.0-point compile-pass but consensus-unfaithful gap.
  arXiv  Detail & Related papers  (2026-06-30T00:27:53Z)
• VASO: Formally Verifiable Self-Evolving Skills for Physical AI Agents [57.240036084348354]
  We introduce VASO, a framework for verification-guided self-evolution of robot skill contracts.<n>VASO verifies logically inconsistent skill contracts, then verifies plans induced by the skill against global and local temporal specifications.<n>On Clearpath Jackal and PX4 quadcopter tasks, VASO reaches 97.2% formal-specification compliance using fewer than 100 optimization samples.
  arXiv  Detail & Related papers  (2026-06-03T20:02:35Z)
• Neuroforger: certified violation witnesses for smart contracts verification via LLMs [0.0]
  Recent large language models (LLMs) incorporate reasoning capabilities that allow them to perform well in predicting whether a smart contract respects a certain property.<n>We introduce a new formal specification language that extends Solidity with abstract types.<n>We design a workflow that combines LLMs with type checking and concrete execution to generate and validate violation witnesses.
  arXiv  Detail & Related papers  (2026-05-29T14:54:51Z)
• From Natural Language to Verified Code: Toward AI Assisted Problem-to-Code Generation with Dafny-Based Formal Verification [0.30915521808748864]
  Large Language Models show promise in automated software engineering, yet their guarantee of correctness is frequently undermined by erroneous or hallucinated code.<n>We provide the NaturalLanguage2VerifiedCode dataset: a collection of 60 complex algorithmic problems.<n>We evaluate 11 randomly selected problem sets across seven open-weight LLMs using a tiered prompting strategy.<n>Our results show that while contextless prompting leads to near-universal failure, structural anchors and iterative self-healing facilitate a dramatic performance turnaround.
  arXiv  Detail & Related papers  (2026-04-24T14:28:10Z)
• 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)
• Autoformalizer with Tool Feedback [52.334957386319864]
  Autoformalization addresses the scarcity of data for Automated Theorem Proving (ATP) by translating mathematical problems from natural language into formal statements.<n>Existing formalizer still struggles to consistently generate valid statements that meet syntactic validity and semantic consistency.<n>We propose the Autoformalizer with Tool Feedback (ATF), a novel approach that incorporates syntactic and consistency information as tools into the formalization process.
  arXiv  Detail & Related papers  (2025-10-08T10:25:12Z)
• Do What? Teaching Vision-Language-Action Models to Reject the Impossible [53.40183895299108]
  Vision-Language-Action (VLA) models have demonstrated strong performance on a range of robotic tasks.<n>We propose Instruct-Verify-and-Act (IVA), a framework that detects when an instruction cannot be executed due to a false premise.<n>Our experiments show that IVA improves false premise detection accuracy by 97.56% over baselines.
  arXiv  Detail & Related papers  (2025-08-22T10:54:33Z)
• Re:Form -- Reducing Human Priors in Scalable Formal Software Verification with RL in LLMs: A Preliminary Study on Dafny [78.1575956773948]
  Large Language Models (LLMs) trained with Reinforcement Learning (RL) face a significant challenge: their verification processes are neither reliable nor scalable.<n>A promising yet largely uncharted alternative is formal language-based reasoning.<n>Grounding LLMs in rigorous formal systems where generative models operate in formal language spaces (e.g., Dafny) enables the automatic and mathematically provable verification of their reasoning processes and outcomes.
  arXiv  Detail & Related papers  (2025-07-22T08:13:01Z)
• Localizing Factual Inconsistencies in Attributable Text Generation [74.11403803488643]
  We introduce QASemConsistency, a new formalism for localizing factual inconsistencies in attributable text generation.<n>We show that QASemConsistency yields factual consistency scores that correlate well with human judgments.
  arXiv  Detail & Related papers  (2024-10-09T22:53:48Z)
• Evaluating LLM-driven User-Intent Formalization for Verification-Aware Languages [6.0608817611709735]
  We propose a metric for evaluating the quality of specifications for verification-aware languages. We show that our metric agrees closely on a human-labeled dataset of Dafny specifications for the popular MBPP code-generation benchmark. We also outline formal verification challenges that need to be addressed to apply the technique more widely.
  arXiv  Detail & Related papers  (2024-06-14T06:52:08Z)
• Reliable Evaluation and Benchmarks for Statement Autoformalization [18.218951526592914]
  We present a comprehensive approach combining improved metrics, robust benchmarks, and systematic evaluation.<n>First, we introduce BEq+, an automated metric that correlates strongly with human judgment, along with ProofNetVerif, a new dataset for assessing the quality of evaluation metrics.<n>We develop two new autoformalization benchmarks: ProofNet#, a corrected version of ProofNet, and RLM25, with 619 new pairs of research-level mathematics from six formalization projects.
  arXiv  Detail & Related papers  (2024-06-11T13:01:50Z)
• SAGA: Summarization-Guided Assert Statement Generation [34.51502565985728]
  This paper presents a novel summarization-guided approach for automatically generating assert statements. We leverage a pre-trained language model as the reference architecture and fine-tune it on the task of assert statement generation.
  arXiv  Detail & Related papers  (2023-05-24T07:03:21Z)

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.