自動推理與認知研究中心成立于2012年3月,現有固定人員10人,其中院士1人,高級研究人員5人。中心瞄準自動推理和可信計算的發展前沿,開展零誤差計算及其在信息安全和先進制造設計中的創新性研究,以促進和推動數學和信息科學的學科交叉與發展。
研究方向一:符號數值混合計算(Symbolic-numeric Hybrid Computing)
數值計算采用有限精度浮點數近似計算,在工業和工程中廣泛使用,效率高但誤差累積造成精度有時過低,通常只能得到局部解。符號計算可以對帶符號的數學表達式精確操作,能準確得到問題的全部解但受制于中間過程膨脹效率相對較低。如何結合高效但有誤差的數值計算與精確但低效的符號計算獲得滿足目標精度的結果是符號數值混合計算的主要研究內容。
-
基于同倫算法和臨界點技術的的實代數簇連通分支樣本點計算(圖1)
-
高維空間的穩定曲線追蹤算法(圖1)
-
雙參數多項式系統的邊界曲線算法(圖2)
-
基于參數多項式系統求解的實同倫算法(圖2)
-
雙參數多項式動力系統的Fold-Hopf分叉邊界計算及在生物系統穩定性分析中的應用(圖2)
-
基于三角分解的實閉域一階理論的量詞消去算法(圖3)
-
含參程序的自動并行化(圖4)

圖1 實連通分支樣本點計算及曲線追蹤
圖2 含參多項式系統求解及應用
圖3 實量詞消去算法

圖4含參程序的自動并行化
研究方向二:零誤差計算(ERROR-FREE NUMERICal COMPUTATION)
數值計算方法不可避免地給計算結果帶來多種誤差,在航天航空、生物醫療等領域,計算誤差可能會帶來嚴重后果。符號計算可以得到問題精確地完備解,但是計算量大且表達式龐大,導致計算效率較低,或者受到計算機內存大小的限制而無法得到結果,往往不能滿足實際問題求解的需要。據此,我們提出“零誤差計算“的構想,即采用近似計算獲得準確結果,研究結合兼具數值計算高效性和符號計算準確性的零誤差數值計算高效算法. 特別地,對代數數的計算問題,我們提出了可充分保證計算結果無誤差的浮點計算方法,在目前掌握的文獻中,該方法計算量最小。相關成果在 ACM Communications in Computer Algebra、The 2014 International Workshop on Symbolic-Numeric Computation (2014年國際數學家大會衛星會議),第六屆全國計算機數學學術會議等期刊和會議上公開發表或報告。

不同于美國紐約大學學者倡導的無限精度EGC模型,我們提出了“零誤差計算”的概念。前期,已將有理數域上的零誤差計算理論推廣到了代數數域(一大類無理數),并從理論上保證中間計算過程采用有誤差的數值計算,最終可得到無誤差的結果(代數數GAP定理)。近期,在代數數恢復的誤差控制方面取得新突破。主要是在符號計算國際頂級會議ISSAC 2014關于廣義LLL格約化基最新結果的基礎上,結合代數數GAP定理和矩陣計算中QR分解的誤差估計方法,探明了計算過程中浮點位數的取值方法,可以充分保證計算結果的無誤差。截至目前,已完成零誤差計算關鍵算法 PSLQ 的數值穩定性分析(該算法曾被評為二十世紀十大算法之一)。據此,有望設計首個數值的PSLQ算法。
-
采用數值計算求解一類半代數系統全部整數解,國家自然科學基金,2017年1月——2020年12月
-
整數關系探測的誤差可控算法與應用,國家自然科學基金,2016年1月——2018年12月
-
零誤差計算理論與應用,中科院“一三五”專項,2014年6月——2016年12月
-
零誤差計算在歐幾里得格和密碼學中的應用,重慶市基礎與前沿研究計劃,2013年12月——2017年12月
研究方向三:因式分解(Factorization)
隨著信息技術的飛速發展,許多基于因式分解技術的密碼方法應運而生。多項式分解問題作為代數運算理論和應用中的基本問題,同時它是一個符號計算在計算機代數領域成功應用的典范。在Maple以及Mathematica等相關數學軟件中,因式分解已經作為一個標準功能被應用,但隨著研究的深入,我們發現針對很多復雜案例的因式分解在理論以及算法的研究尚處于不完善階段。

