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). Sign in to comment.