REVIEW 9 cited by
Formal Specifications from Natural Language
Not yet reviewed by Pith; the record is open.
This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.
SPECIMEN: schema-true, not a live event
T0 review · schema-true
One-sentence machine reading of the paper's core claim.
pith:XXXXXXXX · record.json · timestamp
Signed reviews
read the original abstract
We study the generalization abilities of language models when translating natural language into formal specifications with complex semantics. In particular, we fine-tune language models on three datasets consisting of English sentences and their corresponding formal representation: 1) regular expressions (regex), frequently used in programming and search; 2) First-order logic (FOL), commonly used in software verification and theorem proving; and 3) linear-time temporal logic (LTL), which forms the basis for industrial hardware specification languages. Our experiments show that, in these diverse domains, the language models maintain their generalization capabilities from pre-trained knowledge of natural language to generalize, e.g., to new variable names or operator descriptions. Additionally, they achieve competitive performance, and even outperform the state-of-the-art for translating into regular expressions, with the benefits of being easy to access, efficient to fine-tune, and without a particular need for domain-specific reasoning.
Forward citations
Cited by 9 Pith papers
-
HybridProver: Augmenting Theorem Proving with LLM-Driven Proof Synthesis and Refinement
A dual-model framework that extracts proof sketches from whole-proof candidates and refines them with a tactic model and Sledgehammer, reaching 59.4 percent on miniF2F in Isabelle.
-
Surfacing the Unsaid: CUE-Bench for Affective Stance in Chinese Discourse
CUE-Bench provides 51,823 Chinese discourse instances annotated with a nine-way Affective Stance defined by explicit-implicit polarity, plus pragmatic intent and fine-grained emotion labels.
-
Lost in Translation? Converting RegExes for Log Parsing into Dynatrace Pattern Language
Reptile converts 73.7% of real-world log-parsing RegExes into DPL with test-validated semantic equivalence, and its GPT-4 pattern optimization reaches an average F1-score of 0.91 and MCC of 0.92 across five high-level...
-
CP-Model-Zoo: A Natural Language Query System for Constraint Programming Models
CP-Model-Zoo retrieves the most relevant MiniZinc model from a pool of 67 problems using text embeddings, with mean reciprocal rank between 0.87 and 1.00 in the paper's experiments.
-
Requirements Development and Formalization for Reliable Code Generation: A Multi-Agent Vision
The paper proposes ReDeFo, a multi-agent pipeline that uses formal specifications and verification to generate reliable code from natural language requirements.
-
Towards Specification-Driven LLM-Based Generation of Embedded Automotive Software
A feasibility study in which GPT-4 and GPT-3.5 generated C code for three Scania automotive modules, and some of that code passed Frama-C verification against hand-derived ACSL specifications without iterative feedback.
-
Semiotic logical hexagon theory for LLM logical reasoning
Applying the classical logical hexagon to structure proposition meanings before deduction improves LLM logical reasoning accuracy by about 2.4 to 2.7 points on average across three model backbones.
-
Working Document -- Formalising Software Requirements with Large Language Models
The paper surveys 94 papers on LLM-assisted formalisation of software requirements, organised around formalisation, traceability, formal methods, and UTP/institutions.
-
A Short Survey on Formalising Software Requirements using Large Language Models
A survey summarizing 35 papers on using LLMs to formalize software requirements, but it contains no new experimental results and its classification tables have errors.
Discussion (0). Continue with ORCID to comment.