{"693391":{"#nid":"693391","#data":{"type":"event","title":"PhD Defense by Jiong Yang","body":[{"value":"\u003Cp\u003E\u003Cstrong\u003ETitle\u003C\/strong\u003E: Efficient and Trusted Approximate Model Counting\u003C\/p\u003E\u003Cp\u003E\u0026nbsp;\u003C\/p\u003E\u003Cp\u003E\u003Cstrong\u003EDate\u003C\/strong\u003E: Friday, October 30th, 2026\u003C\/p\u003E\u003Cp\u003E\u003Cstrong\u003ETime\u003C\/strong\u003E: 1:00 - 3:00 PM ET\u003C\/p\u003E\u003Cp\u003E\u003Cstrong\u003ELocation\u003C\/strong\u003E: Klaus 3100\u003C\/p\u003E\u003Cp\u003E\u003Cstrong\u003EZoom\u003C\/strong\u003E:\u0026nbsp;\u003Ca href=\u0022https:\/\/nam12.safelinks.protection.outlook.com\/?url=https%3A%2F%2Fgatech.zoom.us%2Fj%2F92641944955\u0026amp;data=05%7C02%7Cannouncements%40grad.gatech.edu%7Ca3c246bd767d4931f8ea08df2ee2b658%7C482198bbae7b4b258b7a6d7f32faa083%7C1%7C0%7C639281223419915288%7CUnknown%7CTWFpbGZsb3d8eyJFbXB0eU1hcGkiOnRydWUsIlYiOiIwLjAuMDAwMCIsIlAiOiJXaW4zMiIsIkFOIjoiTWFpbCIsIldUIjoyfQ%3D%3D%7C0%7C%7C%7C\u0026amp;sdata=fce8OTMcNdeY7T5LeUWi54tFdiHALkNi7C9F588qUok%3D\u0026amp;reserved=0\u0022 target=\u0022_blank\u0022 title=\u0022https:\/\/gatech.zoom.us\/j\/92641944955\u0022\u003Ehttps:\/\/gatech.zoom.us\/j\/92641944955\u003C\/a\u003E\u003C\/p\u003E\u003Cp\u003E\u0026nbsp;\u003C\/p\u003E\u003Cp\u003E\u003Cstrong\u003EJiong Yang\u003C\/strong\u003E\u003Cbr\u003EPh.D. Student\u003C\/p\u003E\u003Cp\u003ESchool of Computer Science\u003C\/p\u003E\u003Cp\u003ECollege of Computing\u003C\/p\u003E\u003Cp\u003EGeorgia Institute of Technology\u003C\/p\u003E\u003Cp\u003E\u003Ca href=\u0022https:\/\/nam12.safelinks.protection.outlook.com\/?url=https%3A%2F%2Fal-jiongyang.github.io%2F\u0026amp;data=05%7C02%7Cannouncements%40grad.gatech.edu%7Ca3c246bd767d4931f8ea08df2ee2b658%7C482198bbae7b4b258b7a6d7f32faa083%7C1%7C0%7C639281223419944608%7CUnknown%7CTWFpbGZsb3d8eyJFbXB0eU1hcGkiOnRydWUsIlYiOiIwLjAuMDAwMCIsIlAiOiJXaW4zMiIsIkFOIjoiTWFpbCIsIldUIjoyfQ%3D%3D%7C0%7C%7C%7C\u0026amp;sdata=y6vfUujcotKkhqM03nSfMiNWg%2FceV%2B3jg9bKSl4MSUA%3D\u0026amp;reserved=0\u0022 target=\u0022_blank\u0022 title=\u0022Original URL: https:\/\/al-jiongyang.github.io\/. Click or tap if you trust this link.\u0022\u003Ehttps:\/\/al-jiongyang.github.io\/\u003C\/a\u003E\u003C\/p\u003E\u003Cp\u003E\u0026nbsp;\u003C\/p\u003E\u003Cp\u003E\u003Cstrong\u003ECommittee members\u003C\/strong\u003E\u003C\/p\u003E\u003Cp\u003EDr. Kuldeep S. Meel (Advisor) \u2013 School of Computer Science, Georgia Institute of Technology\u003C\/p\u003E\u003Cp\u003EDr. Vijay Ganesh \u2013 School of Computer Science, Georgia Institute of Technology\u003C\/p\u003E\u003Cp\u003EDr. Santosh Pande \u2013 School of Computer Science, Georgia Institute of Technology\u003C\/p\u003E\u003Cp\u003EDr. Qirun Zhang \u2013 School of Computer Science, Georgia Institute of Technology\u003C\/p\u003E\u003Cp\u003EDr. Marijn Heule \u2013 School of Computer Science, Carnegie Mellon University\u003C\/p\u003E\u003Cp\u003EDr. Bruno Dutertre \u2013 Automated Reasoning Group, Amazon Web Services\u003C\/p\u003E\u003Cp\u003E\u0026nbsp;\u003C\/p\u003E\u003Cp\u003E\u003Cstrong\u003EAbstract\u003C\/strong\u003E\u003C\/p\u003E\u003Cp\u003EThe model counting problem asks for the number of satisfying assignments for a given set of constraints. It is a fundamental problem in computer science, with applications in probabilistic inference, neural-network verification, computational biology, and quantum computing. In pursuit of ever-greater scalability in these applications, we study randomized approximate model counting, which trades precision for efficiency. These techniques provide an (\u03b5, \u03b4)-guarantee: with probability at least 1-\u03b4, the estimate lies within a multiplicative factor of 1+\u03b5 of the exact count.\u003C\/p\u003E\u003Cp\u003E\u0026nbsp;\u003C\/p\u003E\u003Cp\u003EState-of-the-art approximate counters use hash functions to partition the solution space into cells and estimate the total count from the size of a sampled cell. The practical use of these techniques entails two complementary requirements: computational efficiency for scalability, and assurance of the (\u03b5, \u03b4)-guarantee for dependable results. First, these techniques rely heavily on repeated SAT calls to compute sampled cell sizes, and these expensive calls limit scalability in practice. Second, critical applications such as network reliability and quantitative verification require trust in the returned estimate, whereas it is not immediate that sophisticated implementations retain the probabilistic guarantee established for the abstract algorithms.\u003C\/p\u003E\u003Cp\u003E\u0026nbsp;\u003C\/p\u003E\u003Cp\u003EThis thesis advances the efficiency and trustworthiness of hashing-based approximate model counting. To improve efficiency, we develop three complementary algorithmic innovations: rounding-based confidence amplification, single-query cell estimation, and native PB-XOR solving. These innovations reduce the number of independent estimates, the number of SAT calls per estimate, and the cost of individual calls, respectively, while preserving their stated probabilistic guarantees. To establish trust, we develop the first certification pipeline for approximate model counting by combining a formal PAC proof with per-run certificate checking. It verifies that concrete executions satisfy the conditions for the claimed probabilistic guarantee, assuming trusted randomness. Finally, we demonstrate their practical impact in binarized neural network (BNN) verification, where we integrate BNN-specific reasoning into counting and certification to further improve efficiency while maintaining trust in the resulting estimates.\u003C\/p\u003E\u003Cp\u003E\u0026nbsp;\u003C\/p\u003E\u003Cp\u003ECollectively, these contributions constitute a unified advance toward more practical and dependable approximate model counting for demanding applications. As a concrete demonstration, the resulting approach achieves a 113\u00d7 speedup over the previous state of the art in quantitative BNN verification. Among the instances successfully solved by the counter, 86% are fully certified within the reported resource limits.\u003C\/p\u003E","summary":"","format":"limited_html"}],"field_subtitle":"","field_summary":[{"value":"\u003Cp\u003EEfficient and Trusted Approximate Model Counting\u003C\/p\u003E","format":"limited_html"}],"field_summary_sentence":[{"value":"Efficient and Trusted Approximate Model Counting"}],"uid":"27707","created_gmt":"2026-10-22 13:39:16","changed_gmt":"2026-10-22 13:39:58","author":"Tatianna Richardson","boilerplate_text":"","field_publication":"","field_article_url":"","field_event_time":{"event_time_start":"2026-10-30T13:00:00-04:00","event_time_end":"2026-10-30T15:00:00-04:00","event_time_end_last":"2026-10-30T15:00:00-04:00","gmt_time_start":"2026-10-30 17:00:00","gmt_time_end":"2026-10-30 19:00:00","gmt_time_end_last":"2026-10-30 19:00:00","rrule":null,"timezone":"America\/New_York"},"location":"Klaus 3100","extras":[],"groups":[{"id":"221981","name":"Graduate Studies"}],"categories":[],"keywords":[{"id":"100811","name":"Phd Defense"}],"core_research_areas":[],"news_room_topics":[],"event_categories":[{"id":"1788","name":"Other\/Miscellaneous"}],"invited_audience":[{"id":"78771","name":"Public"}],"affiliations":[],"classification":[],"areas_of_expertise":[],"news_and_recent_appearances":[],"phone":[],"contact":[],"email":[],"slides":[],"orientation":[],"userdata":""}}}