{"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":"codex-gemma-dda1882f352a","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.0009462186,0.0002174452,0.0002400828,0.000193742,0.0003209802,0.000317694,0.002060394,0.0001234849,0.000009015239],"category_scores_gemma":[0.0005042886,0.0001822201,0.0001389054,0.0007913044,0.0001292081,0.0005737145,0.0003138307,0.0002909409,0.00001357732],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0001308604,"about_ca_system_score_gemma":0.0001852426,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00001917221,"about_ca_topic_score_gemma":0.000005903429,"domain_scores_codex":[0.9980858,0.00001115055,0.0006052855,0.0005393581,0.0004155836,0.000342803],"domain_scores_gemma":[0.9980763,0.00008430507,0.0003981583,0.0002838033,0.001104941,0.00005253715],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"theoretical_or_conceptual","study_design_gemma":"simulation_or_modeling","study_design_scores_codex":[0.00002329952,0.00008689168,0.00003742963,0.00004417249,0.00001296884,1.867179e-8,0.0005268272,0.0007369709,0.0149033,0.6190068,0.00009229538,0.364529],"study_design_scores_gemma":[0.00001898433,0.00003668992,0.0002572346,0.0001332871,0.000008660958,5.92394e-7,0.0001479383,0.5122982,0.3418791,0.1450418,0.00007202265,0.0001055225],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.007834704,0.00001367133,0.9845703,0.001260266,0.0006232489,0.0006790083,0.000007769579,0.0001182451,0.00489281],"genre_scores_gemma":[0.5833451,0.00001560772,0.4156084,0.0001678523,0.00004492309,0.000118974,5.300016e-7,0.000009384469,0.0006892934],"genre_candidate":"methods","genre_consensus":null,"teacher_disagreement_score":0.5755103,"threshold_uncertainty_score":0.7430721,"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."}}