-
數理科學組-原子與分子科學研究所
1. 雷射基本操作以及實驗室維護。
2. 光學儀器,真空系統, 及電子電路的維護或操作。
3. 產生超冷原子至量子簡併態,研究等效規範場及相關的超流體現象。
2. 光學儀器,真空系統, 及電子電路的維護或操作。
3. 產生超冷原子至量子簡併態,研究等效規範場及相關的超流體現象。
-
林育如老師實驗室
-
截止:2024-12-31
-
數理科學組-資訊科學研究所
從事 形式化驗證(formal verification)在
1. 量子軟體系統
2. 儲存系統
的相關研究。
形式化驗證是一個開發高品質軟體的方法。
這方法會要求使用者提供他程式碼的"規格"。一個常見的方式,是用前置-後置條件來描述此規格,對一個排序的程式而言,我們會要求其前置條件是"輸入為一個整數序列",而其後置條件為"回傳值回輸入序列經過由小到大重新排列的結果"。當然,是用電腦能看懂的語言表示。
之後,形式化驗證會用嚴謹的數學方法和電腦工具,"證明"一個該程式是否滿足該規格。這方法已經被很多歐美頂尖企業採用,例如微軟使用它來檢驗協力廠商所撰寫的驅動程式,AWS也大量採用他來驗證其雲端系統。AWS的CTO甚至在AWS 2020的開發者會議上,花了他整個演講1/3的時間,來解釋AWS如何用形式化驗證提高其服務品質。
本實驗室從事形式化驗證已經研究已經有十多年的時間,在全世界同行中也有相當的知名度。目前我們研究主軸在兩個方向:
[量子軟體系統驗證]
隨著量子電腦硬體的逐漸成熟,對應的量子軟體開發技術也日益受到重視。可以預見的,軟體的規模會不斷地增加,確保設計出來的程式正確無誤的難度也會高速提升。這現象在傳統軟體已經很普遍,任何有一定規模的軟體程式,無可避免的都會有大大小小的錯誤,最後只能和這些錯誤共存。我們相信如果沒有引入新的技術,很快量子軟體也會走向這條路。
形式化驗證在量子程式的發展也已經有十數年。目前主流的技術有兩大缺點,基於霍爾邏輯的技術有強大的能力,能處理十分複雜的量子程式分析,但是他的使用需要大量人力介入,需要的工作量常常是寫程式本身的數倍。這樣的技術比較適合用在確保關鍵系統的品質上(如核電廠的控制程式)。基於抽象解釋的技術則是另一個極端。他是全自動的,但是有著常常誤報程式錯誤的缺點。這大大減低的該類工具的可用性。
最近中研院的團隊開發了一個基於樹自動機(tree automata)的全新量子電路驗證技術。他克服了上述兩個問題。這是一個全自動的技術,使用者只需要提供電路和預期的答案,該技術就能自動檢查,對所有允許的起始量子狀態,有沒有任何的可能,在執行完電路後產生和預期不同的結果。同時這樣技術是精確的,他完全不會誤報錯誤,大大的增加了可用性。
有關於這個方向,還可以參考Quantum Computer Systems: Research for Noisy Intermediate-Scale Quantum Computers一書 的Ch 5,6,9來得到大概輪廓(連結:https://www.morganclaypool.com/doi/abs/10.2200/S01014ED1V01Y202005CAC051)。
下面是一些和我們近期研究題目相關的參考文獻:
[1] Yuan-Hung Tsai, Jie-Hong R. Jiang, Chiao-Shan Jhang: Bit-Slicing the Hilbert Space: Scaling Up Accurate Quantum Circuit Simulation. DAC 2021: 439-444
[2] Parosh Aziz Abdulla, Bengt Jonsson, Pritha Mahata, Julien d'Orso: Regular Tree Model Checking. CAV 2002: 555-568
[3]https://zxcalculus.com
[4]Miller, D. Michael, and Mitchell A. Thornton. "QMDD: A decision diagram structure for reversible and quantum circuits." 36th International Symposium on Multiple-Valued Logic (ISMVL'06). IEEE, 2006.
[5]Mingsheng Ying. 2012. Floyd--hoare logic for quantum programs. ACM Trans. Programming Language System
[儲存系統驗證]
可參考我們發表在OSDI的論文:
[1] Yun-Sheng Chang, Yao Hsiao, Tzu-Chi Lin, Che-Wei Tsao, Chun-Feng Wu, Yuan-Hao Chang, Hsiang-Shang Ko, Yu-Fang Chen:
Determinizing Crash Behavior with a Verified Snapshot-Consistent Flash Translation Layer. OSDI 2020: 81-97
和下面相關文獻:
[2] Abdulla, P.A., Haziza, F., Holík, L. et al. An integrated specification and verification technique for highly concurrent data structures. Int J Softw. Tools. Technol. Transfer. 19, 549–563 (2017).
[3] Luke Nelson, James Bornholt, Ronghui Gu, Andrew Baumann, Emina Torlak, Xi Wang:
Scaling symbolic evaluation for automated verification of systems code with Serval. SOSP 2019: 225-242
[4] Frama-c WP tutorial (https://allan-blanchard.fr/publis/frama-c-wp-tutorial-en.pdf)
[5] Tej Chajed, Joseph Tassarotti, M. Frans Kaashoek, Nickolai Zeldovich:
Verifying concurrent, crash-safe systems with Perennial. SOSP 2019: 243-258
1. 量子軟體系統
2. 儲存系統
的相關研究。
形式化驗證是一個開發高品質軟體的方法。
這方法會要求使用者提供他程式碼的"規格"。一個常見的方式,是用前置-後置條件來描述此規格,對一個排序的程式而言,我們會要求其前置條件是"輸入為一個整數序列",而其後置條件為"回傳值回輸入序列經過由小到大重新排列的結果"。當然,是用電腦能看懂的語言表示。
之後,形式化驗證會用嚴謹的數學方法和電腦工具,"證明"一個該程式是否滿足該規格。這方法已經被很多歐美頂尖企業採用,例如微軟使用它來檢驗協力廠商所撰寫的驅動程式,AWS也大量採用他來驗證其雲端系統。AWS的CTO甚至在AWS 2020的開發者會議上,花了他整個演講1/3的時間,來解釋AWS如何用形式化驗證提高其服務品質。
本實驗室從事形式化驗證已經研究已經有十多年的時間,在全世界同行中也有相當的知名度。目前我們研究主軸在兩個方向:
[量子軟體系統驗證]
隨著量子電腦硬體的逐漸成熟,對應的量子軟體開發技術也日益受到重視。可以預見的,軟體的規模會不斷地增加,確保設計出來的程式正確無誤的難度也會高速提升。這現象在傳統軟體已經很普遍,任何有一定規模的軟體程式,無可避免的都會有大大小小的錯誤,最後只能和這些錯誤共存。我們相信如果沒有引入新的技術,很快量子軟體也會走向這條路。
形式化驗證在量子程式的發展也已經有十數年。目前主流的技術有兩大缺點,基於霍爾邏輯的技術有強大的能力,能處理十分複雜的量子程式分析,但是他的使用需要大量人力介入,需要的工作量常常是寫程式本身的數倍。這樣的技術比較適合用在確保關鍵系統的品質上(如核電廠的控制程式)。基於抽象解釋的技術則是另一個極端。他是全自動的,但是有著常常誤報程式錯誤的缺點。這大大減低的該類工具的可用性。
最近中研院的團隊開發了一個基於樹自動機(tree automata)的全新量子電路驗證技術。他克服了上述兩個問題。這是一個全自動的技術,使用者只需要提供電路和預期的答案,該技術就能自動檢查,對所有允許的起始量子狀態,有沒有任何的可能,在執行完電路後產生和預期不同的結果。同時這樣技術是精確的,他完全不會誤報錯誤,大大的增加了可用性。
有關於這個方向,還可以參考Quantum Computer Systems: Research for Noisy Intermediate-Scale Quantum Computers一書 的Ch 5,6,9來得到大概輪廓(連結:https://www.morganclaypool.com/doi/abs/10.2200/S01014ED1V01Y202005CAC051)。
下面是一些和我們近期研究題目相關的參考文獻:
[1] Yuan-Hung Tsai, Jie-Hong R. Jiang, Chiao-Shan Jhang: Bit-Slicing the Hilbert Space: Scaling Up Accurate Quantum Circuit Simulation. DAC 2021: 439-444
[2] Parosh Aziz Abdulla, Bengt Jonsson, Pritha Mahata, Julien d'Orso: Regular Tree Model Checking. CAV 2002: 555-568
[3]https://zxcalculus.com
[4]Miller, D. Michael, and Mitchell A. Thornton. "QMDD: A decision diagram structure for reversible and quantum circuits." 36th International Symposium on Multiple-Valued Logic (ISMVL'06). IEEE, 2006.
[5]Mingsheng Ying. 2012. Floyd--hoare logic for quantum programs. ACM Trans. Programming Language System
[儲存系統驗證]
可參考我們發表在OSDI的論文:
[1] Yun-Sheng Chang, Yao Hsiao, Tzu-Chi Lin, Che-Wei Tsao, Chun-Feng Wu, Yuan-Hao Chang, Hsiang-Shang Ko, Yu-Fang Chen:
Determinizing Crash Behavior with a Verified Snapshot-Consistent Flash Translation Layer. OSDI 2020: 81-97
和下面相關文獻:
[2] Abdulla, P.A., Haziza, F., Holík, L. et al. An integrated specification and verification technique for highly concurrent data structures. Int J Softw. Tools. Technol. Transfer. 19, 549–563 (2017).
[3] Luke Nelson, James Bornholt, Ronghui Gu, Andrew Baumann, Emina Torlak, Xi Wang:
Scaling symbolic evaluation for automated verification of systems code with Serval. SOSP 2019: 225-242
[4] Frama-c WP tutorial (https://allan-blanchard.fr/publis/frama-c-wp-tutorial-en.pdf)
[5] Tej Chajed, Joseph Tassarotti, M. Frans Kaashoek, Nickolai Zeldovich:
Verifying concurrent, crash-safe systems with Perennial. SOSP 2019: 243-258
-
陳郁方老師研究室
-
截止:2025-12-15
-
數理科學組-資訊科技創新研究中心
從事深度學習於電腦視覺相關研究。詳細內容包含人臉辨識、動作識別、物體偵測和追蹤、基於生成模型(Diffusion model, GAN, etc)之圖片影片及3D生成和檢測等多模態生成式AI、視覺與語言之多模態模型、對抗樣本、或其他電腦視覺與人工智慧安全(AI Security)相關研究,視應徵者背景及能力而定。
-
人工智慧影像理解實驗室(AIIULab)
-
截止:2025-12-31
-
數理科學組-化學研究所
全球氣候變遷所帶來的氣候暖化已成為人類發展面臨的迫切挑戰。為了達成國際社會所訂定的2050年碳零排放共同目標,我們的研究團隊專注於生質催化裂解技術和鋰離子電池領域。生質裂解是一種將生物質轉化為碳氫化合物的技術,對於碳中和及能源轉型至關重要。同時,鋰離子電池做為現代電池技術的代表,對於儲能和電動車等領域具有巨大潛力。我們致力於透過創新研究和技術開發,推動這兩個領域的發展,為綠色能源和永續發展做出貢獻。
-
化學所
-
截止:2024-12-31
-
數理科學組-資訊科技創新研究中心
文書處理、耗材管理、信件收發、公文傳遞、協助庶務工作、臨時交辦事項
-
行政室
-
截止:2024-12-31
-
數理科學組-資訊科技創新研究中心
從事後量子密碼學相關研究。詳細內容包含密碼系統的軟體或硬體實作、分析與攻擊,視應徵者背景及能力而定。
-
周彤老師實驗室
-
截止:2024-12-31
-
數理科學組-資訊科技創新研究中心
從事後量子密碼學相關研究。詳細內容包含密碼系統的軟體或硬體實作、分析與攻擊,視應徵者背景及能力而定。
-
周彤老師實驗室
-
截止:2024-12-31
-
數理科學組-資訊科技創新研究中心
• 從事腦機介面或AR/VR/MR的相關研究。
• 提出假設,設計實驗,並進行數據收集。
• 分析電生理訊號(包括但不限於EEG、EMG、EOG、SSVEP、眼球追蹤器等)並彙總發現。
• 撰寫科學論文並發表成果。
• 與其他團隊成員合作,記錄和轉移開發的技術。
• Carry out research in the field of Brain-Computer Interfaces or AR/VR/MR.
• Formulate hypotheses, plan user studies, and carry out data collection.
• Analyze the collected bio-signals (include but not limited to EEG, EMG, EOG, SSVEP, eye-tracker.. ) and summarize the findings.
• Contribute to the design of innovative devices for collecting bio-signals and test them.
• Write scientific papers detailing findings for scientific conferences and journals.
• Cooperate with other team members and business groups on documenting and transferring the developed technologies.”
• 提出假設,設計實驗,並進行數據收集。
• 分析電生理訊號(包括但不限於EEG、EMG、EOG、SSVEP、眼球追蹤器等)並彙總發現。
• 撰寫科學論文並發表成果。
• 與其他團隊成員合作,記錄和轉移開發的技術。
• Carry out research in the field of Brain-Computer Interfaces or AR/VR/MR.
• Formulate hypotheses, plan user studies, and carry out data collection.
• Analyze the collected bio-signals (include but not limited to EEG, EMG, EOG, SSVEP, eye-tracker.. ) and summarize the findings.
• Contribute to the design of innovative devices for collecting bio-signals and test them.
• Write scientific papers detailing findings for scientific conferences and journals.
• Cooperate with other team members and business groups on documenting and transferring the developed technologies.”
-
資創中心王有德老師實驗室
-
截止:2024-12-31
-
數理科學組-資訊科技創新研究中心
1.資訊安全相關領域的實務及學術性研究
2.資訊安全相關系統開發與實作
3.計畫管理與研究報告論文撰寫
4.其他交辦事項
2.資訊安全相關系統開發與實作
3.計畫管理與研究報告論文撰寫
4.其他交辦事項
-
資創中心李育杰老師實驗室
-
截止:2024-12-31
-
生命科學組-生物醫學科學研究所
癌症免疫治療:
1.建立人類免疫系統小鼠
2.發展癌症疫苗與細胞免疫治療
基因治療:
1.研發腺相關病毒載體(AAV)大量生產
2.開發基因治療用的AAV載體
研究地點在--生醫所和國家生技研究園區,
研究內容以產品開發為導向,將接受初階商業課程訓練,未來有技轉和創業機會
1.建立人類免疫系統小鼠
2.發展癌症疫苗與細胞免疫治療
基因治療:
1.研發腺相關病毒載體(AAV)大量生產
2.開發基因治療用的AAV載體
研究地點在--生醫所和國家生技研究園區,
研究內容以產品開發為導向,將接受初階商業課程訓練,未來有技轉和創業機會
-
Dr.陶秘華實驗室
-
截止:2024-12-26
-
數理科學組-資訊科學研究所
處理實驗室行政事務、人事聘任手續、計畫管理、計畫經費安排、實驗室採購、出差手續、文件撰寫、老師行程安排、會議及國內外學者訪問行程安排與連繫、協助辦理會議與活動等相關事宜。
-
古倫維/鐘楷閔/黃瀚萱老師實驗室
-
截止:2024-12-31
-
數理科學組-資訊科學研究所
自然語言處理 (Natural Language Processing)
深度學習 (Deep Learning)
情感計算 (Sentiment Analysis/Affective Computing)
假新聞相關 (Fake News Intervention)
視覺與語言 (Vision and Language/Multi-modal)
可解釋性人工智慧 (XAI/Text Generation)
運動科技指導語 (Sport Tech)
文字探勘與人工智慧相關研究,程式撰寫與論文發表。
深度學習 (Deep Learning)
情感計算 (Sentiment Analysis/Affective Computing)
假新聞相關 (Fake News Intervention)
視覺與語言 (Vision and Language/Multi-modal)
可解釋性人工智慧 (XAI/Text Generation)
運動科技指導語 (Sport Tech)
文字探勘與人工智慧相關研究,程式撰寫與論文發表。
-
古倫維老師實驗室
-
截止:2024-12-31