🤖 AI

Faithful Autoformalization of Natural Language Assertions

The paper introduces Monty, an autoformalization framework that improves the precision of synthesizing executable assertions from natural language by filtering LLM-generated outputs using novel conformance and validity scores, achieving up to a 20-point average precision gain over naive translation methods.

Original authors: Hongyi Liu, Madhusudan Parthasarathy, Adithya Murali

Published 2026-07-16

📖 7 min read🧠 Deep dive

CC BY 4.0

Original authors: Hongyi Liu, Madhusudan Parthasarathy, Adithya Murali

Original paper licensed under CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ This is an AI-generated explanation of the paper below. It is not written or endorsed by the authors. For technical accuracy, refer to the original paper. Read full disclaimer

The Translator's Dilemma: When Code Meets Human Words

Imagine you are building a massive digital city. To keep the traffic flowing and the buildings standing, every street corner and skyscraper needs a rulebook. In the world of software, these rulebooks are called "formal specifications." They are precise, mathematical instructions that tell a computer exactly what a piece of code is supposed to do and what it must never do. Think of them as the unbreakable laws of physics for a digital world. The problem is, writing these laws is incredibly hard. It requires a level of precision that feels like speaking a different language entirely, one that most human programmers find tedious and error-prone.

Enter the "Autoformalization" problem. This is the quest to take a human's messy, natural-language idea—like "don't let the list get too big"—and automatically translate it into that strict, mathematical code. For years, scientists have tried to use Artificial Intelligence (AI), specifically Large Language Models (LLMs), to act as translators. These AI models are like super-smart polyglots that have read almost everything ever written. They are great at guessing what a sentence means. But here is the catch: when you ask an AI to translate a vague human thought into a strict legal contract, it often hallucinates. It might invent rules that don't exist, miss a tiny detail that breaks the whole system, or confidently translate a "maybe" into a "definitely." The core question this paper tackles is: How do we trust an AI translator when the stakes are high, and the human instructions are fuzzy?

Meet Monty: The Detective Who Checks the AI's Homework

This paper introduces a new framework called Monty, a system designed to be a skeptical, detail-oriented editor for AI-generated code rules. The authors, researchers from the University of Wisconsin-Madison and the University of Illinois, realized that simply asking an AI to translate a sentence into code isn't enough. If you ask an AI to translate "the list should be empty," it might guess that means "the list has zero items" or "the list has no items at all." Both sound right, but in computer code, they might mean very different things.

Monty doesn't just trust the first answer the AI gives. Instead, it acts like a detective running a series of tests. Here is how the story unfolds:

1. The AI Generates a Crowd of Suspects
First, Monty asks a Large Language Model to translate a natural-language assertion (a human sentence) into formal code. The AI doesn't just give one answer; it generates a whole crowd of "candidate" translations. Some might be perfect, some might be slightly off, and some might be completely wrong.

2. The "Fuzz" Test: Breaking the Code
Next, Monty puts these candidate translations through a stress test called "fuzzing." Imagine a robot throwing random, wild inputs at the code to see if it crashes or behaves strangely.

If a candidate translation crashes the computer or throws an error, Monty throws it out immediately.
If the translation works but fails to match the logic of the original human sentence, it gets a low score.
Crucially, Monty doesn't assume the human sentence is correct. Sometimes, a programmer writes a rule that is actually wrong (a "buggy" rule). Monty is smart enough to realize that a "valid" translation of a "buggy" rule is still a bug. It looks for both the most likely correct translation and the most likely incorrect translation to see which one fits the context.

3. The "Clause Coverage" Check: The Reverse Translation
This is Monty's secret weapon. To check if an AI translation is truly faithful, Monty uses a clever trick called clausal coverage. It takes the AI's formal code and asks the AI to translate it back into plain English. Then, it compares this new English sentence with the original human sentence.

Did the AI miss a part of the original sentence?
Did it add something that wasn't there?
Did it change the meaning?
The AI acts as a judge, giving a score based on how well the pieces (clauses) of the two sentences match. If the back-translation is missing a key detail, the score drops, and that candidate is filtered out.

