Automatic Theorem Identification for Scenario-Aware Verification in Ubiquitous Operating Systems

ZHANG Manqing; DONG Yunwei; ZHANG Tao

doi:10.12263/DZXB.20250762

您当前的位置：

首页 >

文章列表页 >

Automatic Theorem Identification for Scenario-Aware Verification in Ubiquitous Operating Systems

更新时间：2026-05-11

- Automatic Theorem Identification for Scenario-Aware Verification in Ubiquitous Operating Systems
- ACTA ELECTRONICA SINICA Pages: 1-19(2026)
- 作者机构：
  
  1.西北工业大学软件学院，陕西西安 710129
  2.澳门科技大学计算机科学与工程学院，澳门 999078
- 作者简介：
- 基金信息：
  
  National Key Research and Development Program of China(2022YFB4501800)
- DOI：10.12263/DZXB.20250762
  CLC： TP311.5;
- Received：04 September 2025，
  
  Accepted：11 March 2026，
  
  Online First：11 May 2026，
- 稿件说明：
移动端阅览
ZHANG Manqing, DONG Yunwei, ZHANG Tao. Automatic Theorem Identification for Scenario-Aware Verification in Ubiquitous Operating Systems[J/OL]. ACTA ELECTRONICA SINICA, 2026, 1-19.
DOI：

ZHANG Manqing, DONG Yunwei, ZHANG Tao. Automatic Theorem Identification for Scenario-Aware Verification in Ubiquitous Operating Systems[J/OL]. ACTA ELECTRONICA SINICA, 2026, 1-19. DOI： 10.12263/DZXB.20250762.

摘要

在泛在计算环境下，操作系统需要在跨计算场景的异构硬件与动态应用之间提供统一支持，以保障系统的连续性与安全性。形式化验证作为确保操作系统内核正确性的关键手段，已经在高可信系统构建中发挥重要作用。其中，交互式定理证明方法为系统提供了严格且可靠的正确性保证。以seL4微内核为代表的验证实践表明，形式化方法虽然能够提供强正确性保证，但需要付出极高的验证成本。seL4团队历时近20年构建了超过百万行的形式化证明，其验证成本远超系统代码开发成本。此外，该验证过程在不同计算场景之间缺乏良好的可迁移性。当开发者将系统移植到新的硬件平台时，验证人员往往需要重新进行大规模证明工作，这一过程严重制约了形式化方法在泛在计算环境中的应用。为解决这一问题，seL4团队提出了将证明划分为计算场景无关部分与计算场景相关部分的思路，从而实现部分证明结果的复用。然而，该划分过程依赖专家经验，研究人员难以高效完成该任务，并且该过程容易引入人为错误。针对上述问题，本文提出一种基于知识蒸馏的自动化方法ArchiDistill。该方法用于识别交互式定理中与计算场景相关的关键语义成分，从而支持验证任务的结构化拆分与跨场景迁移。ArchiDistill通过将大规模预训练模型的语义和模式知识迁移至轻量级模型，并结合多任务蒸馏、引入辅助任务及课程学习策略，实现模型对计算场景相关特性的准确判别与跨平台迁移能力。在实验方面，本文基于seL4内核构建了一个包含16 975个样本的多计算场景验证数据集，并对所提出的方法进行了系统评估。实验结果表明，ArchiDistill在计算场景相关定理识别任务上取得了优异性能。该方法的Accuracy达到0.736 2，Precision为0.707 6，Recall为0.720 0，

-score为0.712 0，这些指标均优于传统模型TextRNN（其Accuracy为0.664 7）以及开源大语言模型Qwen3-32B（其Accuracy为0.709 6，

-score为0.630 2）。该方法在保持轻量化的同时，实现了性能与效率的有效提升。此外，本文在CompCert项目上构建了新的数据集，并使用该数据集验证所提出方法的泛化能

力。实验结果表明，ArchiDistill在跨任务场景中仍能保持良好的稳定性与适用性。

Abstract

In ubiquitous computing environments

operating systems are required to provide unified support across heterogeneous hardware and dynamic applications in diverse computational scenarios

thereby ensuring system continuity and security. Formal verification

as a key technique for guaranteeing the correctness of operating system kernels

has played an essential role in building high-assurance systems. Among various approaches

interactive theorem proving offers the most rigorous and reliable correctness guarantees. The verification of the seL4 microkernel demonstrates that

