Ionia: A Typed Learning Framework and Code Generation Tool Based on Coq

Zhang Xiaoli; Chen Gang; Ma Yingying; Hu Ping

doi:10.7544/issn1000-1239.202440672

Journal of Computer Research and Development > 2025 > Uncorrected proof > DOI: 10.7544/issn1000-1239.202440672 CSTR: 32373.14.issn1000-1239.202440672

Zhang Xiaoli, Chen Gang, Ma Yingying, Hu Ping. Ionia: A Typed Learning Framework and Code Generation Tool Based on Coq[J]. Journal of Computer Research and Development. DOI: 10.7544/issn1000-1239.202440672

Citation:

PDF (1633 KB)

Ionia: A Typed Learning Framework and Code Generation Tool Based on Coq

1.
College of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics, Nanjing 211106
2.
Haiguang Information Technology Co. Ltd, Suzhou, Jiangsu 215028
3.
Shanghai Biren Technology Co. Ltd, Shanghai 201114

More Information

Author Bio:
Zhang Xiaoli: born in 1998. Master. Student member of CCF. Her main research interests include formal methods, Coq, and AI compiler

Chen Gang: born in 1958. PhD, professor, PhD supervisor. His main research interests include programming language design, higher order theorem proving, and AI compiler

Ma Yingying: born in 1997. Master. Her main research interests include formal engineering mathematics, functional language, Coq

Hu Ping: born in 1965. PhD, Chief Software Engineer. Her main research interests include type theory, compiler optimization, and high performance computing
Received Date: August 12, 2024
Revised Date: January 22, 2025
Accepted Date: March 02, 2025
Available Online: March 02, 2025

Graphical Abstract

Abstract

Abstract

As the scale of AI grows rapidly, errors in deep learning applications are also increasing. Existing popular deep learning frameworks are mostly built on the dynamically-typed language Python, which lacks type checking mechanisms. This leads to many errors that cannot be eliminated through type checking at the compilation stage. This paper proposes a strongly-typed functional programming style deep learning framework based on the theorem prover Coq. The framework features typed tensor structures and a powerful static type checking capability. The experimental results demonstrate that the framework can automatically, quickly, and effectively detect shape mismatch errors in deep learning models, and it has greater advantages in terms of speed and detection capability compared to other checking tools. Furthermore, this paper designs and implements a set of rewriting rules that translate functional programming models into C code, realizing the translation from functional neural network operator expressions to multi-core parallel OpenMP C code. According to the results of multiple sets of experiments, the C code for operators generated by this method is on par with manually written code. Furthermore, the speed of the generated neural network operator C code with multi-core parallel optimization has been improved by 4-10 times compared with the sequentially executed operator C code. Additionally, the generated C operators are highly secure and can effectively avoid common issues such as out-of-bounds indexing and memory allocation errors in manually written code.
- deep learning(DL) framework,
- static analysis,
- type system,
- shape error checking,
- Coq,
- multi-core parallel code generation

FullText(HTML)

References (41)

References