4. The Final Showdown: Active Learning
Sometimes, the AI generates two candidates that both look perfect and pass all the tests, but they mean slightly different things. This is where the "ambiguity" of human language bites back. In these rare cases, Monty doesn't guess. It uses active learning. It finds a specific scenario (a "distinguishing valuation") where the two candidates would behave differently. It then asks a human (or a simulated oracle) a simple question: "In this specific case, which rule did you actually mean?" The human picks the winner, and Monty locks in the correct translation.

What Monty Found

The researchers tested Monty on 541 different tasks involving Java code, which is a popular programming language. They used datasets that included both perfectly written rules and intentionally broken ones to see if Monty could handle the messiness of real life.

The results were promising. When they let the AI translate naturally without Monty's help, the accuracy was decent but far from perfect. For example, using a specific model called Qwen2.5-Coder, the raw AI got the translation right about 75% of the time on one dataset. But when Monty stepped in to filter and check the answers, that accuracy jumped to 91.6%. On another dataset, it went from 64% to 85%.

The paper suggests that Monty is particularly good at fixing the "precision" problem. This means that when Monty says, "Here is the correct rule," you can trust it much more than when you just ask an AI and take its first answer. It managed to do this without throwing away too many correct answers (keeping the "recall" high).

What Monty Does Not Do

It is important to know what this paper is not claiming. Monty is not a magic wand that solves every programming problem.

It does not try to figure out the high-level "intent" of a whole software project (like "build me a social media app"). It focuses strictly on translating specific, localized rules for individual pieces of code.
It does not claim to have solved the problem of ambiguity forever. Sometimes, the human input is so vague that even Monty needs a human to step in and clarify.
The authors explicitly argue against the idea that we should just assume every rule a programmer writes is correct. Many older tools assumed that if a rule was written, it must be true. Monty rejects this, showing that sometimes the goal is to find the rule that fails, proving the code is buggy.

The Bottom Line

In the end, Monty suggests that the future of writing code isn't just about asking an AI to do the work. It's about building a system where the AI generates ideas, but a smart, rigorous process checks them against reality. By combining the creativity of AI with the skepticism of testing and the precision of "reverse translation," Monty shows a path toward making software safer and more reliable, turning the messy, ambiguous thoughts of human developers into the clean, unbreakable laws of the digital world. The paper suggests that while we aren't there yet, this "check-your-work" approach is a significant step forward in making AI a trustworthy partner in software development.

Technical Summary: Faithful Autoformalization of Natural Language Assertions

Problem Statement

The paper addresses the challenge of reliable autoformalization: synthesizing executable formal assertions (e.g., in Java Modeling Language, JML) from natural-language (NL) specifications. While Large Language Models (LLMs) offer a path to bridge the gap between informal developer intent and formal specifications, current approaches suffer from two critical issues:

Unfaithfulness: LLMs often generate formalizations that do not accurately reflect the semantic content of the original NL assertion.
Ambiguity: Natural language is inherently ambiguous. Existing works often implicitly assume that the NL assertion describes a valid property of the code. However, in contexts like bug finding or testing AI-generated code, the assertion may be intended to be invalid (i.e., to reveal a failure). Assuming validity can lead to filtering out the correct formalization if the code is buggy, or accepting a formalization that fails to check the user's intent.

The goal is to produce a formalization that is faithful to the NL specification, regardless of whether the resulting assertion is valid or invalid with respect to the code implementation.

Methodology: The Monty Framework

The authors propose Monty, a framework that combines LLM generation with program testing and active learning to resolve ambiguity and ensure faithfulness. The pipeline consists of four stages:

1. Candidate Generation

Given a code module (class), method signatures, documentation, and an NL specification, an LLM is prompted to generate multiple candidate formal specifications ( $\psi_1, \dots, \psi_n$ ) in an executable logic (JML).

2. Filtering and Scoring

Candidates are evaluated using two complementary signals:

Validity Score (Execution-Level): A test generator (Randoop) creates test inputs to check the candidates.
- Syntactic Check: Ensures the code compiles.
- Fuzz-Safety Check: Ensures the assertion does not throw runtime exceptions.
- Fuzz-Semantic Check: Determines if the assertion is test-valid or test-invalid for the given method.
- Note: The framework does not discard candidates simply because they are test-invalid; it preserves them to handle cases where the user intends to find bugs.
Conformance Score (Semantic-Level): A novel metric called Clausal Coverage is used.
- The formal candidate is translated back into natural language by an LLM.
- A second LLM (acting as a judge) compares the clausal structure of this generated NL description against the original NL assertion.
- It checks for Soundness (does the description cover all clauses of the original?) and Completeness (does it contain extra/conflicting information?).
- A score in $[-1, 1]$ is assigned, where $+1$ indicates perfect conformance. Candidates below a threshold (e.g., 0.6) are discarded.

3. Decision Matrix

The system selects the "most likely faithful" formalizations by separating candidates into two buckets based on the validity check:

The candidate with the highest conformance score among those that are test-valid.
The candidate with the highest conformance score among those that are test-invalid.
This approach acknowledges that the "correct" formalization depends on the user's intent (documentation vs. bug finding) and avoids the bias of presuming validity.

4. Active Learning Disambiguation

If both a valid and an invalid candidate remain (and both have high conformance scores), the system identifies a distinguishing valuation (a specific input state) where the two candidates differ.

The system queries the user (or an oracle in evaluation) to determine which candidate satisfies the intended specification for this specific valuation.
The system then selects the corresponding formalization.

Key Contributions

Faithful Autoformalization Framework: A pipeline that generates both likely valid and likely invalid formalizations, addressing the limitation of prior work that assumes assertions must be valid.
Clausal Coverage Conformance Checking: A novel technique using LLM-as-a-Judge to evaluate semantic overlap between NL and formal assertions via round-trip translation and clause-level coverage analysis. The paper claims this outperforms standard Natural Language Inference (NLI) baselines.
Active Learning for Disambiguation: A mechanism to resolve inherent ambiguities in NL by generating specific test cases that distinguish between competing faithful formalizations.
New Benchmark Suites: The authors curated datasets containing 541 assertion-generation tasks across 22 Java collection-like classes. These include:
- C2S-Augmented: Synthetically generated NL specs from formal assertions.
- Buggy Datasets: Scenarios with buggy code or intentionally incorrect/misleading assertions.
- Manual NL Specs: Human-written specifications to test generalizability.

Experimental Results

The authors evaluated Monty on 541 tasks using various backbone LLMs (including GPT-oss, Qwen2.5-Coder, and larger models).

Precision Improvement: Monty significantly improves the precision of autoformalization compared to naive "Oneshot" LLM usage.
- On the C2S-Augmented dataset, Qwen2.5-Coder (32B) improved precision from 75% to 91.6%.
- On the Manual NL dataset, precision improved from 64.1% to 85.2%.
Recall Maintenance: The filtering process maintains high recall (e.g., 97.6% for GPT-oss on C2S-Aug), indicating that correct candidates are rarely discarded.
Robustness to Ambiguity: The framework successfully handles "Buggy" datasets where the assertion is intended to be invalid, a scenario where naive LLMs often fail or hallucinate valid assertions.
Ablation Studies:
- The Clausal Coverage method outperformed baselines (including NLI and simple round-trip checks) in AUC metrics.
- Contextual information (code signatures, docs) was shown to be critical for ranking quality.
- Active learning was invoked in a small fraction of cases (where valid/invalid candidates both passed conformance), but proved effective (100% accuracy in eligible cases for GPT-oss).

Significance and Claims

The paper claims that Monty provides a more reliable path to autoformalization by explicitly tackling the ambiguity of natural language and the uncertainty of assertion validity.

Trustworthiness: By filtering for conformance and separating valid/invalid candidates, the tool produces formalizations that are more likely to be faithful translations of developer intent.
Practicality: The approach does not require fine-tuning models; it relies on prompting, testing, and a decision matrix, making it applicable to existing LLMs.
Limitations: The authors note that the approach relies on localized NL assertions (module-level) and does not attempt to formalize high-level application intent or mine specs from unstructured documentation without a specific target method. The active learning component requires user interaction, though the system minimizes this by only querying when necessary.

The work positions itself as a step toward specification-driven development with AI, where human-readable specifications are authored and then rigorously vetted against code using autoformalization and testing.