although formal methods can ensure strong correctness

they incur extremely high verification costs. The seL4 team has spent nearly two decades constructing over one million lines of formal proofs

with verification costs far exceeding those of system development. Moreover

the verification process lacks sufficient portability across different computational scenarios. When the system is ported to a new hardware platform

verification engineers are often required to redo large-scale proofs

which severely limits the applicability of formal methods in ubiquitous computing environments. To mitigate this issue

the seL4 team proposed decomposing proofs into scenario-independent and scenario-dependent components

enabling partial reuse of verification results. However

this decomposition heavily relies on expert knowledge

making it difficult to perform efficiently and prone to human error. To address these challenges

this paper proposes ArchiDistill

an automated method based on knowledge distillation. The proposed method aims to identify key semantic components in interactive theorems that are related to computational scenarios

thereby facilitating structured decomposition of verification tasks and cross-scenario transfer. ArchiDistill transfers semantic and pattern knowledge from large-scale pretrained models to a lightweight mod

and enhances its performance through multi-task distillation

auxiliary tasks

and curriculum learning strategies. This enables accurate identification of scenario-related characteristics and improves cross-platform generalization capability. In the experimental evaluation

we construct a multi-scenario verification dataset based on the seL4 kernel

consisting of 16 975 samples

and conduct a comprehensive assessment of the proposed method. The results show that ArchiDistill achieves superior performance on the task of scenario-related theorem identification

with an accuracy of 0.736 2

precision of 0.707 6

recall of 0.720 0

and

-score of 0.712 0. These results outperform both the traditional model TextRNN with an accuracy of 0.664 7 and the open-source large language model Qwen3-32B with an accuracy of 0.709 6 and an

-score of 0.630 2. While maintaining a lightweight architecture

ArchiDistill achieves an effective balance between performance and efficiency. Furthermore

we construct a new dataset based on the CompCert project to evaluate the generalization capability of the proposed method. Experimental results demonstrate that ArchiDistill maintains strong stability and applicability in cross-task scenarios.

关键词

Keywords

references

Weiser M . The computer for the 21st century [J ] . ACM SIGMOBILE Mobile Computing and Communications Review , 1999 , 3 ( 3 ): 3 - 11 . DOI: 10.1145/329124.329126 http://dx.doi.org/10.1145/329124.329126

曹云帆 , 赵超懿 , 刘瀚之 , 等 . 人机物融合泛在应用的系统支撑 [J ] . 中国科学: 信息科学 , 2025 , 55 ( 3 ): 464 - 480 . DOI: 10.1360/ssi-2024-0338 http://dx.doi.org/10.1360/ssi-2024-0338

Cao Yunfan , Zhao Chaoyi , Liu Hanzhi , et al . System support for ubiquitous human-cyber-physical fusion applications [J ] . Scientia Sinica Informationis , 2025 , 55 ( 3 ): 464 - 480 . (in Chinese) . DOI: 10.1360/ssi-2024-0338 http://dx.doi.org/10.1360/ssi-2024-0338

Mei Hong , Guo Yao . Toward ubiquitous operating systems: A software-defined perspective [J ] . Computer , 2018 , 51 ( 1 ): 50 - 56 . DOI: 10.1109/mc.2018.1151018 http://dx.doi.org/10.1109/mc.2018.1151018

梅宏 , 曹东刚 , 谢涛 . 泛在操作系统: 面向人机物融合泛在计算的新蓝海 [J ] . 中国科学院院刊 , 2022 , 37 ( 1 ): 30 - 37 . DOI: 10.16418/j.issn.1000-3045.20211117009 http://dx.doi.org/10.16418/j.issn.1000-3045.20211117009

Mei Hong , Cao Donggang , Xie Tao . Ubiquitous operating system: Toward the blue ocean of human-cyber-physical ternary ubiquitous computing [J ] . Bulletin of Chinese Academy of Sciences , 2022 , 37 ( 1 ): 30 - 37 . (in Chinese) . DOI: 10.16418/j.issn.1000-3045.20211117009 http://dx.doi.org/10.16418/j.issn.1000-3045.20211117009

