自动推理与认知实验室依托于中国科学院重庆绿色智能技术研究院,她的前身是中国科学院成都计算机应用研究所自动推理实验室,培养了中国科学院院士1人,国家杰出青年基金获得者2人和学术带头人9人。

现实验室结合国家、重庆市的经济、科技发展需求,经重庆研究院批准又建立了“多领域统一建模”和“视频语义认知”两个新的研究方向,既是自动推理技术在先进制造和认知科学的前沿应用,又为人工智能、应用数学、计算机代数等基础研究提出新的科学问题。目前固定科研人员有46人,包括1位中国科学院院士、7名研究员、6名副研究员,其中14人是研究院引进的海外博士;客座教授共5位,其中1位是美国国家工程院院士,2位是中国科学院特聘研究员。

总体定位:瞄准国际自动推理领域发展前沿,密切结合国家重大战略需求和重庆本地的经济发展,针对基础性和前瞻性科学问题,开展创新性研究和自主性关键技术研发。

查看详情

程序正确性验证

随着计算机和互联网的迅猛发展,以通信、存储和计算为核心的信息基础设施已经渗透到政治、经济、军事、文化以及社会的各个层面。软件是信息基础设施的灵魂,但它并不总是让人信任,从而产生“软件可信性”问题。面向应用的程序正确性验证是可信软件基础研究的重要课题之一。

其主要研究如何使用数学方法去证明给定程序是否符合预先设定的目标。内容包括:程序停机问题证明与不变式构造。

符号混合计算

数值计算采用有限精度浮点数近似计算,在工业和工程中广泛使用,效率高但误差累积造成精度有时过低,通常只能得到局部解。符号计算可以对带符号的数学表达式精确操作,能准确得到问题的全部解但受制于中间过程膨胀效率相对较低。

如何结合高效但有误差的数值计算与精确但低效的符号计算获得满足目标精度的结果是符号数值混合计算的主要研究内容。

零误差计算

数值计算方法不可避免地给计算结果带来多种误差,在航天航空、生物医疗等领域,计算误差可能会带来严重后果。符号计算可以得到问题精确地完备解,但是计算量大且表达式庞大,导致计算效率较低,或者受到计算机内存大小的限制而无法得到结果,往往不能满足实际问题求解的需要。据此,我们提出“零误差计算“的构想,即采用近似计算获得准确结果,研究结合兼具数值计算高效性和符号计算准确性的零误差数值计算高效算法.

特别地,对代数数的计算问题,我们提出了可充分保证计算结果无误差的浮点计算方法,在目前掌握的文献中,该方法计算量最小。

同态加密

同态加密是一种新型加密方案, 它可保证对密文进行直接运算解密的结果与对明文进行等价运算所得到的结果相同。

同态加密可以从根本上解决将计算委托给第三方时的保密问题,可满足传统加密方案所保障的通信安全和存储安全外的云端的运算安全。此外,它有望抵御量子攻击,是目前信息安全的前沿领域。

因式分解

随着信息技术的飞速发展,许多基于因式分解技术的密码方法应运而生。多项式分解问题作为代数运算理论和应用中的基本问题,同时它是一个符号计算在计算机代数领域成功应用的典范。在Maple以及Mathematica等相关数学软件中,因式分解已经作为一个标准功能被应用,但随着研究的深入,我们发现针对很多复杂案例的因式分解在理论以及算法的研究尚处于不完善阶段。

主要包含的研究方向有:多元数值因式分解理论研究、二元因式分解数值求解问题。

[1] 杨文强,吴文渊,刘江,陈经纬.一种基于三边定位的自动闸机控制方法.中国专利, 2016.专利号: ZL2014 10447404.5.

[2] 李轶,杨文强,李传璨,朱广,吴文渊,冯勇. 一类有界闭连通域上的循环程序终止性判断方法. 专利:中国, 2015. 申请号:201510181105.6.

[3] 李轶,朱广,杨文强. 一种用于符号线性系统的快速高斯约当消去方法. 专利:中国, 2015. 申请号:201510362146.5.

[4] 陈长波,李文康,杨文强. 一种保留模型特征的 3D 打印自适应切片方法. 专利:中国, 2015. 申请号:201510108708.3.

[5] 陈长波,李文康,吴文渊,杨文强. 一种用于 3D 打印中 CLI 文件错误检查的方法. 专利:中国, 2015. 申请号:201510181569.7.

查看更多
地址:重庆市北碚区方正大道266号615室
邮编:400714
联系方式:
邮箱:zidongtuili@cigit.ac.cn