# Faithful Autoformalization of Natural Language Assertions

arXiv: https://arxiv.org/abs/2607.13303 · HTML: https://mlsanity.com/paper/2607.13303/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 17 of its 70 references that are in the map.
- First posted on arXiv 14 Jul 2026.

## Builds on (most cited first, 17 of 17)

- [Judging LLM-as-a-Judge with MT-Bench and Chatbot Arena](https://mlsanity.com/paper/2306.05685/) (2023)
- [A large annotated corpus for learning natural language inference](https://mlsanity.com/paper/1508.05326/) (2015)
- [Qwen2.5-Coder Technical Report](https://mlsanity.com/paper/2409.12186/) (2024)
- [nl2spec: Interactively Translating Unstructured Natural Language to Temporal Logics with Large Language Models](https://mlsanity.com/paper/2303.04864/) (2023)
- [Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification](https://mlsanity.com/paper/2404.00762/) (2024)
- [SpecGen: Automated Generation of Formal Program Specifications via Large Language Models](https://mlsanity.com/paper/2401.08807/) (2024)
- [Formal Specifications from Natural Language](https://mlsanity.com/paper/2206.01962/) (2022)
- [AssertLLM: Generating Hardware Verification Assertions from Design Specifications via Multi-LLMs](https://mlsanity.com/paper/2411.14436/) (2024)
- [Lessons from the Use of Natural Language Inference (NLI) in Requirements Engineering Tasks](https://mlsanity.com/paper/2405.05135/) (2024)
- [Intent Formalization: A Grand Challenge for Reliable Coding in the Age of AI Agents](https://mlsanity.com/paper/2603.17150/) (2026)
- [Little Tricky Logic: Misconceptions in the Understanding of LTL](https://mlsanity.com/paper/2211.01677/) (2022)
- [Beyond Postconditions: Can Large Language Models infer Formal Contracts for Automatic Software Verification?](https://mlsanity.com/paper/2510.12702/) (2025)
- [AutoReSpec: A Framework for Generating Specification using Large Language Models](https://mlsanity.com/paper/2604.03758/) (2026)
- [Enhancing LLM-based Specification Generation via Program Slicing and Logical Deletion](https://mlsanity.com/paper/2509.09917/) (2025)
- [Doc2Spec: Synthesizing Formal Programming Specifications from Natural Language via Grammar Induction](https://mlsanity.com/paper/2602.04892/) (2026)
- [Choose, Don't Label: Multiple-Choice Query Synthesis for Program Disambiguation](https://mlsanity.com/paper/2604.08792/) (2026)
- [SpecSyn: LLM-based Synthesis and Refinement of Formal Specifications for Real-world Program Verification](https://mlsanity.com/paper/2604.21570/) (2026)

## Built on by (most cited first, 1 of 1)

- [claimcheck: Measuring and Improving Specification Faithfulness](https://mlsanity.com/paper/2610.17358/) (2026)

## Abstract (arXiv)

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.