杨争峰

 杨争峰， 华东师范大学软件工程学院，教授。主要研究方向为大语言模型与自动推理、机器学习与优化、智能系统分析与验证、符号计算。已在CVPR、CAV、AAAI、EMSOFT、FM、ISSAC等国际会议和ACM TECS、IEEE TCAD、JSC、CAD、The Computer Journal等国际期刊上发表学术论文60余篇。近年来主持承担国家自然科学基金、教育部留学人员启动基金、上海市自然科学基金等多个科研课题的研究。

• 大语言模型与自动推理

• 机器学习与优化

• 智能系统分析与验证

  
  

  
  

Students:

 Post-docs:  

• Lydia  Dehbi(PhD from Shanghai University)

 Graduate Students:

• Beibei Xiong(Ph.D'23)

• Niuniu Qi(Ph.D'22)

• Hanrui Zhao(Ph.D'21)

• Lei Wang (M.S.'23), Haojia Shan (M.S.'23), Banglong Liu(M.S.'23)

• Zixuan Yang(M.S.'22),Zhou Zhou(M.S.'22)，Huijiao Xie(M.S.'22)

• Jiahao Chao(M.S.'21)，Jiali Gong(M.S.'21), Li Zhang(M.S.'21)

 Completed Students:

• Xia Zeng(PhD'17, jointly supervised with Prof. Zhenbing Zeng)
  Current Position: associate professor in Southwest University 

• Min Tang(PhD'17, jointly supervised with Prof. Zhenbing Zeng)
  Current Position: associate professor in Guilin University of Electronic Technology

• Wang Lin (PhD'13,jointly supervised with Prof. Zhenbing Zeng)

  Current Position: professor in Zhejiang Sci-Tech University.

• Hongfan Gao(M.S.'21), Xiaochao Tang(M.S.'21), Hao Xue(M.S.'21)

• Xuanming Fu(M.S.'22)，Yidan Zhang(M.S.'22)，Chang Liu(M.S.'21)，Qianting Zhou(M.S.'21)

• Xiangkun Li(M.S.'20)，Wenjun Du (M.S.'19)，Minjie Shen (M.S.'18)，Lilei Wang (M.S.'17)

• Hao Yuan  (M.S.'16)，Kai Song (M.S.'15)，Jian Liu (M.S.'15)，Yijun Zhu (M.S.'14)

Software:

VerifyRealRoots: a MATLAB package for computing real verified solutions of polynomial systems of    equations and inequalities.

Publications :

Google Citation:https://scholar.google.ca/citations?user=jBDmZeQAAAAJ&hl=en

DBLP: https://dblp.uni-trier.de/pers/y/Yang:Zhengfeng.html

2024:

• [65]  H. Zhao,, N. Qi, M. Ren, X. Zeng, Z. Zeng and  Z. Yang*,  Neural Barrier Certificates of NN-Controlled Continuous Systems via  Counterexample-Guided Learning, accepted for publication in DAC'2024. (CCF-A)

• [64]  X. Zeng, B. Liu, Z. Zeng, Z. Liu and Z. Yang*, Safe Controller Synthesis for Nonlinear Systems via  Reinforcement Learning and PAC Approximation, accepted for publication in DAC'2024. (CCF-A).

• [63] N. Qi, D. Lydia, B. Liu, Z. Yang and  Z. Zeng, Global Optimization for Heilbronn Problem  of Convex Polygons  Based on Bilinear Matrix Inequalities Solving, accepted for publication in Journal of System Science and Complexity, 2024. 

2023:

• [62] Z.Yang, L.Zhang, X.Zeng,C.Tang,C.Peng,Z.Zeng,Hybrid Controller Synthesis for Nonlinear Systems  Subject to Reach-avoid Constraints, CAV'2023, 304-325.(CCF-A)

• [61] H. Zhao, N. Qi, L. Dehbi, X. Zeng, Z. Yang*,  Formal Synthesis of Neural Barrier Certificates for Continuous Systems via Counterexample Guided  Learning. Accepted for publication in ACM Trans. Embedded Computing Systems  (Special issue of EMSOFT'2023). (CCF-B)

• [60] J. Chao, Z. Zhou, H. Gao, J. Gong, Z. Yang*, Z. Zeng, Lydia Dehbi,Equivalent Transformation and Dual Stream Network Construction for Mobile Image Super-Resolution, CVPR'2023,  14102-14111. (CCF-A)

• [59] Z. Zhou,  J.Chao, J.Gong, H. Gao, Z.Zeng and Z. Yang*, Enhancing Real-Time Super Resolution with Partial Convolution and Efficient Variance Attention. Accepted for publication in ACM'MM2023. (CCF-A)

• [58] X. Zeng, Z. Yang*, L. Zhang, X. Tang, Z. Zeng and Z. Liu, Safety Verification of Nonlinear Systems with Bayesian Neural Network Controllers. AAAI'2023，15278-15286， (Oral,CCF-A)

• [57] J. Chao, Z. Zhou, H. Gao, J. Gong,  Z.Yang*, Z. Zeng,  A Novel Learnable Interpolation Approach for Scale-Arbitrary Image Super-Resolution. IJCAI'2023, 564-572. (CCF-A)

• [56] H. Zhao, X. Zeng, N. Qi, Z. Yang* and Z. Zeng,  Safe DNN-type Controller Synthesis for Nonlinear Systems via Meta Reinforcement Learning. Accepted for publication in DAC'2023. (CCF-A)
  

• [55] J. Gong, H. Gao,J. Chao, Z. Zhou, Z. Yang* and Z. Zeng,  Kernel Estimation and Deconvolution for Blind Image Super-resolution, ICASSP'2023. (CCF-B)
  

• [54] Z. Yang, H. Zhao, L. Zhi, VerifyRealRoots: A Matlab Package for Computing Verified Real Solutions of Polynomial Systems of Equations and Inequalities. Journal of System Sciences and Complexity,36(2),866-883,2023. (JCR Q2)

2022:

• [53] X. Fu, Z. Yang*, H. Xue, J.Wang, Z. Zeng, Robust Training with Feature-Based Adversarial Examples,  26th ICPR,2957-2963.

• [52] H. Xue, X. Zeng, W. Lin, Z. Yang*, C. Peng and Z. Zeng, An RNN-Based Framework for the MILP Problem in Robustness Verification of Neural Networks.ACCV, 1842-1857, 2022.
  

• [51] X. Tang, Z. Yang*, X. Fu, J. Wang, Z. Zeng, Improving Adversarial Robustness of Deep Neural Networks via Linear Programming.  TASE, 326-343, 2022.

• [50] Z. Zeng, Y. Xu, Y. Chen, Z. Yang,  A Mechanical Method for Isolating Locally Optimal Points of Certain Radical Functions. CASC, 377-396, 2022.
  

• [49] W. Lin, Z. Yang*, Z. Ding, Reachable Set Estimation and Safety Verification of Nonlinear Systems via Iterative Sums of Squares Programming. Journal of System Sciences and Compelxity, 35(3), 1154-1172, 2022. (JCR Q2)

2021:

• [48] Z. Yang,  Y. Zhang, W. Lin, X. Zeng, X. Tang, Z. Zeng and Z. Liu, An Iterative Scheme of Safe Reinforcement Learning for Nonlinear Systems via Barrier Certificate Generation. 33rd International Conference on Computer-Aided Verification(CAV'21), 467-490. (CCF-A)

• [47] Q. Zhao, X. Chen, M. Sha, Z. Yang, W. Lin, E. Tang and X. Li, Synthesizing ReLU Neural Networks with Two Hidden Layers as Barrier Certificates for Hybrid Systems. HSCC'21, 1-11. (CCF-B)

• [46] M. Sha, X. Chen, Y. Ji, Q. Zhao, Z. Yang, W. Lin, E. Tang, Q. Chen, X. Li,  Synthesizing Barrier Certificates of Neural Network Controlled Continuous Systems via Approximations. DAC'2021,631:636. (CCF-A)

  
  

  
  

2020:

• [45] C. He, C. Peng, N. Li, X. Chen, Z. Yang, Z. Hu, CIFEF: Combining Implicit and Explicit Features for Frendship Inference in Location-Based Social Networks. KSEM,168-180,2020.  

• [44] C. Liu, W. Lin and Z. Yang, Generating Adversarial Texts for Recurrent Neural Networks, ICANN, 39-51,2020.

• [43] X. Chen, C. Peng, W. Lin,  Z. Yang*, Y. Zhang and X. Li,  A Novel Approach for Solving the BMI  Problem in Barrier Certificates Generation, 32nd International Conference on Computer-Aided Verification(CAV2020), 582-603.(CCF-A)

•  [42] Z. Zeng, J. Wang, Z. Yang and K. Hidetsune, A Mechanical Proof of the Property of Derived Sets in General Topology(in Chinese), Science China, 2020,50:1-26.
  

• [41] Zhengfeng Yang, M. Wu, W. Lin, An Efficient Framework for Barrier Certificate Generation of Uncertain Nonlinear Hybrid Systems, Nonlinear Analysis: Hybrid Systems(NAHS),100837, 2020.  (JCR Q1）

  
  

Before 2020:

• [40] Wang Lin, Zhengfeng Yang*, Xin Chen, Qingye. Zhao, Xuandong  Li, Zhiming Liu and Jifeng He, Robustness Verification of Classification Deep Neural Networks via Linear Programming, CVPR2019, 11418-11427. （CCF-A)

• [39] Li-yong Shen, Sonia Perez-Diaz,  Zhengfeng Yang*, Numerical Proper Reparametrization of Space Curves and Surfaces,Computer-Aided Design,116,Pages 1-16,2019. (CCF-B)

• [38] Zhenbing Zeng, Jianlin Wang, Zhengfeng Yang, Multi-Agent Automated Reasoning Toward to Machine Self-Aware(Case Study), TASE 2019.

• [37] Yifan Zhang, Zhengfeng Yang*, Wang Lin, Huibiao Zhu, Xin Chen, Xuandong Li, Safety Verification of Nonlinear Hybrid Systems Based on Bilinear Programming. IEEE Trans. on CAD of Integrated Circuits and Systems（Special issue of EMSOFT2018) 37(11): 2768-2778,2018. (CCF-A)

• [36] Erdal Imamoglu, Erich L. Kaltofen, Zhengfeng Yang*:Sparse Polynomial Interpolation With Arbitrary Orthogonal Polynomial Bases. ISSAC 2018: 223-230.

• [35] Wenjun Du, Zhengfeng Yang*, Huibiao Zhu:A Fully Abstract Encoding for Sub Asynchronous Pi Calculus. TASE 2018: 17-27.

• [34] Chao Huang, Xin Chen, Wang Lin,Zhengfeng Yang* and Xuandong Li, Probabilistic Safety Verification of Stochastic Hybrid Systems Using Barrier Certificates,ACM Trans. Embedded Comput. Syst.(Special issue of EMSOFT2017),16(5): 186:1-186:19,2017.  (CCF-B)

• [33] Wang Lin, Min Wu, Zhengfeng Yang* and Zhenbing Zeng,Verification for non-polynomial hybrid systems using rational invariants, The Computer Journal,60(5), 675-689, 2017.(CCF-B)

• [32] Xia Zeng, Wang Lin, Zhengfeng Yang and Zhenbing Zeng, Linear Invariant Generation for Verification of Nonlinear Hybrid Systems via Conservative Approximation, Science China Information Sciences,60(3), 2017. (CCF-A)

• [31] Zhengfeng Yang, Chao Huang, Xin Chen, Wang Lin and Zhiming Liu, A Linear Programming Relaxation Based Approach for Generating Barrier Certificates of Hybrid Systems, the 21st International Symposium on Formal Methods(FM2016),721-738. (CCF-A)

• [30] Xia Zeng,Wang Lin, Zhengfeng Yang*, Xin Chen and Lilei Wang, Darboux-type Barrier Certificates for Safety Verification of Nonlinear Hybrid Systems, ACM/IEEE Conference on Embedded Software (EMSOFT),Article 11, 10 pages,2016.  (CCF-B)

• [29] Min Tang, Zhengfeng Yang and Zhenbing Zeng, Resultant Elimination via Implicitation Equation Interpolation,Journal of System Sciences and Complexity,29(5):1411-1435,2016. 

• [28] Erich L.Kaltofen and Zhengfeng Yang*, Sparse Multivariate Function Recovery With a Small Number of Evaluations, Journal of Symbolic Computation,75,209 - 218,2016.(CCF-B)

• [27] Zhengfeng Yang, Wang Lin and Min Wu, Exact verification of hybrid systems based on bilinear SOS representation. ACM Transactions on Embedded Computing Systems, 14(1), 1-19,2015.  (CCF-B)

• [26] Erich L. Kaltofen and Zhengfeng Yang, Sparse multivariate function recovery with a high error rate in the evaluations, Proceedings of the 39th International Symposium on Symbolic and Algebraic Computation , 280-287, 2014, ACM Press.

• [25] Wang Lin, Min Wu, Zhengfeng Yang and Zhenbing Zeng, Safety verification of nonlinear systems based on rational invariants, SNC'14 Proc. 2014 Internat. Symp. on Symbolic-numeric Comput.,107-108.

• [24] Wang Lin, Min Wu, Zhengfeng Yang and Zhenbing Zeng, Proving total correctness and generating preconditions for loop programs via symbolic-numeric computation methods, Frontiers of Computer Science 8(2), 192-202,2014.

• [23] Wang Lin, Min Wu, Zhengfeng Yang, Zhenbing Zeng，Exact safety verification of hybrid systems using sums-of-squares representation. Science China Information Sciences 57(5): 1-13, 2014. (CCF-A)

• [22] Min Wu, Zhengfeng Yang, Wang Lin, Domain-of-attraction estimation for uncertain non-polynomial systems, Communications in Nonlinear Science and Numerical Simulation,19(9),3044-3052,2013.

• [21] Zhengfeng Yang, Lihong Zhi and Yijun Zhu, Verified Error Bounds for Real Solutions of Positive-dimensional Polynomial Systems, In Proceedings of the 38th International Symposium on Symbolic and Algebraic Computation ,2013,  pp371--378，ACM Press.

• [20] Erich L. Kaltofen and Zhengfeng Yang, Sparse multivariate function recovery from values with noise and outlier errors,In Proceedings of the 38th International Symposium on Symbolic and Algebraic Computation ,2013,  pp219--226，ACM Press.

• [19] Erich L. Kaltofen and Bin Li and Zhengfeng Yang and Lihong Zhi，Exact certification in global polynomial optimization via sums-of-squares of rational functions with rational coefficients,Journal of Symbolic Computation，2012，47(1):1-15. 

• [18] Erich Kaltofen, Wen-shin Lee and Zhengfeng Yang, Fast estimates of Hankel matrix condition numbers and numeric sparse interpolation.In SNC'11 Proc. 2011 Internat. Workshop on Symbolic-Numeric Comput. pages 130-136, ACM Press.

•  [17] Min Wu, Zhengfeng Yang, Generating invariants of hybrid systems via sums-of-squares of polynomials with rational coefficients. In SNC'11 Proc. 2011 Internat. Workshop on Symbolic-Numeric Comput. pages 104-111, ACM Press.

• [16] Wang Lin, Min Wu, Zhengfeng Yang,and Zhenbing Zeng, Proving total correctness of loop programs via symbolic-numeric computation method, In MACIS'11Proc. of 4th International Conference on Mathematical Aspects of Computer and Information Sciences, pages 149-161.

• [15] Zijia Li‚ Zhengfeng Yang and Lihong Zhi‚ Blind image deconvolution via fast approximate GCD. In ISSAC'10 Proc. 2010 Internat. Symp. Symbolic Algebraic Comput. pages 155-162, ACM Press.

• [14] Liyong Shen‚ Min Wu‚ Zhengfeng Yang and Zhenbing Zeng‚ Generating Exact Nonlinear Ranking Functions by Symbolic-Numeric Hybrid Method‚Journal of System Sciences and Complexity, 26 (2), 291-301，2013.

• [13] Erich Kaltofen‚ Zhengfeng Yang and Lihong Zhi‚ A Proof of the Monotone Column Permanent(MCP) Conjecture for Dimension 4 via Sums-Of-Squares of Rational Functions. In SNC´09 Proceedings‚ Pages 65-69‚ ACM Press.

• [12] Liyong Shen‚ Min Wu‚ Zhengfeng Yang and Zhenbing Zeng‚ Finding Positively Invariant Sets of a Class of Nonlinear Loops via Curve Fitting. In SNC´09 Proceedings‚ Pages 185-190‚ ACM Press, pages 167-174.  

• [11] Liyong Shen‚ Min Wu and Zhengfeng Yang‚Simplification of numerical rational surfaces. In 2009 International Joint Conference on Computational Sciences and Optimization‚pages 617-621.

• [10] Erich Kaltofen‚ Bin Li‚ Zhengfeng Yang‚and Lihong Zhi‚Exact certification of global optimality of approximate factorizations via rationalizing sums-of-squares with floating point scalars.In ISSAC 2008 Proceedings 2008 International Symposium on Symbolic Algebraic Computation ACM Press‚ New York‚ N.Y.‚ 2008‚ pages 155-163.

• [9] Erich Kaltofen‚ John May‚ Zhengfeng Yang‚ and Lihong Zhi. Approximate factorization of multivariate polynomials using singular value decomposition. J. Symbolic Comput.‚ 43(5):359-376.

• [8] Erich Kaltofen and Zhengfeng Yang‚ On exact and approximate interpolation of sparse rational functions. In ISSAC 2007 Proceedings 2007 International Symposium on Symbolic Algebraic Computation ACM Press‚ New York‚ N.Y.‚ 2007‚ pages 203-210.

• [7] Erich Kaltofen‚ Bin Li‚ Kartik Sivaramakrishnan‚ Zhengfeng Yang‚and Lihong Zhi. Lower bounds for approximate factorizations via semidefinite programming (extended abstract). In SNC´07 Proceedings 2007 International Workshop on Symbolic-Numeric Computation} ACM Press‚ New York‚ N.Y.‚ 2007‚ pages 203-204.

• [6] Erich Kaltofen‚ Zhengfeng Yang and Lihong Zhi‚ On probabilistic analysis of randomization in hybrid symbolic-numeric algorithms. In SNC´07 Proceedings 2007 InternationalWorkshop on Symbolic-Numeric Computation ACM Press‚ New York‚ N.Y.‚ 2007‚ pages11-17.

• [5] Erich Kaltofen‚ Zhengfeng Yang and Lihong Zhi‚ Approximate greatest common divisors of several polynomials with linearly constrained coefficients and singular polynomials. In ISSAC 2006 Proceedings 2006 International Symposium on Symbolic Algebraic Computation ACM Press‚ New York‚ N.Y.‚ 2006‚ pages 169-176. Full version‚ 30 pages. Submitted‚ Nov. 2007.

• [4] Erich Kaltofen, Zhengfeng Yang and Lihong Zhi, Structured low rank approximation of a generalized Sylvester matrix, Proc. of the Seventh Asian Symposium on Computer Mathematics(Seoul,South Korea,2005),S. Pae and H. Park, Eds., Korea Institute for Advanced Study, Pages 219-222.

• [3] Bingyu Li‚ Zhengfeng Yang and Lihong Zhi‚ Fast low rank approximation of a Sylvester matrix by structured total least norm‚ J. JSSAC (Japan Society for Symbolic and Algebraic Computation)‚ Vol. 11‚ No. 3-4‚ 165-174‚ 2005.

• [2] Shuhong Gao‚ Erich Kaltofen‚John P. May‚Zhengfeng Yang andLihong Zhi‚ Approximate factorization of multivariate polynomials via differential equations. In ISSAC 2004 Proceedings 2004 International Symposium on Symbolic Algebraic Computation ACM Press‚ New York‚ N.Y.‚ 2004‚

  Book Chapters:

• [1] Erich Kaltofen‚ Zhengfeng Yang‚ and Lihong Zhi. Structured low rank approximation of a Sylvester matrix. In Symbolic-Numeric Computation. Trends in Mathematics. Birkhser-Verlag‚ Basel‚ Switzerland‚ 2007‚ pages 69-83.

Selected Talks:

• Darboux-type Barrier Certificates for Safety Verification of Nonlinear Hybrid Systems,Oct. 2016, Pittsburgh, USA.

• Sparse multivariate function recovery from values with noise and outliererrors,July 2016, Waterloo, Canada.

• Error-correcting sparse interpolation of multivariate function,Workshop on Linear Computer Algebra and Symbolic-Numeric Computation, Oct. 2015, Toronto, Canada. 

• Sparse polynomial interpolation with arbitrary orthogonal polynomial bases,the International Congress on Industrial and Applied Mathematics (ICIAM2015), Aug. 2015, Beijing, China.

• Sparse multivariate function recovery from values with noise and outlier errors,SIAM Conference on Applied Algebraic Geometry(SIAM'AG15), Aug.2015,Daejeon,Korea.

• Sparse multivariate function recovery with a high error rate in evaluations,the International Symposium on Symbolic and Algebraic Computation(ISSAC), Jul. 2014, Kobe, Japan.

• Finite-time Reachability Analysis of Nonlinear Systems, NIMS Workshop on Optimization and Algebraic Geometry,Jun.2014,Daejeon,Korea.
  

• Exact Safety Verification of Hybrid Systems Based on Bilinear SOS Representation, 20th Conference of the Inter national Federation of Operational Research Societies(IFORS), Jul. 2014, Barcelona, Spain.

• Safety Verification of Interval Hybrid Systems Based on Reliable SOS Programming, CDZ Workshop GZ1115 on Computation and Reasoning with Constraints, Oct. 2014, Beijing, China.

• Sparse Multivariate Function Recovery from Values with Noise and Outlier Errors,SIAM Conference on Applied Algebraic Geometry(SIAM'AG13), Jul. 2013, Colorado, USA.

• Exact Safety Verification of Hybrid Systems Based on Symbolic-Numeric Computation,Asian Symposium on Computer Mathematics(ASCM), Oct. 2012,Beijing, China. 

• Exact Safety Verification of Hybrid Systems Based on Hybrid Symbolic-Numeric Computation, Colloquium on Logic in Engineering Dependable Software, Nov. 2012, Yunnan, China.

• Generating invariants of hybrid systems via sums-of-squares of polynomials with rational coefficients, the International Workshop on Symbolic-Numeric Computation(SNC2011), Jul. 2011. San Jose, USA.

• Fast estimates of Hankel matrix condition numbers and numeric sparse interpolation, the International Workshop on Symbolic-Numeric Computation(SNC2011), Jul. 2011. San Jose, USA.

• Blind image deconvolution via fast approximate GCD,SIAM/MSRI Workshop on Hybrid Methodologies, Nov. 2010, Berkeley, California.

• Exact Certification in Global Polynomial Optimization via Sums-of-Squares of Rational Functions with Rational Coefficients, Computer-assisted proofs - tools, methods and applications, Nov. 2009, Dagstuhl, Germany.

• Poster,Exact Certification in Global Polynomial Optimization via Sums-of-Squares of Rational Functions with Rational Coefficients,the International Conference of Mathematics Mechanization(ICMM), May 2009, Beijing, China.

• Exact Certification of Global Optimality of Approximate Factorizations via Rationalizing Sums-of-squares with Floating Point Scalars,the International Symposium on Symbolic and Algebraic Computation(ISSAC), Jul. 2008,Hagenberg, Austria.

• Early Termination in Sparse Interpolation of Rational Functions, Computers in Scientific Discovery IV(CSD-IV'2008), Apr. 2008, Shanghai, China.

• On Probabilistic Analysis of Randomization in Hybrid Symbolic-Numeric Algorithms, Department of Mathematics, Simon Fraser University, Dec. 2007, Canada.

• On Exact and Approximate Interpolation of Sparse Rational Functions,the International Symposium on Symbolic and Algebraic Computation(ISSAC), Jul. 2007, Waterloo, Canada.

• Poster, Early Termination in Sparse Interpolation of Rational Functions,East Coast Computer Algebra Day( ECCAD), Apr.2007, Maryland,USA.

• On Exact and Approximate Interpolation of Sparse Rational Functions,NCSU Symbolic Computation Seminar,Mar. 2007.

• Approximate greatest common divisors of several polynomials with linearly constrained coefficients and singular polynomials,the International Symposium on Symbolic and Algebraic Computation (ISSAC), Jul. 2006, Genova, Italy.

• Structured Low Rank Approximation of a Sylvester Matrix,the International Workshop on Symbolic-Numeric Computation(SNC2005),Jul. 2005, Xi'an, China.

• Approximate Factorization of Multivariate Polynomials via Differential Equations,the 6-th International Workshop on Mathematics Mechanization, May 2004, Shanghai, China.

Work Related Links:

   This is the main website for interval computations.

   The website for global optimization test problems.