{"id":"W3022618186","doi":"10.1007/978-3-030-72013-1_16","title":"MachSMT: A Machine Learning-based Algorithm Selector for SMT Solvers","year":2021,"lang":"en","type":"book-chapter","venue":"Lecture notes in computer science","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":26,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of Waterloo","funders":"Office of Naval Research; Defense Advanced Research Projects Agency","keywords":"Algorithm; Computer science; Machine learning; Ranking (information retrieval); Artificial intelligence","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.001866614,0.0006467811,0.0006672369,0.0008325849,0.000440507,0.000615538,0.003356664,0.0004370948,0.00003122011],"category_scores_gemma":[0.0004756209,0.0006429026,0.0002707327,0.0009453747,0.0005248578,0.0005335493,0.0007623251,0.001167296,0.00001338834],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0005174784,"about_ca_system_score_gemma":0.001133775,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00002112566,"about_ca_topic_score_gemma":0.00003945393,"domain_scores_codex":[0.9953046,0.0001138199,0.00062126,0.002018503,0.001066014,0.00087577],"domain_scores_gemma":[0.9963254,0.0009841799,0.0004518059,0.001447772,0.000573204,0.0002176901],"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.000008831851,0.00003413497,0.00001548054,0.00007068493,0.00001341505,0.0000326234,0.0001835547,0.02011464,0.0001134193,0.01300093,0.00002360446,0.9663887],"study_design_scores_gemma":[0.0004277907,0.0003241938,0.0000150641,0.0001956389,0.00001318029,0.00003484742,8.632934e-8,0.9521627,0.005584868,0.0302527,0.0102964,0.0006925462],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.000004886731,0.0006761422,0.9950586,0.0004757404,0.002338183,0.0006809182,0.00001886123,0.0002995708,0.0004471082],"genre_scores_gemma":[0.001200894,0.00003130926,0.9964526,0.001077723,0.0004740019,0.00004796929,0.00003554479,0.00005882215,0.0006211716],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.9656962,"threshold_uncertainty_score":0.9996022,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.02244275859653951,"score_gpt":0.2719503525007648,"score_spread":0.2495075939042253,"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."}}