claimcheck
A method that uses back-translation together with an independent judge mechanism to detect semantic discrepancies between LLM-generated code and formal specifications. It aims to address the gap in formal verification regarding whether a specification is faithful to the requirements.
Timeline (last 90 days)
The paper names the gap of semantic mismatch between natural language requirements and formal artifacts the 'spec formalization problem'.
The authors constructed an end-to-end benchmark covering four formal languages, including Dafny contracts, Lean 4, Isabelle, and Rocq theorem statements, totaling 3,234 lines of paired data.
One third of the samples in the benchmark are semantics-preserving rewrites of formal artifacts, with the label still being faithful, to prevent the judge from simply scoring by 'was edited'.
The core method of claimcheck is to translate the formal artifact back into natural language, and the translation model has never seen the original requirement; then an independent judge model determines whether the informal artifact and the original requirement express the same guarantee.
On the four formal languages, claimcheck achieved a macro recall improvement of 8.2 to 9.8 percentage points compared with a single call.
Even when the baseline got the same list of semantics-preserving rewrites, claimcheck still led by 4.2 to 6.0 percentage points.
Letting the judge also see the formal artifact loses 1.4 to 4.5 percentage points of performance.
Among the four judges that also see the artifact, the stronger the model, the smaller the gain from claimcheck, and the strongest judge is already close to the level of 'informed single call'.
claimcheck can be embedded in a CI pipeline as a semantic gate before formal verification, automatically triggering a semantic equivalence check.
All Facts (9)
The paper names the gap of semantic mismatch between natural language requirements and formal artifacts the 'spec formalization problem'.
50%UnverifiedThe authors constructed an end-to-end benchmark covering four formal languages, including Dafny contracts, Lean 4, Isabelle, and Rocq theorem statements, totaling 3,234 lines of paired data.
50%UnverifiedOne third of the samples in the benchmark are semantics-preserving rewrites of formal artifacts, with the label still being faithful, to prevent the judge from simply scoring by 'was edited'.
50%UnverifiedThe core method of claimcheck is to translate the formal artifact back into natural language, and the translation model has never seen the original requirement; then an independent judge model determines whether the informal artifact and the original requirement express the same guarantee.
50%UnverifiedOn the four formal languages, claimcheck achieved a macro recall improvement of 8.2 to 9.8 percentage points compared with a single call.
50%UnverifiedEven when the baseline got the same list of semantics-preserving rewrites, claimcheck still led by 4.2 to 6.0 percentage points.
50%UnverifiedLetting the judge also see the formal artifact loses 1.4 to 4.5 percentage points of performance.
50%UnverifiedAmong the four judges that also see the artifact, the stronger the model, the smaller the gain from claimcheck, and the strongest judge is already close to the level of 'informed single call'.
50%Unverifiedclaimcheck can be embedded in a CI pipeline as a semantic gate before formal verification, automatically triggering a semantic equivalence check.
50%