Natural Language Annotations for Reasoning about Program Semantics
Authors: Marco Zocca
Venue: EMNLP 2023 Findings (2023)
Keywords: program understanding
natural language reasoning
dataset
TL;DR: We introduce a dataset and annotation protocol for interpretable program understanding.

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 .

Natural Language Annotations for Reasoning about Program Semantics
Marco Zocca
UnfoldML, Göteborg, Sweden marco. wwcca@unfollmmm.ccommm com
Abstract
each el in moves is list with exactly 2 els
P1
for [i, j] in moves:
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 answer these ques- tions propose HTL, dataset and protocol for annotating programs with natural language predicates at a finer granularity than code com- ments and without relying internal compiler representations.
and the first two els of each el of moves
ar
is a non-negative integer
state has at least i+1 els
state[i].
state has least
qa
scope of and bound by for,
Two program statements S₁ and S2 annotated with one or more pre-and post-conditions. Can an au- tomatic system deduce Q2 or P1 from the remaining annotations?
Figure 1:
with missing premises (Sprague al., 2022) we ask whether it is possible to reason about programs with natural language.
The dataset is available at the following address: https://doi.orr/I1000 10.5211/2e00o0oo /t8l///eoooo.7711133 739
As a first step towards answering this ques- tion, we present bi-modal dataset, HTL ("Hoare Triples via Language"), composed of natural language predicates describing pre- and post- condition of given program expression or state- ment, paired with spans of program code.
1 Introduction
Software engineering is an interactive, social prac- tice, in which communication with peers and read- ing program code are as important not more than the act of writing code itself. Recent focus on the application of large language models to program- ming enabled the analysis and synthesis of ever- growing segments of text (both for program syn- thesis (Xu et al., 2022) and summarization (Wang al., 2021)), with helpful and remarkably human- like responses, hinting at the possibility of artificial assistants to augment human users.
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" (Tenenbaum et al., 2007) of program semanties 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 "com- ments" (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 may not coincide with program behaviour) but generally fol- low no 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 for-
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 out- put, in the form of "entailment trees" (Daavi et al., 2021), references their sources, and the like. Inspired by recent results in explainable open- domain question answering (Dalvi et al., 2021; Tafjord et al., 2021) and natural language inference

---

