{"id":"W4400973174","doi":"10.1007/978-3-031-65627-9_8","title":"Formally Certified Approximate Model Counting","year":2024,"lang":"en","type":"book-chapter","venue":"Lecture notes in computer science","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":1,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of Toronto","funders":"Simons Institute for the Theory of Computing, University of California Berkeley; National Supercomputing Centre Singapore; Ministry of Education, India; Vetenskapsrådet; National Research Foundation Singapore; National Research Foundation","keywords":"Computer science; Algorithm; Correctness; True quantified Boolean formula; HOL; Proof assistant; Automated theorem proving; Maximum satisfiability problem; Discrete mathematics; Boolean function; Programming language; Mathematics; Mathematical proof","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","scholarly_communication"],"consensus_categories":[],"category_scores_codex":[0.002161044,0.0005952771,0.0005022024,0.0009640642,0.0002779701,0.001229109,0.004491909,0.0004010073,0.000008008038],"category_scores_gemma":[0.0001166502,0.0005457764,0.0001609144,0.0007777266,0.0005502226,0.001447366,0.00209252,0.001163626,0.000129217],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0004352885,"about_ca_system_score_gemma":0.0005878627,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.000007681354,"about_ca_topic_score_gemma":0.00001164288,"domain_scores_codex":[0.9953117,0.0000231927,0.0007477335,0.001836113,0.001241017,0.0008402743],"domain_scores_gemma":[0.9970884,0.000191031,0.0003245164,0.001958532,0.000279017,0.0001585319],"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.000004402398,0.00001252638,0.000002708741,0.0001436025,0.00000949397,0.00003135267,0.0008223761,0.1550624,0.0002567708,0.5053767,0.00001747895,0.3382601],"study_design_scores_gemma":[0.00006125203,0.00003672094,0.000003146059,0.0002333387,0.000006237889,0.00004011038,6.752168e-8,0.6544287,0.001397327,0.3428077,0.0005815605,0.0004038207],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.00002311658,0.0003470692,0.972185,0.0003729128,0.003388424,0.0004500338,0.000005803786,0.0004857572,0.02274187],"genre_scores_gemma":[0.01481364,0.00003094464,0.982042,0.0008350569,0.000307947,0.0000207204,0.000004634598,0.00005626892,0.001888768],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.4993663,"threshold_uncertainty_score":0.9998077,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.03999781947336101,"score_gpt":0.2814009612170026,"score_spread":0.2414031417436416,"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."}}