search

Radiance-Technologies / prism

Utilities for creating and curating a dataset for automated proof repair in the Coq Proof Assistant.
GNU Lesser General Public License v3.0
5 stars 2 forks source link

Controlled perturbation of data types, specifications, etc. #19

Open a-gardner1 opened 2 years ago

a-gardner1 commented 2 years ago

This mode of data augmentation comprises expert-guided synthesis of broken changes. Unlike #18, which can intrinsically yield supervised examples, the changes induced by expert methods have no a priori ground-truth, repaired versions. However, tools such as PUMPKIN-PATCH or CoqHammer may be used in concert to synthesize repairs.

a-gardner1 commented 2 years ago

Mutations produced by mcoq may serve as a good source of perturbations.