{"id":"W3208505901","doi":"10.48550/arxiv.2110.14187","title":"An Experimental Study of Permanently Stored Learned Clauses","year":2021,"lang":"en","type":"preprint","venue":"arXiv (Cornell University)","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":0,"is_retracted":false,"has_abstract":true,"ca_institutions":"Simon Fraser University","funders":"","keywords":"Computer science; Limiting; Heuristic; Scheme (mathematics); Centrality; Binary number; Parallel computing; Arithmetic; Theoretical computer science; Artificial intelligence; Mathematics; Combinatorics","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.0003674992,0.0002523153,0.0003588893,0.0002265857,0.0001141049,0.0001162113,0.002173743,0.0001905929,0.00003654806],"category_scores_gemma":[0.000031137,0.0003105378,0.0001226113,0.0004714532,0.00009286006,0.0007307569,0.001544247,0.0004083996,0.00000977012],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0001889542,"about_ca_system_score_gemma":0.0001327497,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.0002559441,"about_ca_topic_score_gemma":0.00003075094,"domain_scores_codex":[0.9976309,0.0006120021,0.0002947944,0.001076219,0.0001643867,0.0002216817],"domain_scores_gemma":[0.9972481,0.00003716612,0.0003621807,0.002035367,0.0001919694,0.0001251818],"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.0004595987,0.0231718,0.07400727,0.0004458983,0.0007214476,0.001529446,0.06230481,0.5596059,0.03550266,0.2385587,0.0001057662,0.003586767],"study_design_scores_gemma":[0.002344081,0.002138908,0.02297424,0.0001128344,0.0001787652,0.00001372943,0.03049047,0.8976151,0.04133435,0.001336796,0.00008798128,0.001372705],"study_design_candidate":"simulation_or_modeling","study_design_consensus":"simulation_or_modeling","genre_codex":"empirical","genre_gemma":"empirical","genre_scores_codex":[0.7979434,0.00004672737,0.2007366,0.000003861604,0.0005009319,0.000311729,0.000002650911,0.0001354589,0.0003186936],"genre_scores_gemma":[0.9764791,0.00001732011,0.02327754,0.00001620967,0.00003289791,0.000002096433,0.00001281019,0.00001597257,0.0001461257],"genre_candidate":"empirical","genre_consensus":"empirical","teacher_disagreement_score":0.3380093,"threshold_uncertainty_score":0.9999347,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.1617553693831643,"score_gpt":0.2717542089286544,"score_spread":0.1099988395454901,"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."}}