Brun M , Achermann R , Chajed T , et al . Beyond isolation: OS verification as a foundation for correct applications [C ] // Proceedings of the 19th Workshop on Hot Topics in Operating Systems . New York : ACM , 2023 : 158 - 165 . DOI: 10.1145/3593856.3595899 http://dx.doi.org/10.1145/3593856.3595899

钱汉伟 , 王承毅 . 操作系统形式化验证综述 [J ] . 河海大学学报(自然科学版) , 2021 , 49 ( 5 ): 473 - 481 . DOI: 10.3876/j.issn.10001980.2021.05.014 http://dx.doi.org/10.3876/j.issn.10001980.2021.05.014

Qian Hanwei , Wang Chengyi . Review of formal verification for operating system [J ] . Journal of Hohai University (Natural Sciences) , 2021 , 49 ( 5 ): 473 - 481 . (in Chinese) . DOI: 10.3876/j.issn.10001980.2021.05.014 http://dx.doi.org/10.3876/j.issn.10001980.2021.05.014

Klein G , Elphinstone K , Heiser G , et al . SeL4: Formal verification of an OS kernel [C ] // Proceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Principles . New York : ACM , 2009 : 207 - 220 . DOI: 10.1145/1629575.1629596 http://dx.doi.org/10.1145/1629575.1629596

Gu Ronghui , Shao Zhong , Chen Hao , et al . CertiKOS: An extensible architecture for building certified concurrent OS kernels [C ] // Proceedings of the 12th USENIX Conference on Operating Systems Design and Implementation . Berkeley : USENIX Association , 2016 : 653 - 669 . DOI: 10.5555/3026877.3026928 http://dx.doi.org/10.5555/3026877.3026928

古金宇 , 李浩 , 夏虞斌 , 等 . BrickOS: 面向异构硬件资源的积木式内核 [J ] . 中国科学: 信息科学 , 2024 , 54 ( 3 ): 491 - 513 . DOI: 10.1360/ssi-2022-0413 http://dx.doi.org/10.1360/ssi-2022-0413

Gu Jinyu , Li Hao , Xia Yubin , et al . BrickOS: Specialized kernels for heterogeneous hardware resources [J ] . Scientia Sinica Informationis , 2024 , 54 ( 3 ): 491 - 513 . (in Chinese) . DOI: 10.1360/ssi-2022-0413 http://dx.doi.org/10.1360/ssi-2022-0413

Gou Jianping , Yu Baosheng , Maybank S J , et al . Knowledge distillation: A survey [J ] . International Journal of Computer Vision , 2021 , 129 ( 6 ): 1789 - 1819 . DOI: 10.1007/s11263-021-01453-z http://dx.doi.org/10.1007/s11263-021-01453-z

Naveed H , Khan A U , Qiu Shi , et al . A comprehensive overview of large language models [J ] . ACM Transactions on Intelligent Systems and Technology , 2025 , 16 ( 5 ): 1 - 72 . DOI: 10.1145/3744746 http://dx.doi.org/10.1145/3744746

Zhang Yu , Yang Qiang . A survey on multi-task learning [J ] . IEEE Transactions on Knowledge and Data Engineering , 2022 , 34 ( 12 ): 5586 - 5609 . DOI: 10.1109/tkde.2021.3070203 http://dx.doi.org/10.1109/tkde.2021.3070203

Bengio Y , Louradour J , Collobert R , et al . Curriculum learning [C ] // Proceedings of the 26th Annual International Conference on Machine Learning . London : IMLS , 2009 : 41 - 48 . DOI: 10.1145/1553374.1553380 http://dx.doi.org/10.1145/1553374.1553380

Ma Zhi , Qiao Lei , Yang Mengfei , et al . Verification of real time operating system exception management based on SPARCv8 [J ] . Journal of Computer Science and Technology , 2021 , 36 ( 6 ): 1367 - 1387 . DOI: 10.1007/s11390-021-1644-x http://dx.doi.org/10.1007/s11390-021-1644-x

马智 , 乔磊 , 杨孟飞 , 等 . 面向SPARC处理器架构的操作系统异常管理验证 [J ] . 软件学报 , 2021 , 32 ( 6 ): 1631 - 1646 . DOI: 10.13328/j.cnki.jos.006241 http://dx.doi.org/10.13328/j.cnki.jos.006241

