REVIEW 4 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
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 4 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.
-
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...
-
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.
-
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.