欢迎访问中国科学院重庆绿色智能技术研究院!

中心简介

瞄准自动推理和认知科学的发展前沿,密切结合国家重大战略需求和重庆本地经济发展,针对自动推理和隐私计算的基础性和前瞻性科学问题,开展创新型研究和自主性关键技术研发,促进和推动自动推理与信息安全的融合交叉与发展;研发具有自主知识产权的关键技术和软件平台,以满足国家、行业部门,尤其重庆地区的需求;为国家和地方培养高水平的专业人才。 

研究方向

1.自动推理

包括:符号数值混合计算,基于数据的深度融合新推理理论与方法,以及自动推理在自动并行化、程序验证、智慧交通、工业CAD/CAE中的应用。

2.隐私计算

包括:格密码理论、同态加密方案的安全性验证与优化、格密码方案设计、生物大数据的隐私计算模型与方法。

人才队伍

中心现有研究人员9人,包括正高4人,副高2人,中级3人。

中心主任:吴文渊

研究员:冯勇、吴文渊、陈长波、石明全  

副研究员:李轶、陈经纬  

中级研究人员:杨文强、徐娟、张鹏 

冯勇,2003年6月在中国科学院研究生院获得工学博士学位。中国科学院三期知识创新工程重要方向项目“自动推理及其在高新技术领域中的应用”的首席科学家,国家973项目“基于混合计算的误差可控算法”、国家自然科学基金重大研究计划“基于符号-数值计算的误差可控算法及应用”、国家重点研发计划“变革性技术关键科学问题”重点专项“隐私保护数据处理的数学方法”等子课题负责人,主持3项自然科学基金面上项目,入选第三批重庆市学术技术带头人。现从事计算机推理与定理机器证明的研究工作,曾在油藏数值模拟、盆地数值模拟和自适应光学仿真系统的研究中取得重要成果,与张景中院士共同开创了自动推理中的零误差计算学科方向,在国内外本领域著名杂志和会议上发表学术论文60多篇。 

吴文渊,研究员,博导,自动推理与认知中心主任。1999年于北京大学数学学院获得学士学位,2002年于中国科学院研究生院获得计算机硕士学位,2007年8月在加拿大西安大略大学应用数学系获博士学位,而后在西安大略大学和美国密西根大学做博士后。2010年回国到电子科技大学,2011年10月加入中国科学院重庆绿色智能技术研究院。主要从事自动推理、密码学、隐私计算等领域研究,已经主持完成国家自然科学基金两项,中国科学院西部之光联合学者项目一项,中国科学院前沿重点项目一项,重庆市院士牵头科技创新引导专项五项。曾担任了全国计算机数学第6届会议组织委员会主席,成功在重庆举办全国计算机数学大会。同时担任过国际SNC‘14会议程序委员会委员等学术职务。共发表论文50余篇,包括SCI一区刊物Foundations of Computational Mathematics,计算机科学理论著名国际刊物Theoretical Computer Science,国内的顶级学术刊物中国科学、系统科学与复杂性学报、软件学报等。目前担任中国数学会计算机数学专业委员会第二届、第三届委员,美国Math Review专业评论员、SCI期刊JSSC编委。组织团队承担在研国家重大研究计划项目“隐私保护数据处理的数学方法”的子课题。入选2022年度重庆英才-创新领军人才。 

陈长波,2011年8月在加拿大西安大略大学计算机系获博士学位。2011年9月-2013年8月在西安大略大学从事博士后研究,2013年9月加入中国科学院重庆绿色智能技术研究院电子信息研究所自动推理与认知研究中心,先后获得中国科学院西部青年学者和重庆英才青年拔尖人才称号。主要学术贡献包括提出了一系列高效的多项式系统求解算法并应用于生物化学网络平衡点分析、量子关联判定、循环程序的自动并行和优化等。开发的多项式和半代数系统求解器被集成进著名数学软件Maple的多个官方发行版中。迄今在SIAM-ADS、JSC、PRA等杂志和ISSAC、CASC等会议上发表学术论文50余篇。多次担任奥地利、加拿大和德国等自然科学基金会的评审专家及国际会议ISSAC、CASC、ICMS等的程序委员会委员,担任中国数学会计算机数学大会CM2024程序委员会共同主席。曾受邀在中国数学会年会、中国工业与应用数学学会年会、中国数学会计算机数学大会、德国Dagstuhl 研讨会、国际工业与应用数学大会作邀请报告。

依托本中心,已建成生物计算安全重庆市重点实验室

https://scb.cqucas.ac.cn/

研究成果

(一)代表性成果

1.同态加密及其应用

数据的“可用不可见”是数据隐私保护的一种有效手段,为数据流通和数据价值深度挖掘提供有力保障。作为代表性技术之一的全同态加密已逐渐成为这一手段的有效实现方式。此外,基于格密码的同态加密方案还具有抗量子攻击的性质,因而成为密码领域的研究热点。中心从2013年开始开展同态加密的研究工作,在同态方案设计及应用方面均取得突破,这些方案可保障数据的通信、存储以及云端计算安全,具有密文膨胀率小、公钥小、效率高等特点。通过与生物企业的合作,有些方案已经投入到生物医学的实际应用中,为隐私保护的大健康产业创新发展提供了核心技术支撑。

2.零误差计算

