安杰，中国科学院软件研究所，副研究员，博士生导师

所在部门： 天基综合信息系统全国重点实验室
通信地址： 北京市海淀区中关村南四街4号中国科学院软件研究所
邮政编码： 100190
电子邮件： anjie[@]iscas[DOT]ac[DOT]cn
个人主页： https://leslieaj.github.io/

研究领域

我的研究兴趣在于形式化方法(Formal Methods, FM)，重点是将形式化方法和人工智能技术应用于支撑我们日常生活的智能信息物理融合系统 (Cyber-Physical Systems, CPS），以确保其功能性，鲁棒性，可靠性，安全性，隐私性等。

形式化方法基于严格的数学化和机械化方法来规约、设计、构建、验证、演进计算系统，是改善和确保系统质量的重要方法，其模型、技术和工具已延伸为计算思维的重要载体。
形式化方法已经成功应用于各种硬件 (如芯片) 的设计与验证，在处理软件复杂性和提高软件可靠性方面已显示出无可取代的能力。

CPS深度融合了计算、服务、通信和控制等方面，涉及到航空航天、深空探测、高速铁路、自动驾驶、工业机器人等国家重大需求和世界科技前沿领域。
形式化方法为建模、分析、监控和验证CPS提供了一种严格的途径。然而，CPS高度复杂性，给运用形式化方法有效、高效地解决CPS领域相关问题带来了重大挑战。另一方面，机器学习等人工智能技术已经在许多复杂应用和领域中显示了其有效性，但往往缺乏可解释性和保证。因此，结合轻量级形式化方法和可解释人工智能技术来解决CPS相关问题是十分具有意义的研究领域，但需要在准确性和有效性之间取得平衡。

目前的研究课题包括但不限于：

1. 形式化方法+人工智能：AI for FM, FM for AI
    - 生成式人工智能与定理证明，生成式人工智能与逻辑综合，安全强化学习

2. 模型学习与系统识别
    - 自动机学习(Automata Learning)，动态系统(Dynamical Systems)和混成系统(Hybrid Systems)的学习与推导

3. 实时嵌入式系统和智能信息物理融合系统的设计和分析
    - 数据与机理融合的形式建模(Modeling)与验证(Verification)
    - 基于信号时序逻辑(Signal Temporal Logic)等的监控(Monitoring)和诱错(Falsification)
    - 神经-符号方法结合的控制合成(Control Synthesis)
    - 安全与隐私等复杂性质的误导与强制(Obfuscation and Enforcement)

4. 程序生成与验证


更多内容请见个人主页：https://leslieaj.github.io/

招生信息

本课题组由多位学术功底深厚、有经验负责任、严谨随和的科研工作者和一群热爱学术、积极向上、志趣相投的同学组成，科研经费稳定充足，长期招收想攻读硕士、博士的学生、继续科研工作的博士后以及增长科研经验的实习生，优秀的博士后可聘为中国科学院特别研究助理。本课题组学生和实习生经过一年的扎实学习和工作后，均可形成一篇出色的学术论文 (CCF-A/B)。

面向国家重大需求和世界科技前沿，课题组围绕形式化方法、软件系统和人工智能具备多元化的研究方向，彼此之间亦能够交叉结合，包括但不限于(排序不分先后)：形式化方法(Formal Methods)，信息物理融合系统(Cyber-Physical Systems)，生成式人工智能(Generative Artificial Intelligence)，软件工程(Software Engineering)，自动和交互式定理证明(Automated and Interactive Theorem Proving)，安全强化学习(Safe Reinforcement Learning)，程序验证与生成(Program Verification and Synthesis)等。如果对以上方向感兴趣，并且具有学术热情和自驱力、想变得更加优秀并愿意付出努力，请随时联系：anjie@iscas.ac.cn

招生专业
081202-计算机软件与理论
083500-软件工程
招生方向
形式化方法，信息物理融合系统，程序验证，可信人工智能
软件工程，程序生成

教育背景

2015-09--2020-06   同济大学软件学院   博士
2012-09--2015-03   同济大学软件学院   硕士
2008-09--2012-06   同济大学软件学院   学士

工作经历


工作简历
2024-06~现在, 中国科学院软件研究所, 副研究员
2023-07~2024-05,National Institute of Informatics / 日本国立信息学研究所, 特任助理教授
2022-10~2023-06,National Institute of Informatics / 日本国立信息学研究所, 特任研究员
2020-11~2022-10,Max Planck Institute for Software Systems / 德国马克斯普朗克软件系统所, 博士后研究员

专利与奖励

  • Distinguished Paper Award at ATVA 2025, October 2025
  • Springer Nature High-Impact Publications in Computer Science, August 2020
  • Best Paper Award at FMAC 2019, December 2019

出版信息

   
发表论文
  • Fanpeng Yang, Xing Li, Shuling Wang, Jie An, Zeyu Sun, Shenghua Feng, Wenhan Wang, Weiyi Wang, Naijun Zhan and Fanjiang Xu. How Powerful are LLMs in Generating Program Specifications? In Proceedings of the 43rd International Conference on Machine Learning (ICML 2026).
  • Yue Fang, Zhi Jin, Jie An, Hongshen Chen, Jiangmeng Li, Xiaohong Chen and Naijun Zhan. PRM-PBE: Process Reward Model for Reinforcement Learning in Programming-by-Example. In Proceedings of the 43rd International Conference on Machine Learning (ICML 2026).
  • Zhenya Zhang, Jie An, Paolo Arcaini and Ichiro Hasuo. CauMon: A Tool for Online Monitoring against Signal Temporal Logic. Science of Computer Programming (SCP), 253, 103499:1--103499:5.
  • Hongjing Qing, Jie An and Fanjiang Xu. LLM-Enhanced Two-Stage STL Generation with Structured Intermediate Representation. In Proceedings of the 63rd Design Automation Conference (DAC 2026).
  • Martin Jouve-Genty, Han Su, Sota Sato, Jie An, Zhenya Zhang and Ichiro Hasuo. STLts-Div: Diversified Trace Synthesis from STL Specifications Using MILP. In Proceedings of the 27th International Symposium on Formal Methods (FM 2026).
  • Shenghua Feng, Jie An, Naijun Zhan and Fanjiang Xu. Exact Moment Estimation of Stochastic Differential Dynamics. In Proceedings of the 27th International Symposium on Formal Methods (FM 2026).
  • Hengzhi Yu, Bohan Ma, Mingshuai Chen, Huangying Dong, Jie An, Bin Gu, Naijun Zhan and Jianwei Yin. Derivative-Agnostic Inference of Nonlinear Hybrid Systems. In Proceedings of the 29th ACM International Conference on Hybrid Systems: Computation and Control (HSCC 2026).
  • Hao Wu, Jiyu Zhu, Amir Goharshady, Jie An, Bican Xia and Naijun Zhan. Quantifier Elimination Meets Treewidth. In Proceedings of the 32nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS/ETAPS 2026).
  • Shenghua Feng, Jie An and Fanjiang Xu. Runtime Safety and Reach-Avoid Prediction of Stochastic Systems with Observation-Aware Barrier Functions. In Proceedings of the 40th Annual AAAI Conference on Artificial Intelligence (AAAI 2026).
  • Yue Fang, Zhi Jin, Jie An, Hongshen Chen, Xiaohong Chen and Naijun Zhan. RESTL: Reinforcement Learning Guided by Multi-Aspect Rewards for Signal Temporal Logic Transformation. In Proceedings of the 40th Annual AAAI Conference on Artificial Intelligence (AAAI 2026).
  • Juejie Meng, Jie An, Yong Li, Andrea Turrini and Miaomiao Zhang. SAT-based Synthesis of Minimal Deterministic Real-Time Automata via 3DRTA Representation. In Proceedings of the 27th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2026).
  • Xiaochen Tang, Zhenya Zhang, Miaomiao Zhang and Jie An. Control Synthesis of Cyber-Physical Systems for Real-Time Specifications through Causation-Guided Reinforcement Learning. In Proceedings of the 46th IEEE Real-Time Systems Symposium (RTSS 2025).
  • Ziran Wang, Jie An, Naijun Zhan, Miaomiao Zhang and Zhenya Zhang. On Synthesis of Timed Regular Expressions. In Proceedings of the 46th IEEE Real-Time Systems Symposium (RTSS 2025).
  • Hiroya Fujinami, Masaki Waga, Jie An, Kohei Suenaga, Nayuta Yanagisawa, Hiroki Iseri and Ichiro Hasuo. Componentwise Automata Learning for System Integration. In Proceedings of the 23rd International Symposium on Automated Technology for Verification and Analysis (ATVA 2025), pp. 3--26.
  • Junjie Meng, Jie An, Yong Li, Andrea Turrini, Fanjiang Xu, Naijun Zhan and Miaomiao Zhang. Efficient Decomposition Identification of Deterministic Finite Automata from Examples. In Proceedings of the 11th International Symposium on Dependable Software Engineering: Theories, Tools and Applications (SETTA 2025). To appear.
  • Yue Fang, Zhi Jin, Jie An, Hongshen Chen, Xiaohong Chen and Naijun Zhan. Enhancing Transformation from Natural Language to Signal Temporal Logic Using LLMs with Diverse External Knowledge. In Proceedings of the 63rd Annual Meeting of the Association for Computational Linguistics (ACL 2025). pp. 10446--10458.
  • Chengzi Huang, Behnam Khodabandeloo, Duc Anh Nguyen, Wang Yi, Jie An and Zhenya Zhang. Causality Monitoring for MIMOS. Principles of Formal Quantitative Analysis -- Essays dedicated to Christel Baier on the occasion of her 60th birthday (PFQA-Baier60). pp. 284--300.
  • Yu Teng, Hanyue Chen, Junri Mi, Miaomiao Zhang, Jie An and Naijun Zhan. Active Learning of Deterministic Timed Automata via Timed Classification Tree. SCIENCE CHINA Information Sciences (SCIS), 68(12), 222101:1--222101:17.
  • Zhenya Zhang, Jie An, Paolo Arcaini and Ichiro Hasuo. CauMon: An Informative Online Monitor for Signal Temporal Logic. In Proceedings of the 26th International Symposium on Formal Methods (FM 2024), Part II, pp. 286--304. 
  • Jie An, Qiang Gao, Lingtai Wang, Naijun Zhan and Ichiro Hasuo. The Opacity of Timed Automata. In Proceedings of the 26th International Symposium on Formal Methods (FM 2024), Part I, pp. 620--637.
  • Sota Sato, Jie An, Zhenya Zhang and Ichiro Hasuo. Optimization-Based Model Checking and Trace Synthesis for Complex STL Specifications. In Proceedings of the 36th International Conference on Computer Aided Verification (CAV 2024), Part III, pp. 282--306. 
  • Yu Teng, Miaomiao Zhang and Jie An. Learning Deterministic Multi-Clock Timed Automata. In Proceedings of the 27th International Conference on Hybrid Systems: Control and Computation (HSCC 2024), pp. 6:1--6:11.
  • Zhenya Zhang, Jie An, Paolo Arcaini and Ichiro Hasuo. Online Causation Monitoring of Signal Temporal Logic. In Proceedings of the 35th International Conference on Computer Aided Verification (CAV 2023), Part I, pp. 62--84. 
  • Runqing Xu, Jie An and Bohua Zhan. Active learning of One-Clock Timed Automata using Constraint Solving. In Proceedings of the 20th International Symposium on Automated Technology for Verification and Analysis (ATVA 2022), pp. 249--265.
  • Xiaochen Tang, Wei Shen, Miaomiao Zhang, Jie An, Bohua Zhan and Naijun Zhan. Learning Deterministic One-Clock Timed Automata via Mutation Testing. In Proceedings of the 20th International Symposium on Automated Technology for Verification and Analysis (ATVA 2022), pp. 233--248.
  • Junri Mi, Miaomiao Zhang, Jie An and Bowen Du. Learning Deterministic One-Clock Timed Automata Based on Timed Classification Tree. Journal of Software, 33(8), 2797--2814. (in Chinese)
  • Jie An, Bohua Zhan, Naijun Zhan and Miaomiao Zhang. Learning Nondeterministic Real-Time Automata. ACM Transactions on Embedded Computing Systems (ACM TECS), 20(5s), 99:1--99:26. (Special issue of EMSOFT/ESWEEK 2021) 
  • Xiangyu Jin, Jie An, Bohua Zhan, Naijun Zhan and Miaomiao Zhang. Inferring Switched Nonlinear Dynamical Systems. Formal Aspects of Computing (FAC), 33(3), 385--406.
  • Jie An, Lingtai Wang, Bohua Zhan, Naijun Zhan and Miaomiao Zhang. Learning Real-Time Automata. SCIENCE CHINA Information Sciences (SCIS), 64(9), 192103:1--192103:17.
  • Wei Shen, Jie An, Bohua Zhan, Miaomiao Zhang, Bai Xue and Naijun Zhan. PAC Learning of Deterministic One-Clock Timed Automata. In Proceedings of the 22nd International Conference on Formal Engineering Methods (ICFEM 2020), pp. 129--146.
  • Jie An, Mingshuai Chen, Bohua Zhan, Naijun Zhan and Miaomiao Zhang. Learning One-Clock Timed Automata. In Proceedings of the 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS/ETAPS 2020), pp. 444--462. 
  • Jian Wang, Jie An, Mingshuai Chen, Naijun Zhan, Lulin Wang, Miaomiao Zhang and Ting Gan. From Model to Implementation: A Network-Algorithm Programming Language. SCIENCE CHINA Information Sciences (SCIS), 63(7), 172102:1--172102:17.
  • Mingshuai Chen, Jian Wang, Jie An, Bohua Zhan, Deepak Kapur and Naijun Zhan. NIL: Learning Nonlinear Interpolants. In Proceedings of the 27th International Conference on Automated Deduction (CADE-27), pp. 178--196.
  • Xiaoxue Hou, Jie An, Miaomiao Zhang, Bowen Du and Jing Liu. High-Speed Rail Operating Environment Recognition Based on Neural Network and Adversarial Training. In Proceedings of the 31st IEEE International Conference on Tools with Artificial Intelligence (ICTAI 2019), pp. 840--847.
  • Jie An, Miaomiao Zhang. Verifying Continuous-Time Duration Calculus Against Real-Time Automaton. Journal of Software, 30(7), 1953--1965. (in Chinese)
  • Lingtai Wang, Naijun Zhan and Jie An. The Opacity of Real-time Automata. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems (IEEE TCAD), 37(11), 2845--2856. (Special issue of EMSOFT/ESWEEK 2018)
  • Jie An, Naijun Zhan, Xiaoshan Li, Miaomiao Zhang and Wang Yi. Model Checking Bounded Continuous-Time Extended Linear Duration Invariants. In Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (HSCC 2018), pp. 81--90. (part of CPS Week 2018)

科研活动

科研项目

(1) 中国科学院稳定支持基础领域青年团队计划项目，Co-PI，2026 -- 2030

(2) 软件研究所软件所杰出青年人才发展专项计划项目，项目负责人，2025 -- 2028

(3) 国家高层次海外青年人才项目，信息物理融合系统的形式设计与分析，项目负责人，国家级，2024 -- 2027

(4) 中国科学院“率先行动”引才计划项目，项目负责人，省部级，2024 -- 2028

(5) 软件研究所自主部署基础研究重点项目，智能信息物理融合系统的模型学习，项目负责人，2024 -- 2026

学术服务