paper-with-me

홈 › Papers

Formal Specifications from Natural Language

2022-06-04 · Christopher Hahn, Frederik Schmitt, Julia J. Tillman, Niklas Metzger, Julian Siber, Bernd Finkbeiner

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.

📄 PDF Abstract BibTeX arXiv:2206.01962

Code (0)

등록된 구현이 없습니다.

Tasks

Automated Theorem Proving

Similar Papers 제목 키워드 기반

Doc2Spec: Synthesizing Formal Programming Specifications from Natural Language via Grammar Induction

2026-01-30 · Shihao Xia, Mengting He, Haomin Jia, Linhai Song arxiv

Ensuring that API implementations and usage comply with natural language programming rules is critical for software correctness, security, and reliability. Formal verification can provide strong guarantees but requires p…

LTLGuard: Formalizing LTL Specifications with Compact Language Models and Lightweight Symbolic Reasoning

2026-03-05 · Medina Andresel, Cristinel Mateis, Dejan Nickovic, Spyridon Kounoupidis 외 arxiv

Translating informal requirements into formal specifications is challenging due to the ambiguity and variability of natural language (NL). This challenge is particularly pronounced when relying on compact (small and medi…

Natural Language based Specification and Verification

2026-05-11 · Zhaorui Li, Chengyu Song arxiv

Recent frontier large language models (LLMs) have shown strong performance in identifying security vulnerabilities in large, mature open-source systems. As LLM-generated code becomes increasingly common, a natural goal i…

Trustworthy Formal Natural Language Specifications

2023-10-05 · Colin S. Gordon, Sergey Matskevich

Interactive proof assistants are computer programs carefully constructed to check a human-designed proof of a mathematical claim with high confidence in the implementation. However, this only validates truth of a formal …

Translation

Natural Language Specifications in Proof Assistants

2022-05-16 · Colin S. Gordon, Sergey Matskevich

Interactive proof assistants are computer programs carefully constructed to check a human-designed proof of a mathematical claim with high confidence in the implementation. However, this only validates truth of a formal …

Translation