{"id":"W2755744672","doi":"10.1109/ivsw.2017.8031554","title":"Learning lemma support graphs in Quip and IC3","year":2017,"lang":"en","type":"article","venue":"","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":3,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of Toronto","funders":"","keywords":"Computer science; Satisfiability; Satisfiability modulo theories; Formal verification; Model checking; Subroutine; Boolean satisfiability problem; Theoretical computer science; Lemma (botany); Graph; Functional verification; Runtime verification; Programming language; Algorithm","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.000685386,0.00004787206,0.00006359701,0.00006271015,0.0001661401,0.0002131371,0.0005281032,0.00003108103,0.00001534258],"category_scores_gemma":[0.0001831545,0.0000432886,0.00001214639,0.00005164574,0.00005230578,0.000764275,0.0002219669,0.0001004362,0.00002355678],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.000007957632,"about_ca_system_score_gemma":0.00001414714,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00008999091,"about_ca_topic_score_gemma":0.00002394283,"domain_scores_codex":[0.9994613,0.00004477717,0.0001012234,0.0001784136,0.00008800167,0.0001262663],"domain_scores_gemma":[0.9994091,0.00002240936,0.00006728716,0.0004493504,0.00001709525,0.00003472914],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"theoretical_or_conceptual","study_design_gemma":"observational","study_design_scores_codex":[0.000002711786,0.00001385323,0.1148647,0.00000888325,0.000002326329,0.000008200872,0.000865368,0.000009505935,0.0008273856,0.6152846,0.0001342001,0.2679782],"study_design_scores_gemma":[0.0003828375,0.0001645981,0.8818882,0.00001432806,0.000001688897,0.00002753824,0.00008398177,0.08231056,0.006799967,0.02038381,0.007718276,0.0002242565],"study_design_candidate":"observational","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.4292613,0.00001931426,0.4725486,0.0007677493,0.0003804344,0.0001205231,1.317656e-7,0.0001406885,0.09676124],"genre_scores_gemma":[0.6831933,0.00001078379,0.316085,0.00004779065,0.000006788732,0.000003302715,1.629746e-7,0.000001993178,0.0006508619],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.7670234,"threshold_uncertainty_score":0.2055286,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.03748121500807641,"score_gpt":0.3224533001387928,"score_spread":0.2849720851307164,"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."}}