{"id":"W4409360835","doi":"10.1609/aaai.v39i28.35275","title":"Algorithm Selection for Word-Level Hardware Model Checking (Student Abstract)","year":2025,"lang":"en","type":"article","venue":"Proceedings of the AAAI Conference on Artificial Intelligence","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":2,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of Waterloo","funders":"Deutsche Forschungsgemeinschaft","keywords":"Selection (genetic algorithm); Computer science; Word (group theory); Programming language; Arithmetic; Natural language processing; Artificial intelligence; 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":"metacan-v3-hybrid-931329e0061c","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.003925936,0.001402385,0.0009285499,0.001510825,0.0006307876,0.002250589,0.002573055,0.001056384,0.01149686],"category_scores_gemma":[0.01571465,0.0007078346,0.002035207,0.001188442,0.001206573,0.004099744,0.002475974,0.001737467,0.003191101],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.001377576,"about_ca_system_score_gemma":0.001882565,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00105774,"about_ca_topic_score_gemma":0.001884731,"domain_scores_codex":[0.9915544,0.003414687,0.0007228331,0.001253969,0.002347717,0.0007063992],"domain_scores_gemma":[0.9897357,0.006022227,0.0006864029,0.002392263,0.001018535,0.0001447471],"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.001453168,0.0003260344,0.004671565,0.001039743,0.0002505561,0.0002904351,0.0002220958,0.1093004,0.03487075,0.119146,0.03713645,0.6912929],"study_design_scores_gemma":[0.0002083524,0.0002585842,0.0003938075,0.0001258471,0.00007020654,0.0001901593,0.00004472868,0.8067558,0.06718089,0.1128279,0.01187996,0.00006375308],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.01625272,0.0002759526,0.9557929,0.0004029141,0.0001236984,0.0001275627,0.0003461977,0.02327221,0.003405812],"genre_scores_gemma":[0.357534,0.0001478495,0.6337469,0.0005404018,0.0001373695,0.0002823455,0.001284187,0.00320183,0.003125268],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.01149686,"threshold_uncertainty_score":0.03846079,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.15450902196769,"score_gpt":0.3769225950213758,"score_spread":0.2224135730536858,"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."}}