{"id":"W2086056248","doi":"10.1109/fmcad.2007.13","title":"Boosting Verification by Automatic Tuning of Decision Procedures","year":2007,"lang":"en","type":"article","venue":"","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":94,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of British Columbia","funders":"","keywords":"Computer science; Heuristics; Parameterized complexity; Solver; Model checking; Boosting (machine learning); Software; Machine learning; Satisfiability modulo theories; Heuristic; Artificial intelligence; Bounded function; Process (computing); Algorithm; Programming language; 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.00151037,0.00006871639,0.00008810533,0.0001014965,0.00006748946,0.00003688416,0.0004978108,0.00004611707,0.00001172234],"category_scores_gemma":[0.0008913386,0.00006158894,0.00002275058,0.0004185949,0.00002705856,0.0004902052,0.00007164748,0.00005659946,0.00001676193],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0000341278,"about_ca_system_score_gemma":0.00003497683,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00001056957,"about_ca_topic_score_gemma":0.000001872934,"domain_scores_codex":[0.9989938,0.0000298771,0.0003593673,0.0001916138,0.0002685775,0.0001567779],"domain_scores_gemma":[0.999052,0.0002297191,0.0001851648,0.0003911361,0.0000984324,0.00004358622],"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.000005834587,0.00004965373,0.0006315901,0.00005682581,0.000004249799,6.546348e-7,0.0007847808,0.00003590381,0.1312681,0.08631192,0.0008294212,0.7800211],"study_design_scores_gemma":[0.0001854042,0.00007643479,0.01433422,0.0001011352,0.000003715837,0.00001627665,0.000137449,0.5515079,0.42925,0.003574937,0.0006446911,0.0001677922],"study_design_candidate":"design_other","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.09874144,0.0000546134,0.8965703,0.00002945524,0.0001206123,0.000106249,1.958015e-7,0.0001466515,0.004230456],"genre_scores_gemma":[0.4559616,0.000002143816,0.5439461,0.00003168405,0.000006660886,0.000002063469,5.390027e-7,0.000002794632,0.00004648973],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.7798533,"threshold_uncertainty_score":0.2511524,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.01916878961442004,"score_gpt":0.3105799987214886,"score_spread":0.2914112091070686,"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."}}