Lean 形式化 BB84 可组合安全证明并用 LLM 优化密钥率
热点事件持续更新
Lean 形式化 BB84 可组合安全证明并用 LLM 优化密钥率
1 篇报道1 个报道来源12 小时前更新
先了解这件事
AI 综述
Maor Ben Shahar、Jonathan Morag、Dirk Englund、Kfir Sulimany 在 arXiv 论文（arXiv:2610.17286）中称，他们在 Lean 中形式化了纠缠基 qubit BB84 协议的可组合安全证明，并用 LLM 自动形式化流程完成该证明。 作者称，证明完成后又将同一流程用作“发现机器”，降低了有限码长对密钥率的惩罚。该证明覆盖针对相干攻击的后选择技术并考虑有限块长。 以上基于论文摘要，未提供具体密钥率数值或与传统方法的基线对比。
AI 根据报道生成 · 7 小时前更新
最新进展10月14日 12:00
Lean 中形式化量子密码学安全定理并用 LLM 降低 BB84 有限码长惩罚报道时间线
沿着报道，了解事件的不同侧面。
10月14日
- arXiv · quant-phLean 中形式化量子密码学安全定理并用 LLM 降低 BB84 有限码长惩罚
作者在 Lean 中形式化了纠缠基 qubit BB84 协议的可组合安全定理，并用 LLM 自动形式化流程降低有限码长对密钥率的惩罚。基于论文摘要，该证明覆盖相干攻击、后选择技术及局部操作与经典通信约束，但未提供具体密钥率数值或传统基线对比。
本事件热度走势
- 可比范围当前
- 7
- 可比范围峰值
- 810月14日 18:00
- 近 24 小时变化
- –
02.557.510
18:0019:0020:0021:0022:0023:00
趋势仅比较持续完整观测到的相同主体，范围可能小于当前热度统计。移动指针或点击图表查看每小时热度；键盘可用左右方向键切换。