{"id":"W2963864435","doi":"10.48550/arxiv.1509.06082","title":"Extending ACL2 with SMT Solvers","year":2015,"lang":"en","type":"article","venue":"arXiv (Cornell University)","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":2,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of British Columbia","funders":"","keywords":"Computer science; Satisfiability modulo theories; Programming language; Automated theorem proving; Extension (predicate logic); Satisfiability; Range (aeronautics); Key (lock); Theoretical computer science","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.0003873052,0.0001091375,0.0001009953,0.0001242347,0.00009871327,0.00005643334,0.0008417561,0.00005039073,0.000007721089],"category_scores_gemma":[0.00004814664,0.0001073309,0.00003372472,0.0007754216,0.00008275932,0.001137182,0.0001846999,0.000116825,0.0001297041],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0001467159,"about_ca_system_score_gemma":0.00007518324,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00003568322,"about_ca_topic_score_gemma":0.000007689836,"domain_scores_codex":[0.9991061,0.00008100986,0.00008803043,0.0004019731,0.00008818522,0.0002347041],"domain_scores_gemma":[0.9989862,0.00003188137,0.00008923501,0.0006066858,0.0001081497,0.0001778016],"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.00004178446,0.00004030008,0.008719949,0.000006752941,0.00001705391,0.0001300102,0.0004097565,0.02029164,0.0001016536,0.9676765,0.0003418305,0.002222746],"study_design_scores_gemma":[0.001401506,0.0003525382,0.00367178,0.00002781126,0.00003339375,0.00005824034,0.0006073285,0.967326,0.002513229,0.01739619,0.006049878,0.0005620872],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.1510849,0.000009450528,0.8384632,0.00002983016,0.0002004234,0.0000729392,4.525872e-7,0.0001848899,0.009953852],"genre_scores_gemma":[0.8660676,0.000005281316,0.1330137,0.00005869766,0.00002197674,2.598627e-7,6.88477e-7,0.000006455747,0.000825379],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.9502803,"threshold_uncertainty_score":0.4376827,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.1646556365467033,"score_gpt":0.2057636509691067,"score_spread":0.04110801442240344,"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."}}