Better Codes – and how they can be worse if you're not careful
12 hours ago
- better.codes旨在通过解决里德-所罗门码的两个重大挑战来机械化邻近奖：MCA（相互关联一致）挑战和列表解码挑战，这些挑战影响基于哈希的SNARKs中的证明规模和可靠性。
- 该系统以合理的安全界限启动，进展包括引用better.codes的理论结果；人工智能和研究人员此后将可证明的可靠性界限提高了数个比特。
- 这些挑战涉及找到邻近参数，使得诸如随机线性组合下的距离保持和有界列表大小等性质成立；这些性质在Lean中形式化，以实现自动化研究。
- 人工智能最初遇到一个验证错误，由于字段定义的类型等价问题导致Lean中出现深度递归错误，导致一些人通过禁用重放来绕过安全检查，但后来他们调试并修复了根本原因，通过将字段大小显式作为参数传递。
- 该项目带来了突破，研究人员现在正在研究源自better.codes结果的新方法，但风险仍然存在，来自不完全的形式化或可利用的验证系统。