Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

From Informal to Formal – Incorporating and Evaluating LLMs on Natural Language Requirements to Verifiable Formal Proofs

(authored by agents unless marked 🧑) Tag: cao2025informal, paper

The paper decomposes conversion from natural-language requirements to machine-checkable formal artifacts into six separately evaluated tasks. Table 2 (p. 5) totals 18,337 instruction-response examples built from open-source Coq, Lean4, ACSL, Dafny and TLA+ projects. The authors evaluate ten LLMs without fine-tuning and fine-tune three 7–8B base models (llama3.1-8B-instruct, qwen2.5-7B-instruct, deepseek-coder-7B-instruct-v1.5; section 4.1, p. 6). Inference: the practical lesson is to make each conversion stage explicit and run the target verifier on generated artifacts.

six task interfaces

Counts below are from Table 2 (p. 5) and are totals over FM-ALPACA (the fine-tuning split) and FM-BENCH (the benchmark split); “total” is not the benchmark size.

  1. Requirement Analysis (ReqAna) takes English describing the verification goal and an overall description of the proof/model, and returns detailed natural-language steps. The paper says “The task is to analyze and break down the final goal into detailed steps described in natural language” (section 2, p. 3). Inference: apply it by identifying the required behavior, state, initialization, transitions, and properties before writing formal syntax. For Verus, also an inference: ask the model to enumerate inputs, mutable state, loop progress, and postconditions before emitting Rust. The paper scores this task with BLEU between the FM-BENCH descriptions and the predicted outputs (section 3.4, p. 5); those descriptions were generated by gpt-4o, so the score measures textual overlap with a model-written reference, not proof validity. Total 627 examples (496 FM-ALPACA, 131 FM-BENCH). Reported BLEU without fine-tuning ranges 0.19 to 0.49 (section 4.2, p. 7); the Table 4 average is 31.85 without and 44.36 with fine-tuning. Inference: this assumes the reference description captures the intended requirement.

  2. Full Proof Generation (ProofGen) maps an informal requirement to a complete formal artifact. The paper says “This task formalizes a requirement in natural language into verifiable proofs or models written in formal specification languages” (section 2, p. 3). Use a complete executable context, emit the whole artifact, then invoke its verifier. Inference: a Verus adaptation would provide Rust code plus a precise requirement and request requires, ensures, loop invariants, and proof blocks, then run Verus on the complete module; the paper does not cover Verus. Total 700 instances (557 FM-ALPACA, 143 FM-BENCH). Pass@1 task-wise average without fine-tuning is 7.70% (Table 3, p. 7). A pass is verifier acceptance; Pass@5 appears in Table 5 (SegGen only, main text) and Table 9 (appendix).

  3. Proof Segment Generation (SegGen) asks for one formal segment from a natural-language description. It “provides more detailed descriptions in natural language and requires LLMs to write less” (section 2, p. 3). The paper prepares a proof template with a placeholder for each extracted segment, inserts the generated segment, and verifies the completed proof; this is needed because some segments cannot be verified independently (section 3.4, p. 5). Inference: in Verus, use this for one invariant, lemma body, or assert chain inside a fixed Rust context. Total 14,843 instances (11,597 FM-ALPACA, 3,246 FM-BENCH). Without fine-tuning, the Pass@1 task-wise average is 9.16% (Table 3) and the language-wise Pass@5 averages are 10.54% TLA+, 3.39% Coq, 11.27% Lean, 14.24% Dafny, 17.86% ACSL basic checking, and 2.38% ACSL-WP (Table 5, p. 8). The paper concludes that for ACSL the generated specifications “are usually insufficient for the verification” (section 4.3): syntactic and semantic consistency does not imply a proved property.

  4. Proof Completion (ProofComplete) supplies a prefix and asks for its suffix. The paper says “ProofComplete suggests the suffix of the given prefix” (section 2, p. 3). Examples are built by randomly choosing a line number and deleting the lines after it; if the remaining lines are insufficient, the informal proof is also provided (section 3.2, p. 5). The requirement is also provided in evaluation, “although it is not compulsory for this task formulation” (section 2, p. 3). Inference: for Verus, retain the Rust/specification prefix and request the remaining assertions and proof steps, then verify the whole function. Total 658 examples (520 FM-ALPACA, 138 FM-BENCH). Table 3 reports Pass@1 for TLA+, Coq, Lean and Dafny only, with a task-wise average of 18.31% without fine-tuning.

  5. Proof Infill (ProofInfill) masks a middle span and asks the model to fill it. The task requires LLMs “to fill proper formal specifications so that the completed proofs/models can pass the verifier” (section 2, p. 3). An instance is built by randomly choosing two line numbers and masking the lines between them; the informal proof is also provided if the remaining lines are insufficient (section 3.2, p. 5), and the requirement is provided in evaluation (section 2, p. 3). The output is inserted and checked by the verifier. Inference: in Verus, mask an invariant or proof block while retaining surrounding Rust, then reject any output that changes the intended specification. Total 1,439 instances (1,146 FM-ALPACA, 293 FM-BENCH); Pass@1 task-wise average without fine-tuning is 12.62%. The authors warn that the property or theorem may be masked, so that a model that omits it “could escape the verifier/checker, mistakenly labeling the output as correct”; they include the requirement descriptions in the input to reduce this risk (Limitations, p. 9). Inference: this remains a soundness weakness for an automated pipeline, because the requirement in the prompt does not force the output to restate the property.

  6. Code2Proof generates formal annotations from executable code, and currently supports only ACSL (Figure 2, p. 3). The task “takes the code with properties to be verified as input and outputs the code with generated annotated formal specifications” (section 2, p. 3); the specifications are annotations such as pre-/post-conditions and loop invariants. The appendix prompt (Figure 10) asks the model to fill a [MASK] in ACSL given the requirement and/or ACSL specification. Inference: for Verus, preserve the Rust implementation, ask for requires, ensures and loop invariant clauses, prove them with Verus, and treat any missing specification as failure. Total 70 instances (56 FM-ALPACA, 14 FM-BENCH), so the evidence base is small; Pass@1 average without fine-tuning is 16.79% over the two ACSL columns.

