{"id":"W7109952297","doi":"10.4230/lipics.sat.2025.32","title":"Efficient Certified Reasoning for Binarized Neural Networks","year":2025,"lang":"en","type":"article","venue":"DROPS (Schloss Dagstuhl – Leibniz Center for Informatics)","topic":"Adversarial Robustness in Machine Learning","field":"Computer Science","cited_by":0,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of Toronto","funders":"Natural Sciences and Engineering Research Council of Canada; Alliance de recherche numérique du Canada; Vetenskapsrådet; National Supercomputing Centre Singapore; University of Toronto; Innovation, Science and Economic Development Canada","keywords":"Speedup; Soundness; Scalability; Robustness (evolution); Benchmark (surveying); Artificial neural network; Formal verification; Pipeline (software)","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":"metacan-v3-hybrid-931329e0061c","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.004367248,0.001585459,0.001025746,0.001624238,0.001304679,0.003892875,0.004405166,0.002089323,0.01078737],"category_scores_gemma":[0.03273028,0.001292304,0.003540136,0.0008942168,0.003403547,0.006742958,0.004699287,0.003822408,0.001659597],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.004093711,"about_ca_system_score_gemma":0.007576111,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.01162723,"about_ca_topic_score_gemma":0.02445465,"domain_scores_codex":[0.991205,0.002275681,0.0006002523,0.001499451,0.003558357,0.0008610961],"domain_scores_gemma":[0.982039,0.0110009,0.001012371,0.002983453,0.002683043,0.0002811444],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"simulation_or_modeling","study_design_gemma":"theoretical_or_conceptual","study_design_scores_codex":[0.0007807456,0.000297464,0.004675122,0.001680344,0.0003372829,0.001054597,0.0006120678,0.4827873,0.02882914,0.2724404,0.01375526,0.1927504],"study_design_scores_gemma":[0.00009729469,0.00005144624,0.0001749435,0.0001245336,0.00009051868,0.0001465138,0.00008767842,0.8291045,0.02252753,0.1406887,0.006863498,0.00004280087],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.02119095,0.0003129694,0.9605929,0.0009870584,0.0001455884,0.0002516159,0.0007347259,0.01127388,0.004510306],"genre_scores_gemma":[0.3833543,0.0004376354,0.6049761,0.001123386,0.00009313283,0.0003980208,0.002180848,0.002411133,0.005025515],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.01162723,"threshold_uncertainty_score":0.03608733,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.01107840787201233,"score_gpt":0.2723201104293548,"score_spread":0.2612417025573425,"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."}}