Ma Zhi , Qiao Lei , Yang Mengfei , et al . Verification of operating system exception management for SPARC processor architecture [J ] . Journal of Software , 2021 , 32 ( 6 ): 1631 - 1646 . (in Chinese) . DOI: 10.13328/j.cnki.jos.006241 http://dx.doi.org/10.13328/j.cnki.jos.006241

Guo Xiaojie , Lesourd M , Liu Mengqi , et al . Integrating formal schedulability analysis into a verified OS kernel [C ] // Proceedings of 31st International Conference on Computer Aided Verification . Cham : Springer , 2019 : 496 - 514 . DOI: 10.1007/978-3-030-25543-5_28 http://dx.doi.org/10.1007/978-3-030-25543-5_28

钱振江 , 刘永俊 , 姚宇峰 , 等 . 微内核架构内存管理的形式化设计和验证方法研究 [J ] . 电子学报 , 2017 , 45 ( 1 ): 251 - 256 .

Qian Zhenjiang , Liu Yongjun , Yao Yufeng , et al . Research on method of formal design and verification of memory management based on microkernel architecture [J ] . Acta Electronica Sinica , 2017 , 45 ( 1 ): 251 - 256 . (in Chinese)

乔磊 , 杨孟飞 , 谭彦亮 , 等 . 基于Event-B的航天器内存管理系统形式化验证 [J ] . 软件学报 , 2017 , 28 ( 5 ): 1204 - 1220 . DOI: 10.13328/j.cnki.jos.005218 http://dx.doi.org/10.13328/j.cnki.jos.005218

Qiao Lei , Yang Mengfei , Tan Yanliang , et al . Formal verification of memory management system in spacecraft using Event-B [J ] . Journal of Software , 2017 , 28 ( 5 ): 1204 - 1220 . (in Chinese) . DOI: 10.13328/j.cnki.jos.005218 http://dx.doi.org/10.13328/j.cnki.jos.005218

徐家乐 , 王淑灵 , 李黎明 , 等 . 操作系统内核权能访问控制的形式验证 [J ] . 软件学报 , 2025 , 36 ( 8 ): 3570 - 3586 .

Xu Jiale , Wang Shuling , Li Liming , et al . Formal verification of capability-based access control in operating system kernel [J ] . Journal of Software , 2025 , 36 ( 8 ): 3570 - 3586 . (in Chinese)

张林雁 , 李希萌 , 施智平 , 等 . 微内核操作系统互斥量模块功能正确性的形式化验证 [J ] . 软件学报 , 2024 , 35 ( 9 ): 4179 - 4192 . DOI: 10.13328/j.cnki.jos.007132 http://dx.doi.org/10.13328/j.cnki.jos.007132

Zhang Linyan , Li Ximeng , Shi Zhiping , et al . Formal verification of functional correctness for mutexes in microkernel [J ] . Journal of Software , 2024 , 35 ( 9 ): 4179 - 4192 . (in Chinese) . DOI: 10.13328/j.cnki.jos.007132 http://dx.doi.org/10.13328/j.cnki.jos.007132

姜菁菁 , 乔磊 , 杨孟飞 , 等 . 基于Coq的操作系统任务管理需求层建模及验证 [J ] . 软件学报 , 2020 , 31 ( 8 ): 2375 - 2387 .

Jiang Jingjing , Qiao Lei , Yang Mengfei , et al . Operating system task management requirements layer modeling and verification based on Coq [J ] . Journal of Software , 2020 , 31 ( 8 ): 2375 - 2387 . (in Chinese)

何韬 , 董威 , 文艳军 . GhostFunc: 一种针对Rust操作系统内核的验证方法 [J ] . 软件学报 , 2025 , 36 ( 8 ): 3494 - 3511 .

He Tao , Dong Wei , Wen Yanjun . GhostFunc: Verification method for Rust operating system kernel [J ] . Journal of Software , 2025 , 36 ( 8 ): 3494 - 3511 . (in Chinese)

Oliveira D B D , Cucinotta T , Oliveira R S D . Efficient formal verification for the Linux kernel [C ] // Proceedings of 17th International Conference on Software Engineering and Formal Methods . Cham : Springer , 2019 : 315 - 332 . DOI: 10.1007/978-3-030-30446-1_17 http://dx.doi.org/10.1007/978-3-030-30446-1_17

