{"id":"W6891653032","doi":"10.4230/lipics.sat.2025.18","title":"Towards Practical First-Order Model Counting","year":2025,"lang":"en","type":"article","venue":"DROPS (Schloss Dagstuhl – Leibniz Center for Informatics)","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":0,"is_retracted":false,"has_abstract":true,"ca_institutions":"Vector Institute; University of Toronto","funders":"Natural Sciences and Engineering Research Council of Canada; Alliance de recherche numérique du Canada","keywords":"Inference; Scalability; Domain (mathematical analysis); Code (set theory); Function (biology); State (computer science); Scale (ratio)","routes":{"ca_aff":true,"ca_fund":true,"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.001617157,0.0003953605,0.0004342877,0.000365152,0.0005690097,0.0007463239,0.001587308,0.0003104881,0.00001367991],"category_scores_gemma":[0.001056359,0.0003734729,0.0002021619,0.0008687525,0.0001392095,0.003793691,0.0008329902,0.0005763958,0.0001158871],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0002549038,"about_ca_system_score_gemma":0.0004171454,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00001471869,"about_ca_topic_score_gemma":0.000008696408,"domain_scores_codex":[0.9968224,0.00005495183,0.001260197,0.0003940914,0.0006343763,0.0008339497],"domain_scores_gemma":[0.9971504,0.0002295604,0.0004724589,0.001295439,0.0006915191,0.0001605737],"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.0001024076,0.000412882,0.000953933,0.0009952012,0.0001771352,0.000003443914,0.006350573,0.004439036,0.00005222932,0.9375588,0.01613568,0.03281868],"study_design_scores_gemma":[0.001089023,0.00006971286,0.0002167959,0.0001168679,0.0000291548,0.00002445382,0.0002492822,0.9154094,0.0009066035,0.006971176,0.0745462,0.0003713402],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.003566623,0.00002754682,0.964054,0.001977775,0.001329362,0.0009065893,0.0000641345,0.0003904475,0.02768348],"genre_scores_gemma":[0.05971692,0.0000304509,0.9365275,0.002696043,0.00007585251,0.0002021144,0.00006771593,0.00002778122,0.0006556373],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.9305876,"threshold_uncertainty_score":0.9998717,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.03395770335754854,"score_gpt":0.3415875842140492,"score_spread":0.3076298808565006,"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."}}