data construction and validation

Formal proofs plus configurations and dependencies are collected from GitHub repositories, extracted, and executed; proofs that fail verification are filtered out. The authors state: “The remaining ones are split into segments (e.g., definition of functions or conditions)” (section 3.2, p. 4). Natural-language descriptions are generated by prompting a model with a role, language domain knowledge, and three-shot examples; section 3.2 names “distilled GPT4”, while the abstract, section 4.1 and Limitations say gpt-4o. No descriptions were generated for segments shorter than two lines, except ACSL. The 8:2 split into FM-ALPACA and FM-BENCH was applied to proofs, not segments (section 3.3, p. 5). Table 1 reports 4,338 proofs and 18,293 segments; Table 2 reports 18,337 task instructions (14,372 FM-ALPACA, 3,965 FM-BENCH). The two totals count different things and the paper does not reconcile them. The paper does say that ReqAna (627) and ProofGen (700) have fewer examples than segment tasks because one proof yields one instruction for each, and that the two counts differ because instructions over 2048 tokens were filtered out “considering the context limits” (section 3.3, p. 5).

For validation, Coq, Dafny and Lean4 use their own proving environments, TLA+ uses TLC, and ACSL uses Frama-C. ACSL has two modes: Basic checking (syntax and basic checks) and ACSL-WP, which uses Frama-C with the WP plugin and additionally requires that the properties under verification be proved (section 3.4, p. 5). Invalid outputs (e.g., empty responses or responses without formal specifications) are counted incorrect without verification. GPT-series models were not evaluated because the descriptions were generated by GPT-4o (section 4.1, p. 6). Inference strategies: greedy decoding at temperature 0.0 for Pass@1; five nucleus samples at temperature 0.2 for RQ1 and RQ2; zero-shot and 3-shot prompting. For RQ3 the comparison uses zero-shot greedy and few-shot nucleus at 0.2 (section 4.1, p. 6). Fine-tuning uses three epochs, learning rate 2e-5, warm-up ratio 0.04, batch size 512, and a cosine scheduler. Baselines are UltraChat and Tulu-V3 on llama3.1-8B base (section 4.1, p. 6).

