2025年7月30-31日，CCF软件工程创新与青年发展论坛暨软件工程专委常委会议在CCF业务总部&学术交流中心成功召开。望安科技作为国内形式化方法和CC安全认证领域的头部企业，受邀参与此次盛会，与来自国内软件工程及相关领域的众多研究者和实践者共同探讨软件工程面临的难题与挑战。

本次论坛是CCF软件工程专委会青年论坛成立以来的首次全体活动，具有里程碑意义。论坛由CCF软件工程专委会主任、南京大学马晓星教授，CCF软件工程专委会副主任、复旦大学彭鑫教授担任主席。本次论坛汇聚了来自30家高校、科研院所与企业的60余位软件顶尖专家学者，为软件工程领域的学术交流与合作搭建了高端平台。

在论坛研讨环节，望安科技创始人、浙江大学教授赵永望围绕“软件工程难题与挑战”这一主题，代表CCF发布了AI时代下软件工程面临的一项重要难题——自动程序定理证明。自动程序定理证明作为形式化验证的核心技术，通过将软件需求转化为逻辑命题（如一阶谓词），驱动机器自动生成证明，为高可信软件提供了“数学显微镜级”的严格保障。然而，在AI时代背景下，ATP面临着证明规模大、检查时间长、技术门槛高等三重困境。针对这些问题，赵永望指出，AI/LLM（大型语言模型）具有破解这些困境的潜力。AI的生成能力与FM的严格、精密性具有互补潜力，AI可通过自动生成形式化证明、规约来降低FM的应用成本，而FM可提供严密验证框架来提高AI的可靠性 ，达到优势互补的作用，互相促进应用。

LLMs在自动定理证明方面目前也面临着问题：一是程序证明能力有待进一步提高，目前使用LLM在证明定理时的成功率还有待提升，尤其是在针对软件特征的证明方面；二是AI与形式化工具的集成性不足，LLM与定理证明工具（如Isabelle的Sledgehammer）的集成不够深入；三是AI证明能力的可解释性不足，缺乏对LLM证明能力影响因素的研究；四是对于AI证明能力的评估方法欠缺，目前的评估多停留在固定数据集，忽略了问题难度的差异。目前的LLMs主要集中在数学定理证明的学习上，对于程序证明特定的知识和技巧掌握不足，形象地说，现在的LLM就像一个高中或大学数学竞赛冠军，但对于程序/软件的定理证明却知之甚少。

在论坛现场，参会嘉宾围绕自动程序定理证明这一难题展开了热烈的研讨，大家积极交流观点，分享经验，共同为攻克这一难题出谋划策，为软件工程领域的创新发展贡献智慧和力量。此次论坛的成功举办，不仅为软件工程领域的专业人士提供了一个深入交流与合作的机会，也为推动软件工程技术创新和青年人才培养奠定了坚实基础，相信在各方的共同努力下，软件工程领域将迎来更加广阔的发展前景。望安科技也将持续关注行业动态，积极参与相关研究与实践，助力软件工程领域的高质量发展。

望安科技深耕形式化验证领域多年，通过技术创新和专业能力，成功将形式化验证技术及核心工具应用于国家重大项目，为航空航天、国防、轨道交通等关键领域构建了高可靠性的安全屏障。未来，望安科技将持续深化形式化验证技术的研究与实践，不断拓展形式化验证技术的应用范围，携手各界共同为推动信息技术生态系统的安全性和可靠性做出更大贡献。