Nelson L , Sigurbjarnarson H , Zhang Kaiyuan , et al . Hyperkernel: Push-button verification of an OS kernel [C ] // Proceedings of the 26th Symposium on Operating Systems Principles . New York : ACM , 2017 : 252 - 269 . DOI: 10.1145/3132747.3132748 http://dx.doi.org/10.1145/3132747.3132748

Chen Xiangdong , Li Zhaofeng , Mesicek L , et al . Atmosphere: Towards practical verified kernels in Rust [C ] // Proceedings of the 1st Workshop on Kernel Isolation, Safety and Verification . New York : ACM , 2023 : 9 - 17 . DOI: 10.1145/3625275.3625401 http://dx.doi.org/10.1145/3625275.3625401

Narayanan V , Baranowski M S , Ryzhyk L , et al . RedLeaf: Towards an operating system for safe and verified firmware [C ] // Proceedings of the Workshop on Hot Topics in Operating Systems . New York : ACM , 2019 : 37 - 44 . DOI: 10.1145/3317550.3321449 http://dx.doi.org/10.1145/3317550.3321449

Xu Fengwei , Fu Ming , Feng Xinyu , et al . A practical verification framework for preemptive OS kernels [C ] // Proceedings of 28th International Conference on Computer Aided Verification . Cham : Springer , 2016 : 59 - 79 . DOI: 10.1007/978-3-319-41540-6_4 http://dx.doi.org/10.1007/978-3-319-41540-6_4

王阳 , 方竟成 , 蔡雄 , 等 . 一种面向嵌入式操作系统的形式化验证方法 [J ] . 华东师范大学学报(自然科学版) , 2024 ( 4 ): 1 - 17 . DOI: 10.3969/j.issn.1000-5641.2024.04.001 http://dx.doi.org/10.3969/j.issn.1000-5641.2024.04.001

Wang Yang , Fang Jingcheng , Cai Xiong , et al . A formal verification method for embedded operating systems [J ] . Journal of East China Normal University (Natural Science) , 2024 ( 4 ): 1 - 17 . (in Chinese) . DOI: 10.3969/j.issn.1000-5641.2024.04.001 http://dx.doi.org/10.3969/j.issn.1000-5641.2024.04.001

Zhang Jinkun , Qiao Lei , Yang Hua , et al . Formal modeling and verification of the design layer of space operating systems [C ] //Proceedings of the 11th International Conference on Signal and Information Processing, Networking and Computers (ICSINC): Vol. II . Singapore : Springer , 2024 : 516 - 525 . DOI: 10.1007/978-981-97-2120-7_63 http://dx.doi.org/10.1007/978-981-97-2120-7_63

钱振江 , 黄皓 , 宋方敏 . 操作系统汇编级形式化设计和验证方法 [J ] . 软件学报 , 2016 , 27 ( 12 ): 3143 - 3157 .

Qian Zhenjiang , Huang Hao , Song Fangmin . Method of formal design and verification of OS on assembly layer [J ] . Journal of Software , 2016 , 27 ( 12 ): 3143 - 3157 . (in Chinese)

钱振江 , 黄皓 , 宋方敏 . 操作系统形式化设计与安全需求的一致性验证研究 [J ] . 计算机学报 , 2014 , 37 ( 5 ): 1082 - 1099 . DOI: 10.3724/SP.J.1016.2014.01082 http://dx.doi.org/10.3724/SP.J.1016.2014.01082

Qian Zhenjiang , Huang Hao , Song Fangmin . Research on consistency verification of formal design and security requirements for operating system [J ] . Chinese Journal of Computers , 2014 , 37 ( 5 ): 1082 - 1099 . (in Chinese) . DOI: 10.3724/SP.J.1016.2014.01082 http://dx.doi.org/10.3724/SP.J.1016.2014.01082

钱振江 , 刘苇 , 黄皓 . 操作系统对象语义模型(OSOSM)及形式化验证 [J ] . 计算机研究与发展 , 2012 , 49 ( 12 ): 2702 - 2712 .

Qian Zhenjiang , Liu Wei , Huang Hao . OSOSM: Operating system object semantics model and formal verification [J ] . Journal of Computer Research and Development , 2012 , 49 ( 12 ): 2702 - 2712 . (in Chinese)

Lawall J , Nishimura K , Lozi J P . Should we balance? Towards formal verification of the Linux kernel scheduler [C ] // Proceedings of 31st International Symposium on Static Analysis . Cham : Springer , 2024 : 194 - 215 . DOI: 10.1007/978-3-031-74776-2_8 http://dx.doi.org/10.1007/978-3-031-74776-2_8