for v, f in zip(valids, filenames):
n_digits sum (c. isdigit( for in f)
"'e" character*
S c. ..isdigi(()
Q "'true" 'c' contains digit"
"'f' string"
s c. (.isdigit() for с in
Q "a list with 'true' at each position where contains a digit character and 'false" otherwise"
P "ffllnnames
list of strings" $ for v, f in zip (valldis,, filenames):
Q "If' is bound to each string in "filenames'"
Figure 2: A code snippet from Schuster et al. (2021) and three HTL labeled instances obtained from it. The annotation triples are presented order of inclusion the variables' lexical scope, see the Annotation Guidelines in Section 2 for details. Please refer to Appendix 5 for full description of the schema.
malizing the specification (lordache and Ciobaca, 2021) as well as advanced tooling, when implemen- tations even exist.
and {Q) S2 (R) the compound triple written [Pt] S2 { (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.
To summarize, in this paper we make the follow- ing contributions:
We introduce HTL new dataset of fine- grained natural-language annotations of pro- gram behaviour
The HTL dataset
Desiderata One our aims while preparing this dataset was that the "code" part should be straight- forward 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 com- putable ground truth. In addition, should be possible reason locally about the behavior of the statements to annotated; this restricted us to an idealized fragment of the programming language, e.g. without object class declarations and instances.
We describe the annotation protocol and tool developed to produce the dataset.
Background Hoare (1969) laid an axiomatic foundation for proving properties of computer programs, by introducing triples (written as {P) ((Q) relating precondition predicate P, a statement S and 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
Dataset construction We had few "false starts" while constructing the dataset; many of the paired code-language dataset initially evaluated (c.g. Kocetkov et al. (2022); Yin et al. (2018); Husain et al. (2019)) scraped from public software repositories and often their instances cannot be executed isolation (since that would require ex- ternal libraries or modules that are not included the dataset).
of those. The Hoare for- malism has been extended in many ways since the original publication to account for features of mod- ern programming languages such as lexical scope and recursive function calls (de Boer and Hiep, 2021). By relating pairs of triples with appropri- ate rules, Hoare logic deduces pre- and postcondi- tions of larger programs; for example, in order to compute the final posteondition of two-statement program S S2. the composition axiom of Hoare triples can then be invoked, as long as the interme- diate postcondition coincides with or implies the next precondition: in symbols, given {P.) Si {Q)
Another unsuccessful attempt was with anno- tating the language documentation pages directly (e.g. "reference" in docs. python. org); these con- tain extensive commentary but relatively few code snippets apart from the class headers and method signatures.

---

Praction offiee 055
min
max
mean
std.dev.
15-
Preconditions
0
122
20.1
22.9
Postconditions
5
142
53.5
23.7
Statements
4
501
46.9
68.4
12
14
Number annotations
Table 1: Annotation length statistics (no. of characters)
Figure 3: Annotation coverage of the dataset.
or built-in names., e.g. 'state' has at least 'i' elements, in order to later tokenize them distinct entities.
The current version of the HTL dataset builds upon the "Programming Puzzles" dataset of Schus- ter et al. (2021). Each instance in the source dataset is a Python function implemented to re- turn a Boolean indicating whether the input solves the programming puzzle or not; the code snippets in the source dataset are all on the order of a few tens of lines in length, which explains the distribu- tion of the resulting annotations in Figure 3. Some resulting instances that appear HTL can be seen in Figure 2.
Annotation tool We implemented an interac- tive code annotation tool, consisting of a browser- based frontend and server that samples from the memory- meamory-mapped source dataset and implements simple REST API for annotating single triples, and proceeding the next example (see Figure 4).
The design of the annotation UI underwent a few iterations too, in order to support a human programmer with contextual feedback and allow to build upon previous knowledge incrementally.
Apart from assert statements, the code is mostly "referentially transparent", i.e. it performs no file or socket T/O, however there are instances of in-place variable mutation!
Related Work
Datasets for program understanding Seman- tic parsing (SP) (i.e translating natural utter- formal language while preserving meaning) and program summarization (the inverse process) are well-studied problems that progressed together with the diffusion of code-natural language datasets (such as et al. (2018); Hasan et al. (2021); Lu et al. (2021); Lai et al. (2022)). Most of the larger datasets employ some form of automatic web scraping of sources that contain both code and natural-langune forum questions and answers, etc.), followed by multiple steps of de-duplication and human cura- tion; this approach trades off specificity for scale, and in general not guaranteed to contain func- tional code or informative text (compare with our desiderata in Section 2).
Annotation guidelines Following where possi- ble the protocol of Dalvi et al. (2021), authors were asked to write annotations that are:
entailments postconditions should immedi- ately follow from the statement, and precon- ditions should be immediately precedent to it,
compositional: allowing more general facts to be proven from specific ones. Considering two annotations with one span strictly con- taining the other one, the preconditions of the contained one can be taken to apply to the surrounding one as well.
descriptions (e.g. comments,
When annotation does not have pre- or post- condition, we take the empty slot shorthand for the atom: (T) S (Q) means that whenever halts Q holds; conversely, S (P))(T) [T} true for all compatible and terminating P and S.
Reasoning with natural language Bos and Markert (2005) discuss the approximate entailment problem and "distance" to entailment, but their se- mantic representation is based on first-order logic formulas and grounded with WordNet.
Since the annotations are free-text, we enclose in single quotes any references to program variables
Clark et al. (2021) demonstrate deductive rea- soning in transformer-basee language models us- ing deductive rules expressed in restricted natural language. their setting, all premises and rules must be explicitly stated construct valid training instances.
Mooe specifically, reference can substituted with the definition it points N.B.: asser are optimized away with the -0 runtime flag, and absence of side effects cannot be determined priori Python.
A entails B (written A B) if A cannot be true without B being true.

---

der setivowels: Lististel, Borr=:/'AATAtt/////000 'V', "ee 'CANe", "SSp10HUnTSHE" "No"")3 for Ziplaone1s, TEKES2I 1
ttorable
every time satisfies the predicates
for enumeratett):
Lentel
cllower "eciou" c.lower() and m- len/0 1: assert vfil =
tentvovels)
'oowe'' and 'terts' are lists Iterable
Iterable
"o' Is chargcter
riplsowels, teats):
in mumerate;t):
Lowert) "antos"
1
tente] loverc) "antou" c. Towert) 'y'
for in enurerstetris
Goweert) In "sciou" or cotovert] 'y' and
assert vi3l
returns truel 't'c' is
lenlt)
ussers vial
vowal
incremented by every time satisfies the predicanes
exsert nn Lentvl
the program sm stops 1f not equal to the length of
Figure 4: The user interface of the HTL data labeler. Top left code instance. Top right when the highlights span of code, a callback copies it to the texthox, and the user can input pre- and post-condition. After each annotation round, the updated ranges of the current annotations are superimposed on the code as a heatmap. Bottom the user hovers the highlighted spans, the backend retrieves the annotations that overlap with the cursor.
4 Discussion
(P, - Q (deduction) and P s.t. P -1 (S, Q) (abduction), similarly to recent "masked" language modeling objectives.
In summary, presented HTL new dataset of fine-grained annotations of program behaviour written in natural language and structured Hoare triples. We discussed the limitations of some cur- rent labelling approaches for program understand- ing datasets, and presented a new annotation proto- col.
By "fine-tuning" a preexisting language model such as T5 (Raffel al., 2020) with HTL we hope to leverage the model's implicit world knowledge and language proficiency (e.g. with regards to syn- onymity, polysemy etc.) which could help when aligning semantically-relatee annotations.
This work raised more questions than it an- swered; we hope the dataset we presented here serve as foundation for addressing some of the following ones.
Automatic labeling Understanding and annotat- ing program fragments is very laborious and time- consuming process. Could we delegate this task to generative language model instead?
Grounding Our dataset currently lacks a connec- tion between surface forms (program and language strings) and valuations, and only associates the two language modalities.
Limitations
Since the source dataset (Schuster et al., 2021) ad- dresses algorithm design puzzles, is implemented using functions that do not have computational side effects, does not define and use new types and classes, and additionally does not admit im- ported modules libraries external the Python standard library. Consequently our derived HTL dataset is subject the same limitations and as such its instances are not representative of many world programs.
Open-world vs. closed-world Due to the lack typing of Python code, our annotations make as- sumptions that might be unnecessarily restrictive; it would be interesting to follow previous work (Tafjord et al., 2021) and consider Unknown predi- cate valuations as well.
Training language models on HTL We conjec- ture that language model can be trained with linearized tree of triples (similarly the encoding scheme of Dalvi al. (2021)), e.g. by aiming to reconstruct a missing pre- or post-condition. In symbols, one could approximate or optimize for Q
The annotations are written by humans; as such and despite best efforts they might be noisy and an uneven standard across the corpus.

---

Ethics Statement
Zhou, Linjun Shou, Long Zhou, Michele Tufano, Ming Gong. Ming Zhou, Nan Duan, Neel Sundare- Shao Kun Deng, Shengyu Fu, and Shujie Liu. 2021. CodeXGLUE: machine learning benchmark dataset for code understanding and generation. ArXiv, abs/2102.0466h
Our dataset contains fine-grained annotations on the behaviour of program code; as such, the knowl- edge it embodies is of a very specialized nature and in particular it does not carry potentially harmful biases against any culture society. We release our HTL dataset for research purposes only.
Colin Raffel, Noam Shazeer, Adam Roberts, Kather- ine Lee, Sharan Narang, Michael Matena, Yanqi Zhou, Wei Li, and Peter J. Liu. 2020. Exploring the limits of transfer learning with unified text-to-text transformer. Journal of Machine Learning Research,
References
21(140):1-67.
Johan Bos and Katja Markert. 2005. Recognising textual entailment with logical inference. In HLT- EMNLP, pages 628-635.
Tal Schuster, Ashwin Kalyan, Alex Polozov, and Adam Tauman Kalai. 2021. Programming Puzzles. In NeurlPS: Datasets and Benchmarks Track.
Peter Clark, Oyvind Tafjord, and Kyle Richardson, 2021. Transformers as soft reasoners over language. In
Zayne Sprague, Kaj Bostrom, Swarat Chaudhuri, and Greg Durrett. 2022. Natural language deduction with incomplete information. In EMNLP, pages 8230- 8258.
IJCAI
Bhavana Dalvi, Peter Jansen, Oyvind Tafjord, Zhengnan Xie, Hannah Smith, Leighannaa Pipatanangkura, and Peter Clark. 2021. Explaining answers with entail- ment trees. In EMNLP, pages 7358-7370.
Oyvind Tafjord, Bhavana Dalvi, and Peter Clark. 2021, ProofWriter: Generating implications, proofs, and abductive statements natural language. In ACL- IJNLP (Findings), pages 3621-3634.
Frank S. de Boer and Hans-Dieter A. Hiep. 2021. Com- pleteness and complexity of reasoning about call-by- value in Hoare logic. ACM Trans. Program. Lang. Syst. 43(4).
Joshua B. Tenenbaum, Thomas L., Griffiths, and Sourabh Niyogi. 2007. Intuitive Theories as Gram- mars for Causal Inference. In Causal Learning: Psy- chology, Philosophy, and Computation. Oxford Uni- versity Press.
Masum Hasan, Tanveer Muttaqueen, Abdullah AI Ish- tiaq. Kazi Sajeed Mehrab, Md. Mahim Anjum Haque, Tahmid Hasan, Wasi Ahmad, Anindya Iqbal, and Rifat Shahriyar. 2021. CoDesc: A large code- description parallel dataset. In ACL-IJCNLP (Find- ings), pages 210-218.
Yue Wang, Weishi Wang. Shafiq Joty, and Steven C.H. Hoi. 2021. CodeT5: Identifier-aware unified pre- trained encoder-decoder models for code understand- ing and generation. In EMNLP.
Tony Hoare. 1969, An axiomatic basis for computer programming. Commun. ACM, 12(10))576-580
Frank F. Xu, Uti Alon, Graham Neubig, and Vincent Jo- sua Hellendoorn. 2022. A systematic evaluation of large language models of code. In MAPS, PLDI.
Hamel Husain, Ho-Hsiang Wu, Tiferet Gazit, Miltiadis Allamanis, and Marc Brockschmidt. 2019. Code- SearchNet challenge: Evaluating the state of seman- tic code search.
Pengeheng Yin, Bowen Deng, Edgar Chen, Bogdan Vasilescu, and Graham Neubig. 2018. Learning to mine aligned code and natural language pairs from Stack Overflow. In MSR, pages 476-486.
Viorel lordache and Stefan Ciobaca. 2021. Verifying the conversion into CNF in Dafny. In Workshop on Logic, Language, Information and Computation.
Tao Yu, Rui Zhang, Kai Yang, Michihiro Yasunaga, Dongxu Wang, Zifan Li, James Ma, Irene Li, Qingn- ing Yao, Shanelle Roman, Zilin Zhang, and Dragomir Radev. 2018. Spider: A large-scale human-labeled dataset for complex and cross-domain semantic pars- ing and text-to-SQL task. In EMNLP, pages 3911- 3921.
Denis Kocetkov, Raymond Li, Loubna Ben Allal, Jia Li, Chenghao Mou, Carlos Muñoz Ferrandis, Yacine Jer- nite, Margaret Mitchell, Sean Hughes, Thomas Wolf, Dzmitry Bahdanau, Leandro von Werra, and Harm de Vries. 2022. The Stack: TB permissively licensed source code.
Yuhang Lai, Chengxi Li, Yiming Wang, Tianyi Zhang, Ruiqi Zhong, Luke Zettlemoyer, Scott Wen tau Yih, Daniel Fried, Sida Wang, and Tao Yu. 2022. DS- 1000: A natural and reliable benchmark for data sci- ence code generation.
Shuai Lu, Daya Guo, Shuo Ren, Junjie Huang, Alexey Svyatkovskiy, Ambrosio Blanco. Colin Clement, Dawn Drain, Daxin Jiang, Duyu Tang, Ge Li, Lidong

---

A Annotation Schema
"annTriple":
posstcondi tion": "declares lambda function that returns the 'it1'th 'th element of 'kept'". ireccnniiiion" "'kept' is list".
"statement"; {
"trContent"; "lambda i: kept[i]",
"trEnd": 401,
"trStart": 384
Figure 5: An annotated triple from the FilterInts: instance
Above in Figure an example of an anno- tated triple, serialized as JSON object. The fields precondi tion and postcondition are called P and Q respectively in the main text whereas the trStart, trEnd fields are the position within the original data instance of the start and end of the highlighted code span (i.e. the trContent field which corresponds S in the Hoare triple defini- tion).


Reviews:
[{"review_id": "NDeU2Vh4gE", "reviewer": "Reviewer_nCxi", "summary": "", "questions": "A. Why 'self-contained' and 'reason locally' should be desiderata if they fundamentally limit what types of programs to annotate? As the authors claimed, \"Consequently our derived HTL dataset is subject to the same limitations and as such its instances are not representative of many real-world programs.\". If that is the case, what are the downstream impacts of this dataset?\n\nB. How can HTL augment existing large-scale bi-modal datasets scraped from GitHub? The paper conjectures that a language model can be fine-tuned with HTL but does not provide even preliminary results of how such fine-tuning can lead to a better LM.\n\nC. What are the main benefits of using natural language to annotate pre- and post-conditions if many can be easily translated to programmatic predicates? For example, in Figure 2, \" 'f' is a string\" can be easily translated to `type(f) == str`.\n\nD. Could you provide more in-depth qualitative and quantitative descriptions of HTL dataset?", "limitations": "", "rating": 3, "confidence": 3, "soundness": 3, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "We thank the reviewer for their valuable feedback and we will address their points in turn.\n\n## Reasons to reject\n\n> Lack of clear motivation for building the dataset (HTL): What are the downstream impacts of this dataset?\n\nAs we state in the introduction, one of the motivations is towards producing a model that approximates program behaviour while allowing deductive explanations for its answers. We were inspired by the work on Entailment Trees.\nWe are not presently able to comment on its downstream impact, but we view this work as somewhat fundamental and as a \"conversation starter\".\n\n> No validation of annotation quality: How reliable are the annotations?\n\nHuman-sourced annotations for this dataset require a delicate balance between \"naturalness\" and faithfulness to the source data, but we are not currently aware of how to quantitatively and systematically measure this. We would love to incorporate any suggestions on this issue.\n\n> No in-depth descriptions of the annotated dataset: What are the distributions of these annotations? Are there any patterns and categories? Any artifacts or shortcuts?\n\nThank you for this suggestion. In our final version we can include more descriptive statistics on the dataset. Indeed it would be interesting to show whether they cluster in some sense. \n\n## Questions \n\n> A. Why 'self-contained' and 'reason locally' should be desiderata if they fundamentally limit what types of programs to annotate? \n\nWe deliberately restrict the scope to a \"pure\" fragment of the Python language, i.e. in which the evaluation of statements only depends on their input and not on some background state (I/O etc.) with the purpose of aligning (labeling) the descriptive behaviour given in the annotations with its actual behaviour without any additional assumptions.  Adding external libraries would only make the evaluation harness more complex but the program semantics wouldn't be qualitatively different. On the other hand, adding global state or I/O would also complicate the semantic model, and we see this as an extension to this work.\n\n> B. How can HTL augment existing large-scale bi-modal datasets scraped from GitHub? The paper conjectures that a language model can be fine-tuned with HTL but does not provide even preliminary results of how such fine-tuning can lead to a better LM.\n\nThat's a great question which we are not prepared to answer at present. Indeed, as described in our \"false starts\" paragraph we initially tried with a scraped dataset but these make a lot of implicit assumptions (I/O, custom types, external libraries) which are hard to pin down exhaustively.\n\n> C. What are the main benefits of using natural language to annotate pre- and post-conditions if many can be easily translated to programmatic predicates? For example, in Figure 2, \" 'f' is a string\" can be easily translated to type(f) == str.\n\nIndeed, the one above can easily become a programmatic assertion, but there are cases when the annotations can provide a \"shortcut\" and would be rather cumbersome to evaluate even approximately (e.g. see file `Find files or url: /Users/marco/Documents/research/code-triples-lm/labeler-hs/out/BackwardsDigits:1_3680073601176606239_annot.jsonl` , first statement, postcondition: `'digits' is a dictionary where the keys are strings representing the English spelling of numbers and the values are the corresponding integers`)\n\n\n> D. Could you provide more in-depth qualitative and quantitative descriptions of HTL dataset?\n\nYes, we will include more dataset statistics in the final version.\n\n## Presentation improvements\n\n> Section 2, Dataset construction: The narrative can be straight to the point. Explain why you chose \"Programming Puzzles\" first and then exclude other alternatives.\n\nWe deliberately included our \"false starts\" to document our process and in the hope to inform others who might be interested in constructing a similar datasets.", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "+ A new bi-modal dataset that fills in the gap between informal annotations (e.g., code comments) and formal annotations (e.g., programmatic predicates)", "reasons_to_reject": "- Lack of clear motivation for building the dataset (HTL): What are the downstream impacts of this dataset? \n- No validation of annotation quality: How reliable are the annotations?\n- No in-depth descriptions of the annotated dataset: What are the distributions of these annotations? Are there any patterns and categories? Any artifacts or shortcuts?", "questions_to_authors": "A. Why 'self-contained' and 'reason locally' should be desiderata if they fundamentally limit what types of programs to annotate? As the authors claimed, \"Consequently our derived HTL dataset is subject to the same limitations and as such its instances are not representative of many real-world programs.\". If that is the case, what are the downstream impacts of this dataset?\n\nB. How can HTL augment existing large-scale bi-modal datasets scraped from GitHub? The paper conjectures that a language model can be fine-tuned with HTL but does not provide even preliminary results of how such fine-tuning can lead to a better LM.\n\nC. What are the main benefits of using natural language to annotate pre- and post-conditions if many can be easily translated to programmatic predicates? For example, in Figure 2, \" 'f' is a string\" can be easily translated to `type(f) == str`.\n\nD. Could you provide more in-depth qualitative and quantitative descriptions of HTL dataset?", "paper_topic_and_main_contributions": "This paper presents a new dataset of **natural-language annotations** of program semantics (in the forms of pre- and post-conditions).", "excitement": 3, "reproducibility": null, "ethical_concerns": "No", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {}, "extra_text": {"Typos_Grammar_Style_and_Presentation_Improvements": "- Section 2, Dataset construction: The narrative can be straight to the point. Explain why you chose \"Programming Puzzles\" first and then exclude other alternatives.\n- Figure 3: Using a pie chart would be clearer."}}, {"review_id": "Y0fJXCe7y6", "reviewer": "Reviewer_9DAE", "summary": "", "questions": "A: In your annotation tool, is it possible to select previous annotations (by span) and revise them?", "limitations": "", "rating": 3, "confidence": 3, "soundness": 3, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "We thank the reviewer for their valuable feedback and we will address their concerns in turn.\n\n## Reasons to reject\n\n> the dataset (from what I can tell) appears to cover only 20 programs of the source dataset's ~400 (Schuster et al., 2021). \n\nWe are actively working on an extended version of this dataset aiming to distribute it with the final version of the paper.\n\n## Questions\n\n> A is it possible to select previous annotations (by span) and revise them?\n\nThat's an excellent suggestion! Not possible at present; any edits are done in the JSONL annotation files by hand.\n\n\n## Presentation improvements\n\n> There are two orphans (single trailing lines across a page boundary): one on line 131 and one on line 270.\nWe will fix.\n\n> Please include some data statistics - at least the number of annotated triples + programs. The distribution of annotated code span lengths would be nice to see.\nWe will add plots with more descriptive statistics on the dataset.\n\n> It's a little annoying to have to download the files individually from the Zenodo interface - it would be good to also provide them as a single archive!\nGreat suggestion, we will upload a new version with a zipped archive. The dataset link we provided will always point to the latest version.", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "As the authors note in their motivation, scraping open-source repositories for comments leads to a few issues with the resulting data: comments don't cover all semantic levels of detail, and open-source projects often have complex dependencies that make it difficult to execute them in order to obtain ground-truth semantics. The proposed annotation scheme addresses the former, and the latter problem is addressed (at least in the authors' HTL dataset) by choosing to annotate standalone programs. In principle, addressing these issues should make the resulting resource useful to the community.", "reasons_to_reject": "I don't see any issues in the proposed annotation scheme fundamental enough to merit rejection. However, the dataset (from what I can tell) appears to cover only 20 programs of the source dataset's ~400 (Schuster et al., 2021). Based on the histogram in Figure 3, the dataset as a whole contains 209 annotated triples. This restricted scale limits the usefulness of the primary contribution.", "questions_to_authors": "A: In your annotation tool, is it possible to select previous annotations (by span) and revise them?", "paper_topic_and_main_contributions": "This paper's main contribution is a dataset containing fragments of standalone Python programs annotated with natural language preconditions and postconditions in a manner analogous to Hoare triples. The authors also contribute their annotation tool.\n\nThis resource is intended to support the development of programming assistants with improved understanding of code semantics. From the structure of the data, it appears the authors envision a system with the ability to infer an informal \"mental model\" of the behavior of a piece of code, and interrogate that model at various levels of granularity to provide improved consistency and/or explainability.", "excitement": 3, "reproducibility": 5, "ethical_concerns": "No", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {}, "extra_text": {"Typos_Grammar_Style_and_Presentation_Improvements": "There are two orphans (single trailing lines across a page boundary): one on line 131 and one on line 270.\n\nPlease include some data statistics - at least the number of annotated triples + programs. The distribution of annotated code span lengths would be nice to see.\n\nIt's a little annoying to have to download the files individually from the Zenodo interface - it would be good to also provide them as a single archive!"}}, {"review_id": "frWd8cEKmp", "reviewer": "Reviewer_Q8NV", "summary": "", "questions": "A. The annotation in Figure 2 looks like pseudo code instead of natural language. Have you found any linguistically interesting annotations that do not look like templates? ", "limitations": "", "rating": 2, "confidence": 2, "soundness": 4, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "We thank the reviewer for their valuable feedback and we will address their points in turn:\n\n## Reasons to reject\n\n>   The motivation is unclear to me, at least from a practical engineering perspective (e.g., to build an actually useable system). As the authors pointed out in L120, it was actually unclear how such a system would scale to more general general applications that have external libraries, which are very common in real-life applications.\n\nSince we are presenting a resource paper, we err on the conservative side with our claims and only speculate that this style of dataset could be useful for deducing program behaviour in a setting similar to that of \"Entailment trees\". We are still quite a way off from substantiating claims that have engineering relevance.\n\nMost programming languages have a \"standard library\" which is in scope by default. In Python's case, this is particularly extensive, and together with the language itself already enable one to write very rich programs (with data structures, I/O etc.).\nHowever here we intentionally focus on a \"pure\" subset of the base language, i.e. on computations that have a deterministic output (i.e. independent of the background state of the program or operating system), to align with the capabilities of the Formal Verification community that focuses on Hoare logic (e.g. inferring program invariants of loops) .\n\n\n>    There might be computational linguistic/cognitive science motivations, though, and I am not qualified to judge. I am a bit worried that, by restricting our attention to a closed environment, we are missing the opportunity of collecting data on how language can be used to describe program semantics in a wider range of context.\n\nSince natural language annotations of programs do not naturally have an unambiguous interpretation, here we focus on aligning them to program fragments that do. \nCode that imports external libraries is not fundamentally different from \"vanilla Python\" from an interpretation standpoint; only its evaluation harness is more technically involved.  The reviewer's concerns about applicability to in-the-wild code are legitimate, but we think that addressing those would be an extension of this work.\n\n\n## Questions\n\n> A.The annotation in Figure 2 looks like pseudo code instead of natural language. Have you found any linguistically interesting annotations that do not look like templates?\n\nYes, sometimes, e.g. in file `Find files or url: /Users/marco/Documents/research/code-triples-lm/labeler-hs/out/AnyTriangle:3_3753893779450932199_annot.jsonl` given the expression `a != b != c != a`  we see the postcondition `'True' if 'a' and 'b' and 'c' all have distinct values`. However producing this dataset requires a balancing act between \"naturalness\" and faithfulness, which is why many of the annotations indeed look generated by a template.", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "The authors contributed a dataset and an annotation protocol. \n", "reasons_to_reject": "- The motivation is unclear to me, at least from a practical engineering perspective (e.g., to build an actually useable system). As the authors pointed out in L120, it was actually unclear how such a system would scale to more general general applications that have external libraries, which are very common in real-life applications. \n- There might be computational linguistic/cognitive science motivations, though, and I am not qualified to judge. I am a bit worried that, by restricting our attention to a closed environment, we are missing the opportunity of collecting data on how language can be used to describe program semantics in a wider range of context. ", "questions_to_authors": "A. The annotation in Figure 2 looks like pseudo code instead of natural language. Have you found any linguistically interesting annotations that do not look like templates? ", "paper_topic_and_main_contributions": "The paper proposes an annotation tool and protocal to annotate program semantics with natural language.", "excitement": 2, "reproducibility": null, "ethical_concerns": "No", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {}, "extra_text": {}}]

Author rebuttal:

Meta-review: The paper contributes a dataset containing fragments of Python programs annotated with natural language preconditions and postconditions.

This type of dataset is novel and fills a gap among other existing datasets.

The actual potential applications of this type of dataset are left unclear in the paper. 
The dataset itself is also somewhat small, which restricts its usefulness, and lacks evaluation of annotation quality.
Decision: Accept-Findings