[1]	Paszke A, Gross S, Massa F, et al. Pytorch: An imperative style, high-performance deep learning library[J]. Advances in Neural Information Processing Systems, 2019, 32: 8024−8035
[2]	Abadi M, Agarwal A, Barham P, et al. Tensorflow: Large-scale machine learning on heterogeneous distributed systems[J]. arXiv preprint, arXiv: 1603.04467, 2016
[3]	Jia Yangqing, Shelhamer E, Donahue J, et al. Caffe: Convolutional architecture for fast feature embedding[C]//Proc of the 22nd ACM Int Conf on Multimedia. New York: ACM, 2014: 675−678
[4]	Gulli A, Pal S. Deep Learning with Keras[M]. Birmingham: Packt Publishing Ltd, 2017
[5]	Wu Dangwei, Shen Beijun, Chen Yuting. An empirical study on tensor shape faults in deep learning systems[J]. arXiv preprint, arXiv: 2106.02887, 2021
[6]	Jhoo H Y, Kim S, Song W, et al. A static analyzer for detecting tensor shape errors in deep neural network training code[C]//Proc of the 44th ACM/IEEE Int Conf on Software Engineering. New York: ACM, 2022: 337−338
[7]	Lagouvardos S, Dolby J, Grech N, et al. Static analysis of shape in TensorFlow programs[C/OL]//Proc of the 34th European Conf on Object-Oriented Programming (ECOOP 2020). Dagstuhl, Germany: Schloss-Dagstuhl-Leibniz Zentrum für Informatik, 2020[2024-03-10]. https://drops.dagstuhl.de/storage/00lipics/lipics-vol166-ecoop2020/LIPIcs.ECOOP.2020.15/LIPIcs.ECOOP.2020.15.pdf
[8]	Dolby J, Shinnar A, Allain A, et al. Ariadne: Analysis for machine learning programs[C/OL]//Proc of the 2nd ACM SIGPLAN Int Workshop on Machine Learning and Programming Languages. New York: ACM, 2018[2024-03-10]. https://arxiv.org/pdf/1805.04058
[9]	Hattori M, Sawada S, Hamaji S, et al. Semi-static type, shape, and symbolic shape inference for dynamic computation graphs[C]//Proc of the 4th ACM SIGPLAN Int Workshop on Machine Learning and Programming Languages. New York: ACM, 2020: 11−19
[10]	纪泽宇,张兴军,付哲,等. 分布式深度学习框架下基于性能感知的DBS-SGD算法[J]. 计算机研究与发展,2019,56(11):2396−2409 doi: 10.7544/issn1000-1239.2019.20180880 Ji Zeyu, Zhang Xingjun, Fu Zhe, et al. Performance-Aware based dynamic batch size SGD for distributed deep learning framework[J]. Journal of Computer Research and Development, 2019, 56(11): 2396−2409 (in Chinese) doi: 10.7544/issn1000-1239.2019.20180880
[11]	Zhao Tian, Huang Xiaobing, Cao Yu. Deepdsl: A compilation-based domain-specific language for deep learning[J]. arXiv preprint, arXiv: 1701.02284, 2017
[12]	Wang Liang, Zhao Jianxin. Architecture of Advanced Numerical Analysis Systems: Designing a Scientific Computing System Using OCaml[M]. Berlin: Springer, 2023
[13]	INRIA. The coq proof assistant[EB/OL]. 1997[2022-09-15]. https://coq.inria.fr/
[14]	Steuwer M, Fensch C, Lindley S, et al. Generating performance portable code using rewrite rules: From high-level functional expressions to high-performance OpenCL code[J]. ACM SIGPLAN Notices, 2015, 50(9): 205−217 doi: 10.1145/2858949.2784754
[15]	Atkey R, Steuwer M, Lindley S, et al. Strategy preserving compilation for parallel functional code[J]. arXiv preprint, arXiv: 1710.08332, 2017
[16]	麻莹莹,陈钢. 基于Coq的矩阵代码生成技术[J]. 软件学报,2022,33(6):2224−2245 Ma Yingying, Chen Gang. Matrix code generation technology based on Coq[J]. Journal of Software, 2022, 33(6): 2224−2245 (in Chinese)
[17]	Verma S, Su Zhendong. Shapeflow: Dynamic shape interpreter for tensorflow[J]. arXiv preprint, arXiv: 2011.13452, 2020
[18]	Huang A, Hashimoto J, Paszke A, et al. Hasktorch[EB/OL]. 2019[2024-04-13]. https://github.com/hasktorch/hasktorch
[19]	Paszke A, Gross S, Chintala S, et al. Automatic differentiation in pytorch[J/OL]. 2017[2024-05-15]. https://api.semanticscholar.org/CorpusID:40027675
[20]	Thompson S. Haskell: The Craft of Functional Programming[M]. Boston: Addison-Wesley, 2011
[21]	Roesch J, Lyubomirsky S, Weber L, et al. Relay: A new ir for machine learning frameworks[C]//Proc of the 2nd ACM SIGPLAN Int Workshop on Machine Learning and Programming Languages. New York: ACM, 2018: 58−68
[22]	Roesch J, Lyubomirsky S, Kirisame M, et al. Relay: A high-level compiler for deep learning[J]. arXiv preprint, arXiv: 1904.08368, 2019
[23]	Hattori M, Kobayashi N, Sato R. Gradual tensor shape checking[C]//Proc of the 32nd European Symp on Programming. Berlin: Springer, 2023: 197−224
[24]	Eremondi J, Tanter É, Garcia R. Approximate normalization for gradual dependent types[J]. Proceedings of the ACM on Programming Languages, 2019, 3(88): 1−30
[25]	Lehmann N, Tanter É. Gradual refinement types[J]. ACM SIGPLAN Notices, 2017, 52(1): 775−788 doi: 10.1145/3093333.3009856
[26]	Vazou N, Tanter É, Van Horn D. Gradual liquid type inference[J]. Proceedings of the ACM on Programming Languages, 2018, 2(132): 1−25
[27]	Liu A, Bernstein G L, Chlipala A, et al. Verified tensor-program optimization via high-level scheduling rewrites[J]. Proceedings of the ACM on Programming Languages, 2022, 6(55): 1−28
[28]	Ragan-Kelley J, Barnes C, Adams A, et al. Halide: A language and compiler for optimizing parallelism, locality, and recomputation in image processing pipelines[J]. ACM SIGPLAN Notices, 2013, 48(6): 519−530 doi: 10.1145/2499370.2462176
[29]	Danvy O, Millikin K, Nielsen L R. On one-pass CPS transformations[J]. Journal of Functional Programming, 2007, 17(6): 793−812 doi: 10.1017/S0956796807006387
[30]	马振威,陈钢. 基于Coq记录的矩阵形式化方法[J]. 计算机科学,2019,46(7):139−145 doi: 10.11896/j.issn.1002-137X.2019.07.022 Ma Zhenwei, Chen Gang. Matrix formalization based on Coq record[J]. Computer Science, 2019, 46(7): 139−145 (in Chinese) doi: 10.11896/j.issn.1002-137X.2019.07.022
[31]	麻莹莹,马振威,陈钢. 基于Coq的分块矩阵运算的形式化[J]. 软件学报,2021,32(6):1882−1909 Ma Yingying, Ma Zhenwei, Chen Gang. Formalization of block matrix operations based on Coq[J]. Journal of Software, 2021, 32(6): 1882−1909 (in Chinese)
[32]	Shi Zhengpu, Xie Guojun, Chen Gang. CoqMatrix: Formal matrix library with multiple models in Coq[J]. Journal of Systems Architecture, 2023, 143: 102986 doi: 10.1016/j.sysarc.2023.102986
[33]	Mahboubi A, Tassi E. Mathematical components[EB/OL]. 2021[2024-05-15]. https://math-comp.github.io/
[34]	Boldo S, Lelay C, Melquiond G. Coquelicot: A user-friendly library of real analysis for Coq[J]. Mathematics in Computer Science, 2015, 9: 41−62 doi: 10.1007/s11786-014-0181-1
[35]	LeCun Y, Bottou L, Bengio Y, et al. Gradient-based learning applied to document recognition[J]. Proceedings of the IEEE, 1998, 86(11): 2278−2324 doi: 10.1109/5.726791
[36]	Tai Cheng, Xiao Tong, Zhang Yi, et al. Convolutional neural networks with low-rank regularization[J]. arXiv preprint, arXiv: 1511.06067, 2015
[37]	He Kaiming, Zhang Xiangyu, Ren Shaoqing, et al. Deep residual learning for image recognition[C]//Proc of the 29th IEEE Conf on Computer Vision and Pattern Recognition. Piscataway, NJ: IEEE, 2016: 770−778
[38]	Simonyan K, Zisserman A. Very deep convolutional networks for large-scale image recognition[J]. arXiv preprint, arXiv: 1409.1556, 2014
[39]	DiPietro R, Hager G D. Deep learning: RNNs and LSTM[M]//Handbook of Medical Image Computing and Computer Assisted Intervention. San Diego: Elsevier, 2020: 503−519
[40]	McCann B. github[EB/OL]. [2023-09-05]. https://github.com/pytorch/examples
[41]	Spolsky J. stackoverflow [EB/OL]. [2024-02-22]. https://stackoverflow.com/questions

