{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T21:01:59Z","timestamp":1760043719958,"version":"3.40.3"},"publisher-location":"Cham","reference-count":45,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783031131875"},{"type":"electronic","value":"9783031131882"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,8,6]],"date-time":"2022-08-06T00:00:00Z","timestamp":1659744000000},"content-version":"vor","delay-in-days":217,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Machine learning compilers are large software containing complex transformations for deep learning models, and any buggy transformation may cause a crash or silently bring a regression to the prediction accuracy and performance. This paper proposes an SMT-based translation validation framework for Multi-Level IR (MLIR), a compiler framework used by many deep learning compilers. It proposes an SMT encoding tailored for translation validation that is an over-approximation of the FP arithmetic and reduction operations. It performs abstraction refinement if validation fails. We also propose a new approach for encoding arithmetic properties of reductions in SMT. We found mismatches between the specification and implementation of MLIR, and validated high-level transformations for , , and  with proper splitting.<\/jats:p>","DOI":"10.1007\/978-3-031-13188-2_19","type":"book-chapter","created":{"date-parts":[[2022,8,5]],"date-time":"2022-08-05T08:16:57Z","timestamp":1659687417000},"page":"386-407","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["SMT-Based Translation Validation for\u00a0Machine Learning Compiler"],"prefix":"10.1007","author":[{"given":"Seongwon","family":"Bang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Seunghyeon","family":"Nam","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Inwhan","family":"Chun","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ho Young","family":"Jhoo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8152-9330","authenticated-orcid":false,"given":"Juneyoung","family":"Lee","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,8,6]]},"reference":[{"key":"19_CR1","unstructured":"https:\/\/reviews.llvm.org\/D114127"},{"key":"19_CR2","unstructured":"https:\/\/reviews.llvm.org\/D106258"},{"key":"19_CR3","unstructured":"Arm NN SDK. https:\/\/www.arm.com\/products\/silicon-ip-cpu\/ethos\/arm-nn"},{"key":"19_CR4","unstructured":"NVIDIA TensorRT. https:\/\/developer.nvidia.com\/tensorrt"},{"key":"19_CR5","unstructured":"Supplementary material. https:\/\/doi.org\/10.5281\/zenodo.6615676"},{"key":"19_CR6","unstructured":"Tensor operator set architecture (TOSA) v0.23.0. https:\/\/developer.mlplatform.org\/w\/tosa\/?v=19"},{"key":"19_CR7","unstructured":"TensorFlow Lite Examples: Text classification. https:\/\/www.tensorflow.org\/lite\/examples\/text_classification\/overview"},{"key":"19_CR8","unstructured":"TensorFlow Lite: Hosted models. TensorFlow Lite: Hosted models"},{"key":"19_CR9","unstructured":"XLA: Optimizing compiler for machine learning. https:\/\/www.tensorflow.org\/xla"},{"key":"19_CR10","doi-asserted-by":"publisher","unstructured":"IEEE standard for floating-point arithmetic: IEEE Std 754-2008, pp. 1\u201370 (2008). https:\/\/doi.org\/10.1109\/IEEESTD.2008.4610935","DOI":"10.1109\/IEEESTD.2008.4610935"},{"key":"19_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/978-3-030-25543-5_10","volume-title":"Computer Aided Verification","author":"H Becker","year":"2019","unstructured":"Becker, H., Darulova, E., Myreen, M.O., Tatlock, Z.: Icing: supporting fast-math style optimizations in a verified compiler. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11562, pp. 155\u2013173. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25543-5_10"},{"key":"19_CR12","doi-asserted-by":"crossref","unstructured":"Boldo, S., et al.: Flocq: a unified library for proving floating-point algorithms in Coq. In: 2011 IEEE 20th Symposium on Computer Arithmetic, pp. 243\u2013252 (2011)","DOI":"10.1109\/ARITH.2011.40"},{"key":"19_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/978-3-030-17462-0_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M Brain","year":"2019","unstructured":"Brain, M., Schanda, F., Sun, Y.: Building better bit-blasting for floating-point problems. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019. LNCS, vol. 11427, pp. 79\u201398. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17462-0_5"},{"key":"19_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1007\/978-3-030-25543-5_8","volume-title":"Computer Aided Verification","author":"M Brain","year":"2019","unstructured":"Brain, M., Niemetz, A., Preiner, M., Reynolds, A., Barrett, C., Tinelli, C.: Invertibility conditions for floating-point formulas. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11562, pp. 116\u2013136. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25543-5_8"},{"key":"19_CR15","doi-asserted-by":"crossref","unstructured":"Brillout, A., et al.: Mixed abstractions for floating-point arithmetic. In: 2009 Formal Methods in Computer-Aided Design, pp. 69\u201376 (2009)","DOI":"10.1109\/FMCAD.2009.5351141"},{"key":"19_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"911","DOI":"10.1007\/978-3-030-81688-9_42","volume-title":"Computer Aided Verification","author":"S Chakraborty","year":"2021","unstructured":"Chakraborty, S., Gupta, A., Unadkat, D.: Diffy: inductive reasoning of array programs using difference invariants. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12760, pp. 911\u2013935. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81688-9_42"},{"key":"19_CR17","doi-asserted-by":"publisher","unstructured":"Churchill, B., et al.: Semantic program alignment for equivalence checking. In: PLDI (2019). https:\/\/doi.org\/10.1145\/3314221.3314596","DOI":"10.1145\/3314221.3314596"},{"key":"19_CR18","doi-asserted-by":"publisher","unstructured":"Cl\u00e9ment, B., et al.: End-to-end translation validation for the halide language. Proc. ACM Program. Lang. 6(OOPSLA1), 1\u201330 (2022). https:\/\/doi.org\/10.1145\/3527328","DOI":"10.1145\/3527328"},{"key":"19_CR19","unstructured":"Cyphers, D.S., et al.: Intel nGraph: an intermediate representation, compiler, and executor for deep learning. arXiv arXiv:1801.08058 (2018)"},{"key":"19_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1007\/978-3-030-25540-4_14","volume-title":"Computer Aided Verification","author":"G Fedyukovich","year":"2019","unstructured":"Fedyukovich, G., Prabhu, S., Madhukar, K., Gupta, A.: Quantified invariants via syntax-guided synthesis. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11561, pp. 259\u2013277. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_14"},{"key":"19_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"519","DOI":"10.1007\/978-3-540-73368-3_52","volume-title":"Computer Aided Verification","author":"V Ganesh","year":"2007","unstructured":"Ganesh, V., Dill, D.L.: A decision procedure for bit-vectors and arrays. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 519\u2013531. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73368-3_52"},{"issue":"OOPSLA","key":"19_CR22","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3428289","volume":"4","author":"S Gupta","year":"2020","unstructured":"Gupta, S., Rose, A., Bansal, S.: Counterexample-guided correlation algorithm for translation validation. Proc. ACM Prog. Lang. 4(OOPSLA), 1\u201329 (2020). https:\/\/doi.org\/10.1145\/3428289","journal-title":"Proc. ACM Prog. Lang."},{"key":"19_CR23","unstructured":"Haller, L., et al.: Deciding floating-point logic with systematic abstraction. In: 2012 Formal Methods in Computer-Aided Design, pp. 131\u2013140 (2012)"},{"key":"19_CR24","unstructured":"Howard, A.G., et al.: MobileNets: efficient convolutional neural networks for mobile vision applications. CoRR abs\/1704.04861 (2017)"},{"key":"19_CR25","unstructured":"Iandola, F.N., et al.: SqueezeNet: AlexNet-level accuracy with 50x fewer parameters and $$<$$1\u00a0mb model size. arXiv arXiv:1602.07360 (2016)"},{"key":"19_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/978-3-319-08867-9_2","volume-title":"Computer Aided Verification","author":"A Komuravelli","year":"2014","unstructured":"Komuravelli, A., Gurfinkel, A., Chaki, S.: SMT-based model checking for recursive programs. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 17\u201334. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_2"},{"key":"19_CR27","doi-asserted-by":"crossref","unstructured":"Komuravelli, A., et al.: Compositional verification of procedural programs using horn clauses over integers and arrays. In: Proceedings of the 15th Conference on Formal Methods in Computer-Aided Design, pp. 89\u201396. FMCAD Inc., Austin, Texas (2015)","DOI":"10.1109\/FMCAD.2015.7542257"},{"key":"19_CR28","doi-asserted-by":"crossref","unstructured":"Kumar, R., et al.: CakeML: a verified implementation of ML. In: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 179\u2013191. Association for Computing Machinery, New York (2014)","DOI":"10.1145\/2535838.2535841"},{"key":"19_CR29","unstructured":"K\u00e4stner, D., et al.: Astr\u00e9e: Proving the absence of runtime errors. In: Embedded Real Time Software and Systems (2010)"},{"key":"19_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"752","DOI":"10.1007\/978-3-030-81688-9_35","volume-title":"Computer Aided Verification","author":"J Lee","year":"2021","unstructured":"Lee, J., Kim, D., Hur, C.-K., Lopes, N.P.: An SMT encoding of LLVM\u2019s memory model for bounded translation validation. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12760, pp. 752\u2013776. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81688-9_35"},{"issue":"POPL","key":"19_CR31","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3158135","volume":"2","author":"W Lee","year":"2018","unstructured":"Lee, W., Sharma, R., Aiken, A.: On automatically proving the correctness of math.h implementations. Proc. ACM Program. Lang. 2(POPL), 1\u201332 (2018)","journal-title":"Proc. ACM Program. Lang."},{"issue":"POPL","key":"19_CR32","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3498717","volume":"6","author":"A Liu","year":"2022","unstructured":"Liu, A., Bernstein, G.L., Chlipala, A., Ragan-Kelley, J.: Verified tensor-program optimization via high-level scheduling rewrites. Proc. ACM Program. Lang. 6(POPL), 1\u201328 (2022). https:\/\/doi.org\/10.1145\/3498717","journal-title":"Proc. ACM Program. Lang."},{"key":"19_CR33","doi-asserted-by":"publisher","unstructured":"Lopes, N.P., et al.: Alive2: bounded translation validation for LLVM. In: PLDI (2021). https:\/\/doi.org\/10.1145\/3453483.3454030","DOI":"10.1145\/3453483.3454030"},{"key":"19_CR34","unstructured":"McCarthy, J.: Towards a mathematical science of computation. In: IFIP Congress (1962)"},{"key":"19_CR35","doi-asserted-by":"crossref","unstructured":"de Moura, L., Bj\u00f8rner, N.: Generalized, efficient array decision procedures. In: 2009 Formal Methods in Computer-Aided Design, pp. 45\u201352 (2009)","DOI":"10.1109\/FMCAD.2009.5351142"},{"key":"19_CR36","doi-asserted-by":"publisher","unstructured":"Necula, G.C.: Translation validation for an optimizing compiler. In: PLDI (2000). https:\/\/doi.org\/10.1145\/349299.349314","DOI":"10.1145\/349299.349314"},{"key":"19_CR37","unstructured":"R\u00fcmmer, P., Wahl, T.: An SMT-LIB theory of binary floating-point arithmetic. In: SMT 2010 Workshop (2010)"},{"key":"19_CR38","unstructured":"Shen, H., et al.: Nimble: efficiently compiling dynamic neural networks for model inference. In: Smola, A., Dimakis, A., Stoica, I. (eds.) Proceedings of Machine Learning and Systems, vol. 3, pp. 208\u2013222 (2021)"},{"key":"19_CR39","doi-asserted-by":"crossref","unstructured":"Shen, Q., et al.: A comprehensive study of deep learning compiler bugs. In: Proceedings of the 29th ESEC\/FSE 2021, pp. 968\u2013980. Association for Computing Machinery, New York (2021)","DOI":"10.1145\/3468264.3468591"},{"issue":"1","key":"19_CR40","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3230733","volume":"41","author":"A Solovyev","year":"2019","unstructured":"Solovyev, A., Baranowski, M.S., Briggs, I., Jacobsen, C., Rakamari\u0107, Z., Gopalakrishnan, G.: Rigorous estimation of floating-point round-off errors with symbolic Taylor expansions. ACM Trans. Program. Lang. Syst. 41(1), 1\u201339 (2019). https:\/\/doi.org\/10.1145\/3230733","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"19_CR41","doi-asserted-by":"publisher","unstructured":"Stepp, M., et al.: Equality-based translation validator for LLVM. In: CAV (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-159","DOI":"10.1007\/978-3-642-22110-159"},{"key":"19_CR42","doi-asserted-by":"publisher","unstructured":"Tristan, J.B., et al.: Evaluating value-graph translation validation for LLVM. In: PLDI (2011). https:\/\/doi.org\/10.1145\/1993316.1993533","DOI":"10.1145\/1993316.1993533"},{"key":"19_CR43","doi-asserted-by":"crossref","unstructured":"Yadav, R., Aiken, A., Kjolstad, F.: DISTAL: the distributed tensor algebra compiler (2022)","DOI":"10.1145\/3519939.3523437"},{"key":"19_CR44","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/978-3-319-94205-6_17","volume-title":"Automated Reasoning","author":"A Zelji\u0107","year":"2018","unstructured":"Zelji\u0107, A., Backeman, P., Wintersteiger, C.M., R\u00fcmmer, P.: Exploring approximations for floating-point arithmetic using UppSAT. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds.) IJCAR 2018. LNCS (LNAI), vol. 10900, pp. 246\u2013262. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-94205-6_17"},{"key":"19_CR45","doi-asserted-by":"crossref","unstructured":"Zhu, K., et al.: DISC: A dynamic shape compiler for machine learning workloads. arXiv arXiv:2103.05288 (2021)","DOI":"10.1145\/3437984.3458838"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-13188-2_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,8,5]],"date-time":"2022-08-05T08:20:52Z","timestamp":1659687652000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-13188-2_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031131875","9783031131882"],"references-count":45,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-13188-2_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"6 August 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Haifa","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Israel","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 August 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 August 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"34","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2022\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"209","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"40","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"11","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"19% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3.9","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"9.7","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}