行業大模型企業類型

 

（以下內容來自報告）

 

（一）科大國創：星云大模型星空機器人編程大模型

 

科大國創自主研發了星云大模型星空機器人編程大模型——國創星碼編程助手。模型通過精心構建大規模通用代碼語料庫和形式驗證領域的專用代碼語料庫，基于transformer架構對模型進行深度訓練，使得模型具備了生成通用代碼和形式規約的能力，為軟件的生成和驗證提供了強大的支持。為了進一步提升形式規約的生成能力，模型還采用了提示工程、上下文學習、小樣本學習及思維鏈等關鍵技術，使得模型在理解開發者自然語言需求意圖、生成準確形式規約方面有了顯著提升，進一步增強了工具的實用性和準確性。同時，公司還自主研發了先進的程序驗證器，它采用基于Hoare邏輯的演繹推理和自動定理證明技術，對模型生成的代碼進行形式化驗證。這一驗證過程確保了程序的行為嚴格符合形式規約的描述，從而保證了通過驗證的程序的正確性。

 

圖9  星云大模型星空機器人編程大模型示意圖

 

國創星碼編程助手不僅能提供函數級代碼補全、代碼解釋、代碼優化、代碼注釋生成、單元測試生成、智能問答、智能修復等功能，還可以提供形式標注輔助生成功能，能夠針對C語言等特定語言，實現從自然語言到形式化規約的自動生成，并通過形式驗證，確保生成代碼的高度可信。

 

1.高效智能補全代碼信息

 

國創星碼編程助手可以對代碼進行全面解析，在隨后代碼編程中進行自動補全。上下文的代碼質量越高、內容越豐富，補全的代碼信息越準確。

 

2.精準修復漏洞優化代碼

 

國創星碼編程助手不僅可以根據使用者的需求和習慣，快速檢查代碼中的語法錯誤和邏輯錯誤，幫助開發者規范代碼格式，還可以識別代碼中的冗余和低效部分，并給出優化建議，提升代碼的執行效率和可維護性。

 

3.清晰解釋代碼邏輯功能

 

當開發者需要處理別人的代碼，或者在既有代碼中進行延展開發時，可以通過國創星碼編程助手快速理解和解釋初始代碼的邏輯和功能，降低理解成本，幫助開發者更好地理解和調試代碼。

 

4.從自然語言到形式標注生成

 

結合形式化技術，國創星碼編程助手可以將自然語言的需求描述轉化為形式規約的標注，并使用科創星云形式驗證工具對程序執行嚴格的形式驗證，確保生成高度可信的代碼。

 

5.星空人工智能問答專業編程技術

 

國創星碼編程助手集成了智能問答功能，開發者可以隨時隨地以各種方式向編程助手進行編程技術對話咨詢。

 

國創星碼編程助手能帶來顯著的經濟效益。一方面，通過提升軟件開發的效率和質量，模型能夠幫助企業降低開發成本，縮短開發周期，增強企業的競爭力。另一方面，模型的應用能夠顯著減少軟件中的缺陷和錯誤，降低后期維護成本，提高軟件的穩定性和可靠性。這將為企業節省大量的維護費用，確保軟件系統的長期穩定運行，進一步提升企業的經濟效益。最后，通過強化軟件的安全性和可靠性，模型能夠減少因軟件故障引發的安全事故和經濟損失，保障人民群眾的生命財產安全。特別是對于航空航天、汽車電子、能源核電、軌道交通等安全攸關領域，模型將為高可信軟件的開發提供堅實的安全保障。