{"id":"W4280619266","doi":"10.4230/lipics.itp.2022.18","title":"Automatic Test-Case Reduction in Proof Assistants: A Case Study in Coq","year":2022,"lang":"en","type":"article","venue":"DROPS (Schloss Dagstuhl – Leibniz Center for Informatics)","topic":"Software Testing and Debugging Techniques","field":"Computer Science","cited_by":2,"is_retracted":false,"has_abstract":true,"ca_institutions":"Prevention of Organ Failure","funders":"","keywords":"Computer science; Reduction (mathematics); Test (biology); Proof assistant; Proof of concept; Programming language; Operating system; Mathematics; Mathematical proof","routes":{"ca_aff":true,"ca_fund":false,"ca_venue":false,"about_ca":false,"invisible_to_affiliation_only":false},"retraction":null,"screen":null,"direct_labels":[],"prediction":{"model_version":"codex-gemma-dda1882f352a","candidate_categories":["metaepi_narrow"],"consensus_categories":[],"category_scores_codex":[0.002215012,0.0003608523,0.0004672061,0.0009027749,0.0005223856,0.000368625,0.0009687223,0.0001002655,0.00001676452],"category_scores_gemma":[0.000566832,0.0003674492,0.0001129424,0.001430996,0.00006132442,0.001305743,0.0009235336,0.0007238576,0.000008607249],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0005992746,"about_ca_system_score_gemma":0.0001740931,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.0005685604,"about_ca_topic_score_gemma":0.0001968657,"domain_scores_codex":[0.9966213,0.0001795942,0.001481366,0.0004341249,0.0005879138,0.0006956769],"domain_scores_gemma":[0.9976929,0.0004752062,0.0004859856,0.001080572,0.0001353448,0.0001299535],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"observational","study_design_gemma":"simulation_or_modeling","study_design_scores_codex":[0.0001088262,0.01282159,0.5397379,0.001359667,0.0001517503,0.0477252,0.1702927,0.001543775,0.00002424353,0.0007517342,0.01124731,0.2142353],"study_design_scores_gemma":[0.005607311,0.002257142,0.004036469,0.0002366706,0.00003145888,0.09849019,0.01413069,0.8699138,0.0000844795,0.003471231,0.0006969973,0.001043623],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"empirical","genre_gemma":"empirical","genre_scores_codex":[0.9715615,0.0000244981,0.02218303,0.0001205096,0.0005464756,0.00261789,0.00009699233,0.002644373,0.0002047697],"genre_scores_gemma":[0.9599725,9.179511e-7,0.03854389,0.000159839,0.000029014,0.001193331,0.00002873215,0.0000331928,0.0000385797],"genre_candidate":"empirical","genre_consensus":"empirical","teacher_disagreement_score":0.8683699,"threshold_uncertainty_score":0.9998778,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.02613850071469267,"score_gpt":0.2937174769024335,"score_spread":0.2675789761877409,"validation_status":"score_only:v0-immature-baseline","note":"Baseline scores from an immature model (maturity gate not passed). Scores rank; they never assert a category."}}