Li Weihong , Bilen H . Knowledge distillation for multi-task learning [C ] // Proceedings of Computer Vision - ECCV 2020 Workshops . Cham : Springer , 2020 : 163 - 176 . DOI: 10.1007/978-3-030-65414-6_13 http://dx.doi.org/10.1007/978-3-030-65414-6_13

Xu Yangyang , Yang Yibo , Zhang Lefei . Multi-task learning with knowledge distillation for dense prediction [C ] // Proceedings of the IEEE/CVF International Conference on Computer Vision . Piscataway : IEEE , 2023 : 21493 - 21502 . DOI: 10.1109/iccv51070.2023.01970 http://dx.doi.org/10.1109/iccv51070.2023.01970

Liu Jia , Yue Yinlei , Jin Yongjun , et al . Collaborative estimation of tropical cyclone wind radii with multitask learning and multiteacher distillation [J ] . IEEE Journal of Selected Topics in Applied Earth Observations and Remote Sensing , 2025 , 18 : 12545 - 12558 . DOI: 10.1109/jstars.2025.3567472 http://dx.doi.org/10.1109/jstars.2025.3567472

Jacob G M , Agarwal V , Stenger B . Online knowledge distillation for multi-task learning [C ] // Proceedings of the IEEE/CVF Winter Conference on Applications of Computer Vision . Piscataway : IEEE , 2023 : 2358 - 2367 . DOI: 10.1109/WACV56688.2023.00239 http://dx.doi.org/10.1109/WACV56688.2023.00239

Yi Qingqing , Tang Jingjing , Zeng Yujian , et al . DMMP: A distillation-based multi-task multi-tower learning model for personalized recommendation [J ] . Knowledge-Based Systems , 2024 , 284 : 111236 . DOI: 10.1016/j.knosys.2023.111236 http://dx.doi.org/10.1016/j.knosys.2023.111236

Lê H Â , Pham M T . Leveraging knowledge distillation for partial multi-task learning from multiple remote sensing datasets [C ] // IGARSS 2024 - 2024 IEEE International Geoscience and Remote Sensing Symposium . Piscataway : IEEE , 2024 : 8019 - 8023 . DOI: 10.1109/igarss53475.2024.10641954 http://dx.doi.org/10.1109/igarss53475.2024.10641954

Matei V C , Tăiatu I M , Smădu R A , et al . Enhancing Romanian offensive language detection through knowledge distillation, multi-task learning, and data augmentation [C ] // Proceedings of 29th International Conference on Applications of Natural Language to Information Systems on Natural Language Processing and Information Systems . Cham : Springer , 2024 : 317 - 332 . DOI: 10.1007/978-3-031-70239-6_22 http://dx.doi.org/10.1007/978-3-031-70239-6_22

Yang Zhendong , Zeng Ailing , Li Zhe , et al . From knowledge distillation to self-knowledge distillation: A unified approach with normalized loss and customized soft labels [C ] // Proceedings of the IEEE/CVF International Conference on Computer Vision . Piscataway : IEEE , 2023 : 17139 - 17148 . DOI: 10.48550/arXiv.2303.13005 http://dx.doi.org/10.48550/arXiv.2303.13005

Marvin G , Hellen N , Jjingo D , et al . Prompt engineering in large language models [C ] // Proceedings of ICDICI 2023 on Data Intelligence and Cognitive Informatics . Singapore : Springer , 2024 : 387 - 402 . DOI: 10.1007/978-981-99-7962-2_30 http://dx.doi.org/10.1007/978-981-99-7962-2_30

Lan Weichao , Cheung Y M , Xu Qing , et al . Improve knowledge distillation via label revision and data selection [J ] . IEEE Transactions on Cognitive and Developmental Systems , 2025 , 17 ( 6 ): 1377 - 1388 . DOI: 10.1109/tcds.2025.3559881 http://dx.doi.org/10.1109/tcds.2025.3559881

Sun Wujie , Chen Defang , Siwei Lyu , et al . Knowledge distillation with refined logits [C ] // Proceedings of the IEEE/CVF International Conference on Computer Vision . Piscataway : IEEE , 2025 : 1110 - 1119 . DOI: 10.1109/iccv51701.2025.00111 http://dx.doi.org/10.1109/iccv51701.2025.00111