数值计算方法不可避免地给计算结果带来多种误差,在航天航空、生物医疗等领域,计算误差可能会带来严重后果。符号计算可以得到问题精确的完备解,但是计算量大且表达式庞大,导致计算效率较低,或者受到计算机内存大小的限制而无法得到结果,往往不能满足实际问题求解的需要。据此,我们提出“零误差计算”的构想,即采用近似计算获得准确结果,研究结合兼具数值计算高效性和符号计算准确性的零误差数值计算高效算法。我们厘清了零误差计算的基础,即从一个实数的近似值恢复出其准确值的前提是这个数属于某个一致离散集合;解决了误差干扰情况下恢复实代数数的PSLQ算法的终止性、正确性和稳定性问题。

3.符号数值计算

我们提出了适用于任意实代数簇的满秩表示以及误差可控的计算奇异实代数簇连通分支样本点的计算方法;针对几乎处处满秩和处处亏秩的不同情况给出了两种误差可控的高维空间代数曲线绘制方法。完整建立了双参数半代数系统误差可控计算的理论并给出了多参数情况下的计算框架,并针对生物系统稳定分析等应用中出现的结构对算法做了改进,将参数半代数系统的求解规模从几变元扩展到20个变元左右。我们融合半代数系统的符号数值计算和机器学习方法,在量子关联判定中的几个重要问题,比如贝尔非局域性如何通过量子导引判定,量子导引和量子纠缠结构的高效判定等中取得新进展。

4.程序正确性验证

软件是信息基础设施的灵魂,但它并不总是让人信任,从而产生“软件可信性”问题。面向应用的程序正确性验证是可信软件基础研究的重要课题之一。其主要研究如何使用数学方法去证明给定程序是否符合预先设定的目标。研究内容包括:程序停机问题证明与不变式构造。我们将Tiwari提出的线性循环程序的终止性问题等价归约为两类特殊程序的终止性问题,并建立了终止性判定的递归算法。同时构造了线性程序不可终止点集合的实多面体吸引集,并建立了基于不动点理论的多项式循环程序终止性判定理论。此外,提出了L-depth Eventual线性秩函数概念,证明了该函数与程序可终止性的内在关联。进一步提出了微分不变式的新定义,丰富了不变式的表现形式。

(二)代表性论文

[1] C. Chen and W. Wu. A Geometric Approach for Analyzing Parametric Biological Systems by Exploiting Block Triangular Structure. SIAM Journal on Applied Dynamical Systems 2022 21:2, 1573-1596.  

[2] Jingwei Chen, Yong Feng, Yang Liu, Wenyuan Wu and Guanci Yang. Non-interactive privacy-preserving naive Bayes classifier using homomorphic encryption. In: Proc. SPNCE '21, pages 192-203. Springer, Cham, 2022  

[3] Bai, Yanan, Yong Feng, and Wenyuan Wu. Privacy-preserving and Communication-efficient Convolutional Neural Network Prediction Framework in Mobile Cloud Computing. KSII Transactions on Internet and Information Systems (TIIS) 15, no. 12 (2021): 4345-4363.  

[4] Yi Li, Wenyuan Wu, Yong Feng. On ranking functions for single-path linear-constraint loops. International Journal on Software Tools for Technology Transfer (2020) 22:655– 666.  

[5] Y. Feng, J. Chen, and W. Wu. The PSLQ algorithm for empirical data. Mathematics of Computation, 317(88):1479-1501, 2019.  

[6] C. Ren and C. Chen. Steerability detection of an arbitrary two-qubit state via machine learning. Physical Review A, 100(2):022314, 2019.  

[7] Changbo Chen, Changliang Ren, Xiang-Jun Ye, and Jing-Ling Chen. Mapping criteria between nonlocality and steerability in qudit-qubit systems and between steerability and entanglement in qubit-qudit systems. Phys. Rev. A, 98:052114, Nov 2018.  

[8] Wenyuan Wu, Greg Reid, and Yong Feng. Computing real witness points of positive dimensional polynomial systems. Theoretical Computer Science, 681:217-231, 2017.  

[9] Wenyuan Wu and Zhonggang Zeng. The numerical factorization of polynomials. Foundations of Computational Mathematics, 17(1):259-286, 2017.  

[10] C. Chen and M. Moreno Maza. Quantifier elimination by cylindrical algebraic decomposition based on regular chains. Journal of Symbolic Computation, 75:74-93, 2016  

(三)代表性项目

1. 隐私保护数据处理的数学方法,国家重点研发计划子课题,2020-2025,200万元

2. 计算机数学核心理论、算法与软件,国家重点研发计划子课题,2023-2028,133万元

3. 基于数值方法的有理数域上准确多元多项式因式分解,国家自然科学基金面上项目,2012-2015,50万元

4. 微分代数方程中的误差可控计算理论与算法,国家自然科学基金面上项目,2015-2018,65万元

5. 采用数值计算求解一类半代数系统全部整数解,国家自然科学基金面上项目, 2017-2020,48万元

6. 参数半代数系统的误差可控计算理论与算法,国家自然科学基金面上项目,2018-2021,48万元

7. 基于同态加密的隐私计算理论与应用,重庆市在渝院士牵头科技创新引导专项,2022-2024,50万元

8. 面向基因数据分析的隐私计算方法及演示软件开发,企事业单位委托项目,2023-2024,98万元

联系方式

联系人:吴文渊 

联系电话:023-65935516

邮箱:zidongtuili@cigit.ac.cn