# Trustworthy Formal Natural Language Specifications

arXiv: https://arxiv.org/abs/2310.03885 · HTML: https://mlsanity.com/paper/2310.03885/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 14 of its 142 references that are in the map.
- First posted on arXiv 5 Oct 2023.

## Builds on (most cited first, 14 of 14)

- [Attention Is All You Need](https://mlsanity.com/paper/1706.03762/) (2017)
- [What BERT is not: Lessons from a new suite of psycholinguistic diagnostics for language models](https://mlsanity.com/paper/1907.13528/) (2019)
- [Autoformalization with Large Language Models](https://mlsanity.com/paper/2205.12615/) (2022)
- [Language models are not naysayers: An analysis of language models on negation benchmarks](https://mlsanity.com/paper/2306.08189/) (2023)
- [The Parallel Meaning Bank: Towards a Multilingual Corpus of Translations Annotated with Compositional Meaning Representations](https://mlsanity.com/paper/1702.03964/) (2017)
- [Sorting through the noise: Testing robustness of information processing in pre-trained language models](https://mlsanity.com/paper/2109.12393/) (2021)
- [A Survey and Classification of Controlled Natural Languages](https://mlsanity.com/paper/1507.01701/) (2015)
- [Limits for Learning with Language Models](https://mlsanity.com/paper/2306.12213/) (2023)
- [A CCG-Based Version of the DisCoCat Framework](https://mlsanity.com/paper/2105.07720/) (2021)
- [Little Tricky Logic: Misconceptions in the Understanding of LTL](https://mlsanity.com/paper/2211.01677/) (2022)
- [Tabled Typeclass Resolution](https://mlsanity.com/paper/2001.04301/) (2020)
- [Formalising Type-Logical Grammars in Agda](https://mlsanity.com/paper/1709.00728/) (2017)
- [Towards Property-Based Tests in Natural Language](https://mlsanity.com/paper/2202.03616/) (2022)
- [Natural Language Specifications in Proof Assistants](https://mlsanity.com/paper/2205.07811/) (2022)

## Abstract (arXiv)

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 claim, which may have been mistranslated from a claim made in natural language. This is especially problematic when using proof assistants to formally verify the correctness of software with respect to a natural language specification. The translation from informal to formal remains a challenging, time-consuming process that is difficult to audit for correctness. This paper shows that it is possible to build support for specifications written in expressive subsets of natural language, within existing proof assistants, consistent with the principles used to establish trust and auditability in proof assistants themselves. We implement a means to provide specifications in a modularly extensible formal subset of English, and have them automatically translated into formal claims, entirely within the Lean proof assistant. Our approach is extensible (placing no permanent restrictions on grammatical structure), modular (allowing information about new words to be distributed alongside libraries), and produces proof certificates explaining how each word was interpreted and how the sentence's structure was used to compute the meaning. We apply our prototype to the translation of various English descriptions of formal specifications from a popular textbook into Lean formalizations; all can be translated correctly with a modest lexicon with only minor modifications related to lexicon size.