Instantiation-based Formalization of Logical Reasoning Tasks using Language Models and Logical Solvers

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

The paper introduces Semantic Self-Verification (SSV), which asks an LLM to write an executable solver program and independently generate concrete positive and negative examples for each constraint. A logical solver checks those examples, and failures guide semantic repair. The claim is selective: a case marked verified is usually correct, but only a subset of cases can be verified. The abstract describes “a consistency-based approach to produce strong abstract formalizations of problems using concrete instantiations that are generated by the model and verified by the solver” (Abstract, p. 1).

technique: segmented solver program generation

What it is. SSV generates a solver-executable program P divided into initial definitions, constraints, and answer options. Each constraint has a natural-language annotation, allowing the instantiation generator to map a sentence to one code segment. The paper gives the structure as Pinit + C1 + … + CN + O1 + … + OM, with Pinit holding initial definitions and the constraints and options annotated with comments such as “#CONSTRAINT:” and “#OPTION:” (Section 2, p. 4).

Steps. (1) Prompt the LLM to generate P. (2) Feed syntax or execution errors back for error-based repair. (3) If direct generation fails, generate code compositionally for each constraint. (4) Execute P in the logical solver to obtain an answer A. The paper uses the Z3 SMT solver and 1-4 few-shot examples drawn from training datasets; these are implementation facts from Section 3, p. 5.

Verus form. Inference: translate each constraint into a Rust predicate or spec fn, and make the executable answer function carry requires/ensures. Compositional generation maps to separate Rust functions and proof lemmas. A Verus proof checks the specified predicate, whereas an LLM-generated solver program and its natural-language annotation remain proposal artifacts until manually or mechanically connected to the Rust specification.

technique: concrete positive/negative instantiation verification

What it is. For every constraint Ci, SSV asks the LLM for one positive instantiation Ip and one negative instantiation In. It checks Pinit + Ci + Ip is satisfiable and Pinit + Ci + In unsatisfiable. If all checks pass and P is well formed, SSV returns A with verification success. The paper describes the positive check as “constructing and executing the expression Pinit + Ci + Ip and checking that the solver returns SAT”, and for the negative instantiation “it checks that the expression Pinit + Ci + In is UNSAT” (Section 2, p. 4).

Steps. Parse constraints and their natural-language descriptions from P; prompt the LLM, from those descriptions and the initialization code, for one positive and one negative example each (the Related Work section, p. 7, says these are “literal assignments” generated “independently from the program constraints”); translate them to solver expressions; run SAT/UNSAT checks; return the first failing instantiation Ifail; reject verification if any check fails. Also check that P follows the specified structure, returns a single answer, and avoids degenerate expressions (tautologies or vacuous implications) (Section 2, p. 4). A constraint that cannot be expressed in the given data structures gets “NONE” and “pass” as its example (Appendix 7.2).

Verus form. Inference: represent Ip and In as concrete Rust values and prove ensures for each positive case and contradiction for each negative case. This is a finite test obligation unless the Verus predicate is quantified; passing examples alone cannot establish a universal property. Use assert and proof fn lemmas to connect each case to the abstract constraint.

Evidence and limitation. With GPT-4, Table 1 reports verification coverage from 21.7% on AR-LSAT (230 questions) to 75.2% on ProofWriter (600 test examples), with reported precision 94.0% and 98.7% on the original labels (100.0% after the authors’ own label corrections: 3 AR-LSAT, 1 FOLIO and 6 ProofWriter cases, Appendix 7.4), respectively (Table 1, p. 5; dataset sizes in Section 3, pp. 4-5). Coverage is verified cases divided by the full dataset, while precision is correct answers among cases flagged verified. The authors list as their first limitation that “Concrete instantiations are insufficient”, because examples “may not cover all aspects of a general constraint, particularly corner cases” (Section 4, p. 6).

technique: semantic repair from a failing instantiation

What it is. If verification fails, the first failing concrete case is sent with the program to a repair prompt. The LLM is asked to diagnose whether the error lies in initial definitions, constraint code, or the instantiation, then produce corrected code. The repaired program re-enters the verification loop. This is semantic repair, distinct from fixing syntax or execution errors (Section 2, p. 4).

