{"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":"metacan-v3-hybrid-931329e0061c","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.001754161,0.0009072704,0.0007224252,0.00159897,0.0008531775,0.002110432,0.002254792,0.00121976,0.01055131],"category_scores_gemma":[0.01934084,0.0007808045,0.001949793,0.001290044,0.001504461,0.003412405,0.003902409,0.002256583,0.002459008],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.001405916,"about_ca_system_score_gemma":0.0028652,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.007668186,"about_ca_topic_score_gemma":0.01670985,"domain_scores_codex":[0.9977826,0.0005090273,0.0001189093,0.0005144193,0.0008368779,0.0002380357],"domain_scores_gemma":[0.9891351,0.006353007,0.0005941453,0.002629762,0.00102242,0.0002654328],"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.0007290966,0.0005089196,0.008986135,0.0007228531,0.0001150193,0.001196516,0.0005781451,0.2138554,0.01163604,0.1709359,0.03019048,0.5605454],"study_design_scores_gemma":[0.00009850311,0.0001026735,0.000768441,0.00007851308,0.00004826466,0.0002504763,0.0001425439,0.6836713,0.008744734,0.2909305,0.01513412,0.00002996124],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.03491214,0.0002017397,0.9429832,0.0007391404,0.00006029695,0.0003602702,0.001442742,0.01280774,0.006492726],"genre_scores_gemma":[0.2819992,0.0001953344,0.7045553,0.0005417729,0.00005880584,0.0003891251,0.006219984,0.001439852,0.004600678],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.01055131,"threshold_uncertainty_score":0.03529763,"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."}}