買專利賣專利找龍圖騰，真高效！ 查專利查商標用IPTOP,全免費！專利年費監控用IP管家,真方便！

龍圖騰網恭喜南京航空航天大學申請的專利一種從函數式卷積表達式到C代碼的重寫轉換方法獲國家發明授權專利權，本發明授權專利權由國家知識產權局授予，授權公告號為：CN118170384B 。

龍圖騰網通過國家知識產權局官網在2025-03-21發布的發明授權授權公告中獲悉：該發明授權的專利申請號/專利號為：202410232651.7，技術領域涉及：G06F8/40；該發明授權一種從函數式卷積表達式到C代碼的重寫轉換方法是由張曉麗;陳鋼設計研發完成，并于2024-03-01向國家知識產權局提交的專利申請。

本一種從函數式卷積表達式到C代碼的重寫轉換方法在說明書摘要公布了：本發明提供了一種在Coq定理證明器中以函數式方式表達AI神經網絡算子的方法，實現了一種將函數式卷積表達式轉換為C代碼的重寫技術。主要包括六個關鍵部分，張量原語的形式化定義、中間變量綁定值的形式化定義、張量原語及中間變量綁定值的命令式組合子的形式化定義、張量原語及中間變量綁定值的重寫規則的形式化定義、函數式張量卷積表達式的定義，以及其他AI神經網絡算子如池化、激活等的表達式形式化定義。對于后續在Coq中進行神經網絡算子正確性驗證和優化提供了有力支持。有效規避了傳統深度學習框架中常見的形狀不匹配和不可靠性等問題。這為構建高可靠性的AI編譯器打下了堅實的基礎。

本發明授權一種從函數式卷積表達式到C代碼的重寫轉換方法在權利要求書中公布了：1.一種從函數式卷積表達式到C代碼的重寫轉換方法，其特征在于，具體包括以下步驟：1：在Coq定理證明器中定義一個從下標索引到元素值的張量原語；步驟1的實現具體為：使用了一個從下標索引到元素值的第一映射函數f:finn-expd，以構造張量原語mkvSeq，其中finn是從0到n-1的自然數，d是一個歸納定義的數據類型，exp是一個表達式類型；2：在Coq定理證明器中定義中間變量綁定值的操作；3：在Coq定理證明器中定義張量原語的中間命令式組合子、中間變量綁定值的中間命令式組合子；4：在Coq定理證明器中定義張量原語針對賦值函數A的重寫轉換規則、張量原語針對命令函數C的重寫轉換規則、中間變量綁定值針對函數A的重寫轉換規則和中間變量綁定值針對函數C的重寫轉換規則；步驟4的實現，具體包括：張量原語針對賦值函數A的重寫轉換規則，對于一個由第一映射函數f構造的張量，使用函數A將其賦給接收器a，等價于通過mkvSeql將函數A應用到每個第一映射函數f和接收器a上，其中函數A是一個賦值操作，用于將表達式賦值給接收器；張量原語針對命令函數C的重寫轉換規則，對于給定的張量構造第一映射函數f和命令映射函數c，在應用函數C時，等價地通過命令new引入一個臨時變量，并將mkvSeqf賦值給臨時變量，再將臨時變量的表達式值傳遞給命令映射函數c，其中函數C是一個表達式到命令的映射函數；中間變量綁定值針對函數A的重寫轉換規則：在中間變量綁定中，對于給定的表達式e和第一映射函數f，通過函數A將let_bindingef賦值給接收器a，等價于應用命令式組合子letl；中間變量綁定值針對函數C的重寫轉換規則：對于給定的表達式e，第一映射函數f和命令映射函數c，在應用函數C時，等價地通過命令new引入一個臨時變量，并將let_bindingef賦值給臨時變量，再將臨時變量的表達式值傳遞給命令映射函數c，其中函數C是一個表達式到命令的映射操作；5：在Coq定理證明器中定義函數式張量表達式的卷積操作，并利用步驟4中的重寫轉換規則將卷積操作轉換為相應的C語言卷積代碼；6：在Coq定理證明器中定義其他AI編譯器核心算子的函數式張量表達式，其他AI編譯器核心算子包括池化、激活、全連接。

如需購買、轉讓、實施、許可或投資類似專利技術，可聯系本專利的申請人或專利權人南京航空航天大學，其通訊地址為：213300 江蘇省常州市溧陽市濱河東路29號；或者聯系龍圖騰網官方客服，聯系龍圖騰網可撥打電話0551-65771310或微信搜索“龍圖騰網”。