{"id":"W7017161555","doi":"","title":"AlphaSMT: A Reinforcement Learning Guided SMT Solver","year":2023,"lang":"en","type":"dissertation","venue":"UWSpace (University of Waterloo)","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":0,"is_retracted":false,"has_abstract":true,"ca_institutions":"Blackberry (Canada)","funders":"","keywords":"Satisfiability modulo theories; Reinforcement learning; Flexibility (engineering); Solver; Class (philosophy); Function (biology); Artificial neural network; Software","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.0008139795,0.0009997441,0.0006740639,0.0004197998,0.0003473092,0.0009655483,0.001903076,0.001568687,0.008560228],"category_scores_gemma":[0.003533275,0.0004361809,0.0009735145,0.0003511096,0.0008321842,0.0009101207,0.00154617,0.002023716,0.001404309],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00083287,"about_ca_system_score_gemma":0.002504174,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.003772443,"about_ca_topic_score_gemma":0.007855834,"domain_scores_codex":[0.9994979,0.0001383404,0.00003022844,0.0001087976,0.0001453626,0.00007931404],"domain_scores_gemma":[0.9990197,0.0006475595,0.00008305251,0.00007540384,0.0001197569,0.00005452771],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"simulation_or_modeling","study_design_gemma":"simulation_or_modeling","study_design_scores_codex":[0.0002382576,0.0001452311,0.001362694,0.0002554969,0.00008875359,0.0002531916,0.0001087921,0.7950922,0.003741676,0.05759461,0.01243105,0.1286879],"study_design_scores_gemma":[0.00004456461,0.00002416802,0.0000343697,0.00001215189,0.000006884824,0.00002003593,0.000006573211,0.9862721,0.0007393273,0.01055352,0.002282305,0.000003964488],"study_design_candidate":"simulation_or_modeling","study_design_consensus":"simulation_or_modeling","genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.01471878,0.0003609294,0.9655792,0.0007209991,0.0001594587,0.000182598,0.0004409582,0.004651295,0.01318579],"genre_scores_gemma":[0.3416129,0.000335407,0.6441609,0.000704135,0.00008840653,0.0004833517,0.0008203124,0.0006685279,0.011126],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.008560228,"threshold_uncertainty_score":0.02863687,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.02864262116072009,"score_gpt":0.2590200300961433,"score_spread":0.2303774089354232,"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."}}