{"id":"W4281610263","doi":"10.4230/lipics.itp.2023.12","title":"Lessons for Interactive Theorem Proving Researchers from a Survey of Coq Users","year":2023,"lang":"en","type":"preprint","venue":"HAL (Le Centre pour la Communication Scientifique Directe)","topic":"Logic, programming, and type systems","field":"Computer Science","cited_by":1,"is_retracted":false,"has_abstract":true,"ca_institutions":"Prevention of Organ Failure","funders":"","keywords":"Mathematical proof; Proof assistant; Computer science; Software engineering; Programming language; Plug-in; Software; Process (computing); Proof of concept; Operating system; Mathematics","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.01383035,0.0002747252,0.0004751426,0.0002372916,0.0002425682,0.000642373,0.003186745,0.0002622205,0.00001387882],"category_scores_gemma":[0.00652309,0.0002668895,0.0002266712,0.0005477106,0.0002515776,0.000221098,0.002881478,0.0005791241,0.00002442609],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0001512043,"about_ca_system_score_gemma":0.0006069429,"about_ca_topic_candidate":true,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.03333385,"about_ca_topic_score_gemma":0.01700734,"domain_scores_codex":[0.9899914,0.007518329,0.0005702825,0.0009859982,0.000508674,0.000425347],"domain_scores_gemma":[0.9855237,0.007661875,0.0007579247,0.00250318,0.003394629,0.0001586721],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"theoretical_or_conceptual","study_design_gemma":"theoretical_or_conceptual","study_design_scores_codex":[0.00005804842,0.000553604,0.007544275,0.0004002066,0.0003975474,0.000006437213,0.04242072,0.00008433952,0.0009823164,0.8384069,0.001666482,0.1074791],"study_design_scores_gemma":[0.002881282,0.000009355935,0.1157899,0.003554739,0.0001320713,0.000007090553,0.002086203,0.3352999,0.07445034,0.4520274,0.01146067,0.002301038],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":"theoretical_or_conceptual","genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.009341448,0.0003412599,0.9769301,0.004936476,0.000605835,0.001140134,0.0001671213,0.000339976,0.006197615],"genre_scores_gemma":[0.9599711,0.00009160822,0.03580114,0.00001966562,0.00001962635,0.0002042106,0.0005533554,0.00004341199,0.003295856],"genre_candidate":"methods","genre_consensus":null,"teacher_disagreement_score":0.9506297,"threshold_uncertainty_score":0.9999783,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.1046349544622271,"score_gpt":0.323948681985571,"score_spread":0.2193137275233439,"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."}}