Limantoro S E . Parameter-free logit distillation via sorting mechanism [J ] . IEEE Signal Processing Letters , 2025 , 32 : 3849 - 3853 . DOI: 10.1109/lsp.2025.3602654 http://dx.doi.org/10.1109/lsp.2025.3602654

Seidenfeld T . Entropy and uncertainty [J ] . Philosophy of Science , 1986 , 53 ( 4 ): 467 - 491 . DOI: 10.1086/289336 http://dx.doi.org/10.1086/289336

Mao Anqi , Mohri M , Zhong Yutao . Cross-entropy loss functions: Theoretical analysis and applications [C ] // Proceedings of the 40th International Conference on Machine Learning . New York : Curran Associates, Inc. , 2023 : 23803 - 23828 . DOI: 10.48550/arXiv.2304.07288 http://dx.doi.org/10.48550/arXiv.2304.07288

Cui Jiequan , Tian Zhuotao , Zhong Zhisheng , et al . Decoupled Kullback-Leibler divergence loss [C ] // Proceedings of the 38th International Conference on Neural Information Processing Systems . New York : Curran Associates Inc. , 2024 : 2370 . DOI: 10.52202/079017-2370 http://dx.doi.org/10.52202/079017-2370

Cipolla R , Gal Y , Kendall A . Multi-task learning using uncertainty to weigh losses for scene geometry and semantics [C ] // 2018 IEEE/CVF Conference on Computer Vision and Pattern Recognition . Piscataway : IEEE , 2018 : 7482 - 7491 . DOI: 10.1109/cvpr.2018.00781 http://dx.doi.org/10.1109/cvpr.2018.00781

鲁银圆 , 许升全 , 谢娟英 . AI-DETR: 自适应加权的可解释目标检测方法 [J ] . 电子学报 , 2025 , 53 ( 7 ): 2279 - 2304 .

Lu Yinyuan , Xu Shengquan , Xie Juanying . AI-DETR: Interpretable object detection method based on adaptive weighting [J ] . Acta Electronica Sinica , 2025 , 53 ( 7 ): 2279 - 2304 . (in Chinese)

Besson F , Blazy S , Wilke P . A verified CompCert front-end for a memory model supporting pointer arithmetic and uninitialised data [J ] . Journal of Automated Reasoning , 2019 , 62 ( 4 ): 433 - 480 . DOI: 10.1007/S10817-017-9439-Z http://dx.doi.org/10.1007/S10817-017-9439-Z

Wang Ruiqi , Yang Zezhou , Gao Cuiyun , et al . An empirical study of knowledge distillation for code understanding tasks [PP/OL ] . V1. arXiv ( 2025-08-21 ). https://arXiv.org/abs/2508.15423 https://arXiv.org/abs/2508.15423 .

Laurens V D M , Hinton G . Visualizing data using t-SNE [J ] . Journal of Machine Learning Research , 2008 , 9 ( 86 ): 2579 - 2605 .

Garreau D , Luxburg U . Explaining the explainer: A first theoretical analysis of LIME [C ] // Proceedings of the Twenty Third International Conference on Artificial Intelligence and Statistics . Palermo, Italy : PMLR , 2020 : 1287 - 1296 .

Views

下载量

CSCD

Alert me when the article has been cited

提交

Tools

Publicity Resources

Infrared-Visible Image Fusion via Heterogeneous Multi-Level Distillation

Towards Incremental Object Detection via Hierarchical Proposal and Decoupled Supervision

Differentially Private with Sparse and Smooth Self-Distillation

Open World Object Detection Based on Causal Prompt Distillation

Multimodal Intent Recognition Based on Hierarchical Semantic-Consistency Learning

Related Author

ZHANG Qi

SONG Hong

LI Jin-fu

MA Shi-han

LIN Yu-cong

YANG Jian

LIANG Jia-wei

LIANG Si-yuan

Related Institution

School of Optics and Photonics, Beijing Institute of Technology

School of Computer Science and Technology, Beijing Institute of Technology

School of Cyber Security, University of Chinese Academy of Sciences

Institute of Information Engineering, Chinese Academy of Sciences

College of Computing and Data Science, Nanyang Technological University

⁰