# Natural Language Specifications in Proof Assistants

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

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 8 of its 96 references that are in the map.
- First posted on arXiv 16 May 2022.

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

- [What BERT is not: Lessons from a new suite of psycholinguistic diagnostics for language models](https://mlsanity.com/paper/1907.13528/) (2019)
- [Provable Limitations of Acquiring Meaning from Ungrounded Form: What Will Future Language Models Understand?](https://mlsanity.com/paper/2104.10809/) (2021)
- [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)
- [Certified Robustness to Programmable Transformations in LSTMs](https://mlsanity.com/paper/2102.07818/) (2021)
- [Tabled Typeclass Resolution](https://mlsanity.com/paper/2001.04301/) (2020)
- [Formalising Type-Logical Grammars in Agda](https://mlsanity.com/paper/1709.00728/) (2017)
- [The HoTT Library: A formalization of homotopy type theory in Coq](https://mlsanity.com/paper/1610.04591/) (2016)

## Built on by (most cited first, 1 of 1)

- [Trustworthy Formal Natural Language Specifications](https://mlsanity.com/paper/2310.03885/) (2023)

## 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 argues that it is possible to build support for natural language specifications within existing proof assistants, in a way that complements the principles used to establish trust and auditability in proof assistants themselves.