{"id":"W4399851533","doi":"10.1145/3656438","title":"Towards Trustworthy Automated Program Verifiers: Formally Validating Translations into an Intermediate Verification Language","year":2024,"lang":"en","type":"article","venue":"Proceedings of the ACM on Programming Languages","topic":"Security and Verification in Computing","field":"Computer Science","cited_by":5,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of British Columbia","funders":"Schweizerischer Nationalfonds zur Förderung der Wissenschaftlichen Forschung","keywords":"Trustworthiness; Computer science; Programming language; Software engineering; Natural language processing; Computer security","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":[],"consensus_categories":[],"category_scores_codex":[0.0008109552,0.0002217489,0.0001923982,0.0002143999,0.0002799135,0.000904006,0.002811791,0.0001133708,0.000005758098],"category_scores_gemma":[0.000551713,0.0001734022,0.0001487778,0.001119465,0.0001112244,0.001113725,0.0003881935,0.0003262361,0.000008959906],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00006429774,"about_ca_system_score_gemma":0.0000800054,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00005599268,"about_ca_topic_score_gemma":0.000004795106,"domain_scores_codex":[0.9982083,0.00003163588,0.0004418622,0.0005257851,0.0004446272,0.0003477919],"domain_scores_gemma":[0.9986918,0.00009427252,0.0002227505,0.0007177406,0.000183107,0.00009030371],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"design_other","study_design_gemma":"simulation_or_modeling","study_design_scores_codex":[0.00001297526,0.000174211,0.0002843539,0.0004017958,0.00005220718,0.000002590627,0.04186472,0.00003113389,0.008138883,0.02589377,0.0002400284,0.9229034],"study_design_scores_gemma":[0.000967149,0.001476823,0.008463183,0.002152669,0.0001753772,0.00008054799,0.01829193,0.7225583,0.2211279,0.009041154,0.01430519,0.001359803],"study_design_candidate":"design_other","study_design_consensus":null,"genre_codex":"empirical","genre_gemma":"empirical","genre_scores_codex":[0.9806365,0.0007402101,0.00472467,0.002813464,0.000746511,0.001176332,0.000006645326,0.007717431,0.001438222],"genre_scores_gemma":[0.8267823,0.000008878698,0.1728058,0.00007661713,0.0001318739,0.0001322043,0.00001317561,0.00002447229,0.00002462275],"genre_candidate":"empirical","genre_consensus":"empirical","teacher_disagreement_score":0.9215435,"threshold_uncertainty_score":0.871735,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.0193190425675604,"score_gpt":0.3301303058016578,"score_spread":0.3108112632340974,"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."}}