arXiv · quant-ph· Maor Ben Shahar, Jonathan Morag, Dirk Englund, Kfir Sulimany·· 12 小时前
Lean 中形式化量子密码学安全定理并用 LLM 降低 BB84 有限码长惩罚
Quantum Cryptography and Autoformalization in Lean
arXiv:2610.17286v1阅读论文 PDF ↗
仅依据论文摘要整理；未读取全文，实验条件、证明与基准细节请核对原文。
作者：Maor Ben Shahar, Jonathan Morag, Dirk Englund, Kfir Sulimany
研究任务与主要进展
作者在 Lean 中形式化了纠缠基 qubit BB84 协议的可组合安全定理，并用 LLM 自动形式化流程降低有限码长对密钥率的惩罚。基于论文摘要，该证明覆盖相干攻击、后选择技术及局部操作与经典通信约束，但未提供具体密钥率数值或传统基线对比。
阶段、条件与复现 · 深读核对
- AI 解决哪一个明确的量子问题？
- 训练数据、物理约束、误差与分布外检验是什么？
- 相同精度和总资源下，是否优于已有方法？
这些是阅读核对问题；材料未说明的条件保留未知。请结合上方论文版本、资料范围与原文核验。
来源：arXiv · quant-ph · arxiv.org