摘要
针对现有神经符号方法在竞赛数学表现优异但缺乏现实实现验证能力的问题，本文提出 s2n-bignum-bench 基准。该基准基于 AWS 工业级加密库 s2n-bignum，利用其已在 HOL Light 中验证的汇编例程，要求大语言模型根据形式化规范生成可被证明检查器接受的证明脚本。这是首个专注于工业级底层加密汇编机器可检验证明合成的公开基准，为评估超越竞赛数学的定理证明能力提供了极具挑战性的测试床。
AI 推荐理由
论文核心评估 LLM 在工业级底层代码上的形式化证明与逻辑推理能力，属推理研究。
研究机构
技术研究所，史蒂文斯理工学院
亚马逊网络服务，西雅图
论文信息