行业大模型企业类型

 

（以下内容来自报告）

 

（一）科大国创：星云大模型机器人编程大模型

 

科大国创自主研发了星云大模型机器人编程大模型——国创星码编程助手。模型通过精心构建大规模通用代码语料库和形式验证领域的专用代码语料库，基于transformer架构对模型进行深度训练，使得模型具备了生成通用代码和形式规约的能力，为软件的生成和验证提供了强大的支持。为了进一步提升形式规约的生成能力，模型还采用了提示工程、上下文学习、小样本学习及思维链等关键技术，使得模型在理解开发者自然语言需求意图、生成准确形式规约方面有了显著提升，进一步增强了工具的实用性和准确性。同时，公司还自主研发了先进的程序验证器，它采用基于Hoare逻辑的演绎推理和自动定理证明技术，对模型生成的代码进行形式化验证。这一验证过程确保了程序的行为严格符合形式规约的描述，从而保证了通过验证的程序的正确性。

 

图9  星云大模型机器人编程大模型示意图

 

国创星码编程助手不仅能提供函数级代码补全、代码解释、代码优化、代码注释生成、单元测试生成、智能问答、智能修复等功能，还可以提供形式标注辅助生成功能，能够针对C语言等特定语言，实现从自然语言到形式化规约的自动生成，并通过形式验证，确保生成代码的高度可信。

 

1.高效智能补全代码信息

 

国创星码编程助手可以对代码进行全面解析，在随后代码编程中进行自动补全。上下文的代码质量越高、内容越丰富，补全的代码信息越准确。

 

2.精准修复漏洞优化代码

 

国创星码编程助手不仅可以根据使用者的需求和习惯，快速检查代码中的语法错误和逻辑错误，帮助开发者规范代码格式，还可以识别代码中的冗余和低效部分，并给出优化建议，提升代码的执行效率和可维护性。

 

3.清晰解释代码逻辑功能

 

当开发者需要处理别人的代码，或者在既有代码中进行延展开发时，可以通过国创星码编程助手快速理解和解释初始代码的逻辑和功能，降低理解成本，帮助开发者更好地理解和调试代码。

 

4.从自然语言到形式标注生成

 

结合形式化技术，国创星码编程助手可以将自然语言的需求描述转化为形式规约的标注，并使用科创星云形式验证工具对程序执行严格的形式验证，确保生成高度可信的代码。

 

5.人工智能问答专业编程技术

 

国创星码编程助手集成了智能问答功能，开发者可以随时随地以各种方式向编程助手进行编程技术对话咨询。

 

国创星码编程助手能带来显著的经济效益。一方面，通过提升软件开发的效率和质量，模型能够帮助企业降低开发成本，缩短开发周期，增强企业的竞争力。另一方面，模型的应用能够显著减少软件中的缺陷和错误，降低后期维护成本，提高软件的稳定性和可靠性。这将为企业节省大量的维护费用，确保软件系统的长期稳定运行，进一步提升企业的经济效益。最后，通过强化软件的安全性和可靠性，模型能够减少因软件故障引发的安全事故和经济损失，保障人民群众的生命财产安全。特别是对于航空航天、汽车电子、能源核电、轨道交通等安全攸关领域，模型将为高可信软件的开发提供坚实的安全保障。