Steps. Keep the failing Ifail; supply the initial definitions code, the constraint code with its natural-language description, and the failing instantiation expression to the LLM; generate a repair; repeat the verification loop (Figure 5 places GenInstantiations inside this loop, so instantiations are inferred again); stop at MaxRepairs. The full implementation uses MaxRepairs = 2 and Temperatures = [0, 0.3, 0.4, 0.5] (Section 3, p. 5). The text and Figure 5 line 14 attempt repair “provided no answer has been found” (A = ∅); I did not resolve how this squares with repairing after a verification failure that has an answer. If no verified answer is found across temperatures, return the best answer with verification failure; if no executable answer exists, fall back to direct LLM inference (Figure 5, p. 4).

Evidence. On AR-LSAT, the paper reports that semantic repair improves accuracy by 6.1% and temperature exploration by 10.0%; coverage gains 5.2% with repair and more than doubles with temperature exploration, rising 12.2% above an initial 10.9% (Section 3.1, p. 6). Repairs stop improving metrics beyond three attempts, while temperature gains continue to 0.6. These percentages are ablation changes on AR-LSAT, not universal improvements.

Verus form. Inference: treat Ifail as a counterexample for a failed postcondition, edit the Rust function or proof lemma, and rerun Verus. A repair loop may regenerate specifications, so VL should freeze the intended contract and permit changes only when a reviewer accepts the changed requirement.

technique: independent candidate exploration and fallback

SSV loops over temperatures; Appendix 7.6 says the computations are independent for each temperature, although Abest is shared. Each candidate program gets executed, instantiated, verified, and possibly repaired. The first answer is retained as Abest; a verified candidate returns immediately. If no candidate verifies, the algorithm returns Abest with False (Figure 5, p. 4). Runtime tests over 250 data points (50 from each of five datasets) found median 152 seconds per task, first quartile 108 s, third quartile 267 s, and mean 249 s on the stated 16-core Xeon machine (Appendix 7.6, p. 35). The paper proposes parallel temperature runs, parallel independent solver calls, and caching checks for unchanged constraints.

Verus form. Inference: parallel candidate generation can produce alternative Rust implementations, but only a Verus-verified candidate should be accepted. Caching is sound only when the specification and relevant code are unchanged; a dependency-aware build can invalidate cached proof obligations.

what is proved, measured, and trusted

Z3 proves SAT/UNSAT for supplied concrete expressions; it does not prove that the expressions capture the natural-language problem. SSV’s strong GPT-4 results are empirical: Table 1 gives 100% corrected-label precision on every dataset, but the authors report GPT-3.5 incorrect verified cases (one PrOntoQA and four ProofWriter) and explain that both program and examples can share the same error (Section 4, p. 6). GPT-3.5 coverage is zero on AR-LSAT and LogicalDeduction, with 97% average precision on the three datasets where coverage exists (Table 2, p. 7; Section 3.1, p. 6). Dataset answer corrections affect reported precision; the paper reports original and corrected values separately.

Inference: the product threat to agent-written verified Rust is a specification gap. SSV’s counterexample-guided loop can expose missing or conflated predicates, but finite examples and an LLM-generated formalization do not prove the statute or requirement. VL can adopt segmented contracts, independent positive/negative witnesses, semantic repair, and explicit coverage/precision reporting, then require Verus proofs over quantified behavior before code enters a trusted artifact.

techniques for the catalog

• segmented solver generation — emit initial definitions, separately annotated constraints, and options so each part can be checked and repaired
• positive/negative instantiation checks — require SAT for a concrete positive case and UNSAT for a concrete negative case for every constraint
• counterexample-guided semantic repair — feed the first failing instantiation back to the model and repeat bounded verification
• temperature and solver parallelism — explore independent candidate programs and parallelize independent checks, caching unchanged obligations Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “Three cases in the AR-LSAT dataset were verified correctly by our system, but were labelled with the wrong answers in the dataset.”): read the whole paper including the appendix and checked every quotation, number, page and section reference, and the technique steps against the text; changed the SAT/UNSAT quotation (the old one omitted a word), the page references for the Pinit structure (p. 4), MaxRepairs and Temperatures (p. 5), Table 2 (p. 7), and Section 4 (p. 6), the repair-prompt inputs, the instantiation-generation inputs, and added the note on the repair condition; link kept from the paper text (arXiv:2501.16961). Did not check the cited works, the prompts line by line beyond what is quoted, or the Figure 2-4 code.

Last edited: 2026-10-17