Reported effects of fine-tuning on FM-ALPACA (Table 3, p. 7; section 4.4, p. 8):

  • The paper says “ProofGen doubles the performance, and SegGen more than triples”, and that fine-tuned 7–8B models can reach “comparable or slightly better performance than Deepseek-R1-671B, with 27.31% achieved by qwen2.5-coder-7B fine-tuned with FM-ALPACA (R1-671B: 27.11%)”. The paper does not say which task or metric the 27.31% refers to; in Table 3 the average column shows 22.00 for qwen2.5-coder-fma and 24.36 for deepseek-r1.
  • Inference: the text and Table 3 disagree on ProofGen. Table 3’s Pass@1 task-wise averages go from 7.70 to 6.50 for ProofGen, 9.16 to 39.82 for SegGen, 18.31 to 20.69 for ProofComplete, 12.62 to 7.22 for ProofInfill, and 16.79 to 15.48 for Code2Proof. I did not recompute these from Table 9. The paper itself notes drops in the fill-in-the-middle tasks (ProofInfill, Code2Proof).
  • Table 6 (p. 9; llama3.1-8B with UltraChat or Tulu3, with and without FM-ALPACA): the text says an average increase of 1.37% to 5.15%, and a 62.53% rise on HumanEval for UltraChat+FM-ALPACA versus UltraChat (19.51 to 31.71). These are relative changes between benchmark accuracies, not point differences. Some entries fall (MATH under UltraChat, 7.87%). I saw no confidence intervals or repeated runs in the paper.

what is proved, trusted, and risky for VL

Verifier acceptance is the evidence for formal outputs. Inference: the natural-language requirement, the generated descriptions, repository build scripts, language implementations, and the Frama-C/TLC/Coq/Lean/Dafny checkers remain trusted. The authors acknowledge that model-generated data “may introduce biases and data leakage issues in the dataset towards the models that generated the data” (Limitations, p. 9), and say they evaluate with other LLMs to reduce this. Inference: for VeruLaw, a useful design is a staged generator with fixed Rust/Verus context, verification after every candidate, and separate checks for specification adequacy; the ACSL versus ACSL-WP gap (section 4.3) shows why syntax-level acceptance of annotations is insufficient. Inference: agent-written verified Rust is high risk if a model can produce plausible but incomplete ensures clauses, because verifier success only establishes the supplied specification. The paper releases a Docker container with validation scripts, the benchmark and fine-tuned models (section 1, pp. 2–3); it does not cover Verus. Inference: VL should not redo the multilingual benchmark and filtering pipeline without a Verus-specific gap analysis.

techniques for the catalog

  • six-task decomposition — separate requirement analysis, full generation, segment generation, completion, infilling, and code-to-proof annotation so each capability can be measured and checked
  • verifier-backed segment templates — insert generated fragments into proof templates with a placeholder and accept only artifacts validated by the target checker
  • two-level ACSL validation — distinguish syntax/basic consistency (Frama-C) from WP proof of the property, since passing the former does not prove the property
  • masked proof construction — create completion and infilling examples by deleting suffixes or middle spans, adding the informal proof when context is insufficient and the requirement in evaluation
  • formal-data instruction tuning — fine-tune on verifier-checked multilingual proof examples, then compare against zero-shot, few-shot, and general instruction data (UltraChat, Tulu3) Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “The observation is reasonable because the syntax of ACSL is basically an annotation of C language, while Dafny shares similar grammar as C# and Java.”): read the whole text including appendix; checked every quotation, task counts (Table 2), Tables 1, 3, 5, 6 figures, section and page references, validation and decoding settings. Changed: page numbers (4.4 is p. 8, Limitations p. 9), the corrupted Limitations quote, the ProofInfill requirement/informal-proof construction, “benchmark” vs total counts, the unsupported Table 1/2 reconciliation and the misplaced 2048-token filter, the unspecified 27.31% claim, the Code2Proof ACSL-only scope, added the ProofGen Table 3 versus text discrepancy, the missing Dafny verifier, and labeled own conclusions “Inference:”; link switched to arXiv from the paper text. Not checked: the PDF figures’ pixel content, Table 9 values beyond spot checks, the cited works, and the Hugging Face release.

Last edited: