# miniCodeProps

By: [Evan Lohn](https://www.evanlohn.com/) `<evanlohn@cmu.edu>` and [Sean Welleck](https://wellecks.com/) `<swelleck@andrew.cmu.edu>`

We collect a variety of programs and associated properties from the Tons of Inductive Problems dataset and translate them into Lean 4. Each example of a property and its associated program(s) can then be used to evaluate the capabilities of agents that prove formal properties of code in Interactive Theorem Prover (ITP) environments. 



## Motivation


1. **For what purpose was the dataset created?** *(Was there a specific task in mind? Was there a specific gap that needed to be filled? Please provide a description.)*
    
    The dataset was created to be used as a benchmark for formal theorem proving agents, specifically targeting capability to prove properties of code in Lean 4. It is intended to be used similarly to [miniF2F](https://arxiv.org/abs/2109.00110), but in the domain of proving code properties rather than mathematical theorems.

1. **Who created this dataset (e.g., which team, research group) and on behalf of which entity (e.g., company, institution, organization)?**
    
    This dataset was created by Evan Lohn and Sean Welleck, a graduate student and professor respectively at Carnegie Mellon University (CMU).

1. **Who funded the creation of the dataset?** *(If there is an associated grant, please provide the name of the grantor and the grant name and number.)*
    
    Lohn was funded through the Computer Science Department at CMU to create this dataset.

1. **Any other comments?**
    
    None





## Composition


1. **What do the instances that comprise the dataset represent (e.g., documents, photos, people, countries)?** *(Are there multiple types of instances (e.g., movies, users, and ratings; people and interactions between them; nodes and edges)? Please provide a description.)*
    
    Each instance is a textual statement of a code property in the form of a theorem definition in Lean 4, paired with relevant information needed to fully define the theorem in Lean 4. This additional information includes the text of all functions and properties referenced in the theorem definition, as well as the locations in the source files (provided alongside the dataset) for the supporting functions and properties.


1. **How many instances are there in total (of each type, if appropriate)?**
    
    The dataset contains 177 instances at the time of writing. These instances are further split into 3 categories. Medley (86 instances) refers to all properties of the form `prop_n` where `n` is an integer.  Sorting (63 instances) are the remaining theorem with names that begin with `prop_`. Termination (28 instances) are the remaining instances.

1. **Does the dataset contain all possible instances or is it a sample (not necessarily random) of instances from a larger set?** *(If the dataset is a sample, then what is the larger set? Is the sample representative of the larger set (e.g., geographic coverage)? If so, please describe how this representativeness was validated/verified. If it is not representative of the larger set, please describe why not (e.g., to cover a more diverse range of instances, because instances were withheld or unavailable).]* 
    
    The Lean source code for miniCodeProps is translated from a subset of [Tons of Inductive Problems](https://github.com/tip-org/benchmarks) specifically selected to have relevance to programming. We examined the Haskell source code of TIP and selected 3 source files in which a majority of properties involved programs defined elsewhere in the source.

1. **What data does each instance consist of?** *(''Raw'' data (e.g., unprocessed text or images)or features? In either case, please provide a description.)*
    
    Each instance is a json object with 7 fields:
    1. `full_name` -- The unique name of the code property to prove. This name is used as the name of the theorem in its Lean 4 definition.
    2. `prop_defn` -- The theorem definition in Lean 4 that describes the property to be proven.
	3. `prop_loc` -- The file name and line number corresponding to the beginning of this property in the Lean source code in the format \<file name\>:\<line number\>
	4. `score` -- A heuristic score between 1 and 5 for the difficulty of proving the property. 1 indicates that the theorem is very simple and mathematical in nature, 2 indicates a slightly more complex mathematical statement, 3 indicates a difficult mathematical or simpler code property, and 5 indicates a code property expected to be nontrivial to prove. This heuristic is only meaningful in the Medley section; all properties in Sorting and Termination are nontrivial and have a score of 5.
	5. `deps` -- The text of all Lean code needed to define the terms used in the theorem definition in `prop_defn`. In particular, when the contents of this field and the contents of `prop_defn` are concatenated in a file, Lean will type check the file without errors.
	6. `proof_state` -- The Lean proof state of the theorem before any tactics or terms are applied. 
	7. `file_locs` -- The file names and line numbers (same format as `prop_loc`, separated by `&&`) of the last line in each source file needed to define the property. This is useful for prompting
strategies that expect full file contexts and evaluation modes that require the agent to filter for useful lemmas and definitions in the context.


1. **Is there a label or target associated with each instance? If so, please provide a description.**
    
    No; correct proofs are not provided per instance. Generated proofs should be checked by the Lean 4 kernel. Proofs for the Termination instances can be found in the Lean source code.


1. **Is any information missing from individual instances?** *(If so, please provide a description, explaining why this information is missing (e.g., because it was unavailable). This does not include intentionally removed information, but might include, e.g., redacted text.)*
    
    No information is missing.

1. **Are relationships between individual instances made explicit (e.g., users' movie ratings, social network links)?** *( If so, please describe how these relationships are made explicit.)*
    
    Instances may be related in several ways, i.e. two instances may be properties of an overlapping set of programs. Many properties in Sorting rely on the full proof of a property from Termination.These relationships are not made explicit per instance.


1. **Are there recommended data splits (e.g., training, development/validation, testing)?** *(If so, please provide a description of these splits, explaining the rationale behind them.)*
    
    The entire dataset is intended to be used for testing as a benchmark.


1. **Are there any errors, sources of noise, or redundancies in the dataset?** *(If so, please provide a description.)*
    
    With respect to the dataset's intention to be used as a benchmark of proving code properties, 21 of the properties in the Medley section can be viewed as purely mathematical; this may be interpreted as a source of noise; the `score` field is intended to provide visibility into this issue.

1. **Is the dataset self-contained, or does it link to or otherwise rely on external resources (e.g., websites, tweets, other datasets)?** *(If it links to or relies on external resources, a) are there guarantees that they will exist, and remain constant, over time; b) are there official archival versions of the complete dataset (i.e., including the external resources as they existed at the time the dataset was created); c) are there any restrictions (e.g., licenses, fees) associated with any of the external resources that might apply to a future user? Please provide descriptions of all external resources and any restrictions associated with them, as well as links or other access points, as appropriate.)*
    
    The dataset is sourced from [TIP](https://github.com/tip-org/benchmarks), but is independent from TIP. The dataset also relies on an accompanying [repository](https://github.com/evanlohn/MiniCodePropsLeanSrc) of Lean 4 source code on github, also maintained by us. All our resources are made available for use via permissive licensing.


1. **Does the dataset contain data that might be considered confidential (e.g., data that is protected by legal privilege or by doctor-patient confidentiality, data that includes the content of individuals' non-public communications)?** *(If so, please provide a description.)*
    
    No; TIP is licensed with BSD 3-Clause, and so is miniCodeProps.


1. **Does the dataset contain data that, if viewed directly, might be offensive, insulting, threatening, or might otherwise cause anxiety?** *(If so, please describe why.)*
    
    No.


1. **Does the dataset relate to people?** *(If not, you may skip the remaining questions in this section.)*
    
    No.

1. **Does the dataset identify any subpopulations (e.g., by age, gender)?** *(If so, please describe how these subpopulations are identified and provide a description of their respective distributions within the dataset.)*

1. **Is it possible to identify individuals (i.e., one or more natural persons), either directly or indirectly (i.e., in combination with other data) from the dataset?** *(If so, please describe how.)*

1. **Does the dataset contain data that might be considered sensitive in any way (e.g., data that reveals racial or ethnic origins, sexual orientations, religious beliefs, political opinions or union memberships, or locations; financial or health data; biometric or genetic data; forms of government identification, such as social security numbers; criminal history)?** *(If so, please provide a description.)*
    

1. **Any other comments?**
    
    No.





## Collection Process


1. **How was the data associated with each instance acquired?** *(Was the data directly observable (e.g., raw text, movie ratings), reported by subjects (e.g., survey responses), or indirectly inferred/derived from other data (e.g., part-of-speech tags, model-based guesses for age or language)? If data was reported by subjects or indirectly inferred/derived from other data, was the data validated/verified? If so, please describe how.)*
    
    Two steps were taken to collect the data.
    1. *Translation from Haskell to Lean source code*
       After selecting source files from TIP with high proportions of code properties, Lohn translated the code from Haskell to Lean 4. Effort was taken to recreate the original code as faithfully as possible in Lean. One large difference appeared in the definitions of nontrivial recursive sorting algorithms; Lean requires proofs that such functions terminate, while Haskell does not. As such, while translating these functions, Lohn proved a variety of lemmas relating to function termination. These lemmas became the `Termination` section of the dataset. The remaining instances in miniCodeProps were derived directly from properties present in TIP.
    2. *Extraction into benchmark form*
       Lightweight code analysis using the Lean kernel was performed to extract the fields necessary for each instance.

1. **What mechanisms or procedures were used to collect the data (e.g., hardware apparatus or sensor, manual human curation, software program, software API)?** *(How were these mechanisms or procedures validated?)*
    
    Manual human curation was used.

1. **If the dataset is a sample from a larger set, what was the sampling strategy (e.g., deterministic, probabilistic with specific sampling probabilities)?**
    
    We sampled files from TIP containing heuristically high proportions of properties of code.

1. **Who was involved in the data collection process (e.g., students, crowdworkers, contractors) and how were they compensated (e.g., how much were crowdworkers paid)?**
    
    We (the authors) were the only ones involved in the data collection.

1. **Over what timeframe was the data collected?** *( Does this timeframe match the creation timeframe of the data associated with the instances (e.g., recent crawl of old news articles)?  If not, please describe the timeframe in which the data associated with the instances was created.)*
    
    The dataset was collected in the first 5 months of 2024..

1. **Were any ethical review processes conducted (e.g., by an institutional review board)?** *(If so, please provide a description of these review processes, including the outcomes, as well as a link or other access point to any supporting documentation.)*
    
    No.

1. **Does the dataset relate to people?** *(If not, you may skip the remaining questions in this section.)*
    
    No.

1. **Did you collect the data from the individuals in question directly, or obtain it via third parties or other sources (e.g., websites)?**
    
1. **Were the individuals in question notified about the data collection?** *(If so, please describe (or show with screenshots or other information) how notice was provided, and provide a link or other access point to, or otherwise reproduce, the exact language of the notification itself.)*
    
1. **Did the individuals in question consent to the collection and use of their data?** *(If so, please describe (or show with screenshots or other information) how consent was requested and provided, and provide a link or other access point to, or otherwise reproduce, the exact language to which the individuals consented.)*
    
1. **If consent was obtained, were the consenting individuals provided with a mechanism to revoke their consent in the future or for certain uses?** *(If so, please provide a description, as well as a link or other access point to the mechanism (if appropriate).)*

1. **Has an analysis of the potential impact of the dataset and its use on data subjects (e.g., a data protection impact analysis)been conducted?** *(If so, please provide a description of this analysis, including the outcomes, as well as a link or other access point to any supporting documentation.)*
    
1. **Any other comments?**
    
    None.





## Preprocessing/cleaning/labeling


1. **Was any preprocessing/cleaning/labeling of the data done (e.g., discretization or bucketing, tokenization, part-of-speech tagging, SIFT feature extraction, removal of instances, processing of missing values)?** *(If so, please provide a description. If not, you may skip the remainder of the questions in this section.)*

    Only insofar as the extraction of the Lean source code into our benchmark form is considered preprocessing.

1. **Was the "raw" data saved in addition to the preprocessed/cleaned/labeled data (e.g., to support unanticipated future uses)?** *(If so, please provide a link or other access point to the "raw" data.)*
    
    The Lean [source code](https://github.com/evanlohn/MiniCodePropsLeanSrc) is linked to from the [dataset repo](https://huggingface.co/datasets/elohn/miniCodeProps)

1. **Is the software used to preprocess/clean/label the instances available?** *(If so, please provide a link or other access point.)*
    
    Yes, see our [extraction script](https://huggingface.co/datasets/elohn/miniCodeProps/blob/main/extract.py)


1. **Any other comments?**
    
    None.





## Uses


1. **Has the dataset been used for any tasks already?** *(If so, please provide a description.)*
    
    The dataset was used for preliminary establishment of baselines in our paper.


1. **Is there a repository that links to any or all papers or systems that use the dataset?** *(If so, please provide a link or other access point.)*
    
    No.

1. **What (other) tasks could the dataset be used for?**
    
    The dataset could be used for few-shot generation of code and associated properties.


1. **Is there anything about the composition of the dataset or the way it was collected and preprocessed/cleaned/labeled that might impact future uses?** *(For example, is there anything that a future user might need to know to avoid uses that could result in unfair treatment of individuals or groups (e.g., stereotyping, quality of service issues) or other undesirable harms (e.g., financial harms, legal risks)  If so, please provide a description. Is there anything a future user could do to mitigate these undesirable harms?)*
    
    The functions translated from TIP cover a very specific niche of programs; most (64) involved linked lists, while the remaining 3, 4, and 5 cover numbers, binary trees, and heaps respectively. Because the source of our data was TIP, the functions and properties all involve inductive reasoning. 

1. **Are there tasks for which the dataset should not be used?** *(If so, please provide a description.)*
    
    The dataset is likely no large enough to be used for successful fine-tuning.


1. **Any other comments?**
    
    None.




## Distribution


1. **Will the dataset be distributed to third parties outside of the entity (e.g., company, institution, organization) on behalf of which the dataset was created?** *(If so, please provide a description.)*
    
    Yes, the dataset is available to everyone.


1. **How will the dataset will be distributed (e.g., tarball  on website, API, GitHub)?** *(Does the dataset have a digital object identifier (DOI)?)*
    
    Our dataset can be used by cloning our [huggingface repo](https://huggingface.co/datasets/elohn/miniCodeProps).


1. **When will the dataset be distributed?**
    
    The dataset was released fully in June 2024.


1. **Will the dataset be distributed under a copyright or other intellectual property (IP) license, and/or under applicable terms of use (ToU)?** *(If so, please describe this license and/or ToU, and provide a link or other access point to, or otherwise reproduce, any relevant licensing terms or ToU, as well as any fees associated with these restrictions.)*
    
    The dataset is licensed under a BSD 3-clause license.


1. **Have any third parties imposed IP-based or other restrictions on the data associated with the instances?** *(If so, please describe these restrictions, and provide a link or other access point to, or otherwise reproduce, any relevant licensing terms, as well as any fees associated with these restrictions.)*
    
    Not to our knowledge.


1. **Do any export controls or other regulatory restrictions apply to the dataset or to individual instances?** *(If so, please describe these restrictions, and provide a link or other access point to, or otherwise reproduce, any supporting documentation.)*
    
    Not to our knowledge.


1. **Any other comments?**
    
    None.





## Maintenance


1. **Who is supporting/hosting/maintaining the dataset?**
    
    Evan Lohn maintains both the main dataset and associated Lean source code.


1. **How can the owner/curator/manager of the dataset be contacted (e.g., email address)?**
    
    E-mail addresses are at the top of this document.


1. **Is there an erratum?** *(If so, please provide a link or other access point.)*
    
    No.


1. **Will the dataset be updated (e.g., to correct labeling errors, add new instances, delete instances')?** *(If so, please describe how often, by whom, and how updates will be communicated to users (e.g., mailing list, GitHub)?)*
    

    We do not anticipate updates due to errors, but if we add to the dataset in the future it will be explicitly detailed in the readme with information for accessing the prior version(s).

1. **If the dataset relates to people, are there applicable limits on the retention of the data associated with the instances (e.g., were individuals in question told that their data would be retained for a fixed period of time and then deleted)?** *(If so, please describe these limits and explain how they will be enforced.)*
    
    N/A


1. **Will older versions of the dataset continue to be supported/hosted/maintained?** *(If so, please describe how. If not, please describe how its obsolescence will be communicated to users.)*
    
    Yes; all data will be versioned.


1. **If others want to extend/augment/build on/contribute to the dataset, is there a mechanism for them to do so?** *(If so, please provide a description. Will these contributions be validated/verified? If so, please describe how. If not, why not? Is there a process for communicating/distributing these contributions to other users? If so, please provide a description.)*
    
    Not at the moment. If you would like to do so, please contact us.


1. **Any other comments?**
    
    None.