Natural Language Annotations for Reasoning about Program Semantics (2023)

Abstract: By grounding natural language inference in code (and vice versa), researchers aim to create programming assistants that explain their work, are “coachable” and can surface any gaps in their reasoning. Can we deduce automatically interesting properties of programs from their syntax and common-sense annotations alone, without resorting to static analysis? How much of program logic and behaviour can be captured in natural language? To stimulate research in this direction and attempt to answer these questions we propose HTL, a dataset and protocol for annotating programs with natural language predicates at a finer granularity than code comments and without relying on internal compiler representations. The dataset is available at the following address: https://doi.org/10.5281/zenodo.7893113 .

## introduction software engineering is an interactive, social practice, in which communication with peers and reading program code are as important if not more than the act of writing code itself. recent focus on the application of large language models to programming enabled the analysis and synthesis of evergrowing segments of text (both for program synthesis @xcite and summarization @xcite ), with helpful and remarkably humanlike responses, hinting at the possibility of artificial assistants to augment human users. a common issue with generative models of text is that their output cannot be explicitly controlled, and as such it may contain factual inaccuracies, copies of the training set, etc. it is desirable, then, that such models produce explanations of their output, in the form of "entailment trees" @xcite , references to their sources, and the like. inspired by recent results in explainable opendomain question answering @xcite and natural language inference for [i, j] in moves: state with missing premises @xcite we ask whether it is possible to reason about programs with natural language. as a first step towards answering this question, we present a bi-modal dataset, htl ("hoare triples via language"), composed of natural language predicates describing a pre-and postcondition of a given program expression or statement, paired with spans of program code. by asking practitioners to produce behavioural annotations of statements and larger blocks of code as they would communicate to a mentee, we aim to capture "intuitive theories" @xcite of program semantics in language, i.e. sketches of causal knowledge that can guide deduction and inform explanation of results. a natural language approximation of program semantics aims to fill the gap between code "comments" (as programmers usually attach to functions or module headers) and exact formal methods. on one hand, comments can be highly informative about programmer intent (which may or may not coincide with program behaviour) but generally follow no set quality standard and contain jargon and abbreviations; on the other, formal methods such as static analysis and symbolic execution provide sound approximations but require expertise in for-for v, f in zip(valids , filenames ): @xmath0. isdigit () for c in f) p : " c is a character " s : c . isdigit () q : " true if c contains a digit " p : " f is a string " s : c . isdigit () for c in f q : " a list with true at each position where f contains a digit character and ↩→ false otherwise " p : " filenames is a list of strings " s : for v , f in zip ( valids , filenames ) : q : " f is bound to each string in filenames " malizing the specification @xcite as well as advanced tooling, when implementations even exist. to summarize, in this paper we make the following contributions: background hoare (1969) laid an axiomatic foundation for proving properties of computer programs, by introducing triples (written as {p } s {q} ) relating a precondition predicate p , a statement s and a postcondition predicate q that results from executing the statement (provided this terminates). it is worth noting that predicates p and q can apply either to individual variables in the program or to sets of those. the hoare formalism has been extended in many ways since the original publication to account for features of modern programming languages such as lexical scope and recursive function calls @xcite . by relating pairs of triples with appropriate rules, hoare logic deduces pre-and postconditions of larger programs; for example, in order to compute the final postcondition of a two-statement program s 1 ; s 2 , the composition axiom of hoare triples can then be invoked, as long as the intermediate postcondition coincides with or implies the next precondition: in symbols, given {p 1 } s 1 {q} and {q} s 2 {r} , the compound triple is written {p 1 } s 1 ; s 2 {r} . in the example of figure 1 , the two triples can be composed because the second one appears in the lexical scope introduced by the first one. the htl dataset desiderata one of our aims while preparing this dataset was that the "code" part should be straightforward to verify. the source data should then be made of code that is self-contained (i.e. needs no external libraries) and it should be efficiently computable as a ground truth. in addition, it should be possible to reason locally about the behavior of the statements to be annotated; this restricted us to an idealized fragment of the programming language, e.g. without object class declarations and instances. ## discussion in summary, we presented htl , a new dataset of fine-grained annotations of program behaviour written in natural language and structured as hoare triples. we discussed the limitations of some current labelling approaches for program understanding datasets, and presented a new annotation protocol. this work raised more questions than it answered; we hope the dataset we presented here can serve as a foundation for addressing some of the following ones. grounding our dataset currently lacks a connection between surface forms (program and language strings) and valuations, and only associates the two language modalities. open-world vs. closed-world due to the lack of typing of python code, our annotations make assumptions that might be unnecessarily restrictive; it would be interesting to follow previous work @xcite and consider unknown predicate valuations as well. training language models on htl we conjecture that a language model can be trained with a linearized tree of triples (similarly to the encoding scheme of @xcite ), e.g. by aiming to reconstruct a missing pre-or a post-condition. in symbols, one could approximate or optimize for q s.t. (p, s) q (deduction) and p s.t. p (s, q) (abduction), similarly to recent "masked" language modeling objectives. by "fine-tuning" a preexisting language model such as t5 @xcite with htl we hope to leverage the model's implicit world knowledge and language proficiency (e.g. with regards to synonymity, polysemy etc.) which could help when aligning semantically-related annotations. automatic labeling understanding and annotating program fragments is a very laborious and timeconsuming process. could we delegate this task to a generative language model instead?