二元因式分解數值求解問題

成果發表在 SCI 期刊 Science China Mathematics 和 J. System Scienc & Compleixty 上。
研究方向四:同態加密及其應用(Homomorphic Encryption and Its Applications)
同態加密是一種新型加密方案, 它可保證對密文進行直接運算解密的結果與對明文進行等價運算所得到的結果相同。所以它可以從根本上解決將計算委托給第三方時的保密問題,可滿足傳統加密方案所保障的通信安全和存儲安全外的云端的運算安全。此外,它有望抵御量子攻擊,是目前信息安全的前沿領域。

中心從2013年開始對同態加密的研究工作,開發有若干基于同態加密的軟件應用。HEBinCalc是我們基于IBM的HElib開發的同態整數運算庫,該函數庫利用HElib提供的二進制與運算(AND)和異或運算(XOR),實現了在計算機上使用密文來進行不同進制下的加減乘除等算術運算的功能,可以靈活地選取數據位數,對大整數進行操作,加密數據可以進行存儲或網絡傳輸。運行庫可以移植到各種服務器、PC以及嵌入式平臺之上。目前該庫在core i7 CPU的PC機上,可以在2.1s內完成16位的整數加減法。在此基礎之上可以開發保密的數據通信及數據計算系統。
同態整數運算庫性能
Arithmetic | Circuit | #bits | m | #slots | Lc | time (s) |
Addition | RCA | 16 | 14351 | 504 | 17 | 2.16 |
| CLA | 16 | 7781 | 150 | 7 | 2.53 |
| CLA | 64 | 13981 | 600 | 13 | 37.69 |
Subtraction | RCS | 16 | 14351 | 504 | 17 | 2.17 |
| CLA | 16 | 7781 | 150 | 7 | 2.52 |
| CLA | 64 | 13981 | 600 | 13 | 37.16 |
Multiplication | RCA | 8 | 8191 | 630 | 9 | 4.62 |
| RCA | 16 | 14351 | 504 | 17 | 46.32 |
Division | RCA | 4 | 18631 | 720 | 21 | 14.63 |
另外,我們基于該整數運算庫,進一步開發了基于同態加密的電子投票系統演示平臺,該平臺利用同態加密技術進行選票的加密和計票過程,保證了投票過程的保密性,并利用時間戳和數字簽名技術保證選票的安全性。

研究方向五:程序正確性驗證(Verification of Program Correctness)
隨著計算機和互聯網的迅猛發展,以通信、存儲和計算為核心的信息基礎設施已經滲透到政治、經濟、軍事、文化以及社會的各個層面。軟件是信息基礎設施的靈魂,但它并不總是讓人信任,從而產生“軟件可信性”問題。面向應用的程序正確性驗證是可信軟件基礎研究的重要課題之一。其主要研究如何使用數學方法去證明給定程序是否符合預先設定的目標。研究內容包括:程序停機問題證明與不變式構造。
-
將Tiwari提出的線性循環程序的終止性問題等價歸約為兩類特殊程序的終止性問題,并建立了終止性判定的遞歸算法。
-
構造了線性程序不可終止點集合的實多面體吸引集。
-
建立了基于不動點理論的多項式循環程序終止性判定理論。
-
提出了L-depth Eventual 線性秩函數概念,證明了該函數與程序可終止性的內在關聯。
-
提出了微分不變式的新定義,豐富了不變式的表現形式。
圖1 線性程序多面體吸引集的半代數刻畫

圖2 L-depth Eventual 線性秩函數

聯系人:吳文淵 郵箱:zidongtuili@cigit.ac.cn 網址:http://www.arcnl.org/