[1]	Jin Dongming, Jin Zhi, Chen Xiaohong, Wang Chunhui. ChatModeler: A Human-Machine Collaborative and Iterative Requirements Elicitation and Modeling Approach via Large Language Models[J]. Journal of Computer Research and Development, 2024, 61(2): 338-350. DOI: 10.7544/issn1000-1239.202330746
[2]	Wang Juanjuan, Wang Hongan. Multi-Agent Multi-Criticality Scheduling Based Self-Healing System of Power Grid[J]. Journal of Computer Research and Development, 2017, 54(4): 720-730. DOI: 10.7544/issn1000-1239.2017.20161026
[3]	He Wenbin, Liu Qunfeng, Xiong Jinzhi. The Error Theory of Polynomial Smoothing Functions for Support Vector Machines[J]. Journal of Computer Research and Development, 2016, 53(7): 1576-1585. DOI: 10.7544/issn1000-1239.2016.20148462
[4]	He Wangquan, Wei Di, Quan Jianxiao, Wu Wei, Qi Fengbin. Dynamic Task Scheduling Model and Fault-Tolerant via Queuing Theory[J]. Journal of Computer Research and Development, 2016, 53(6): 1271-1280. DOI: 10.7544/issn1000-1239.2016.20148445
[5]	Zhao Yu, Wang Yadi, Han Jihong, Fan Yudan, and Zhang Chao. A Formal Model for Cryptographic Protocols Based on Planning Theory[J]. Journal of Computer Research and Development, 2008, 45(9).
[6]	Shi Jin, Lu Yin, and Xie Li. Dynamic Intrusion Response Based on Game Theory[J]. Journal of Computer Research and Development, 2008, 45(5): 747-757.
[7]	Li Ye, Cai Yunze, Yin Rupo, Xu Xiaoming. Support Vector Machine Ensemble Based on Evidence Theory for Multi-Class Classification[J]. Journal of Computer Research and Development, 2008, 45(4): 571-578.
[8]	Lin Jianning, Wu Huizhong. Research on a Trust Model Based on the Subjective Logic Theory[J]. Journal of Computer Research and Development, 2007, 44(8): 1365-1370.
[9]	He Lijian and Zhang Wei. An Agent Organization Structure for Solving DCOP Based on the Partitions of Constraint Graph[J]. Journal of Computer Research and Development, 2007, 44(3).
[10]	Mu Kedian and Lin Zuoquan. Symbolic Dempster-Shafer Theory[J]. Journal of Computer Research and Development, 2005, 42(11): 1833-1842.