AI证明也能众包了！Choir开源协议让独立贡献者各用自己的LLM订阅，分布式形式化整本教科书！
Choir: An Open Protocol for Distributed Multi-Agent Autoformalization
📖 AI 总结
Choir 是一种面向分布式多智能体自动形式化的开放协议，旨在解决当前 AI 形式化工作高度集中化的问题。现有系统虽已能借助 Lean 等证明助手将整本教材和重要定理形式化，但通常由单一团队运行全部智能体并承担全部算力成本。Choir 将形式化项目拆解为可由独立贡献者完成的任务，每位参与者使用自己的智能体和 LLM 订阅，并完全通过项目的 GitHub 仓库进行协调。为支持开放参与，所有贡献在合并前均需通过确定性门控检查。该协议支持 Lean 4、Isabelle 和 Rocq，采用开源模块化设计，项目可替换单个组件或扩展协议。其意义在于将形式化工作从集中式模式转向开放协作模式，降低参与门槛与成本负担。
🔑 关键词速览
| Choir | 本文提出的一个开放协议，用于分布式多智能体自动形式化，通过GitHub仓库协调独立贡献者。 |
| Autoformalization | 自动将自然语言数学文本转化为形式化证明助手可验证的代码的过程。 |
| Lean 4 | 一种交互式定理证明器和编程语言，常用于形式化数学和验证软件正确性。 |
| Deterministic gate | 一种确定性的检查机制，在合并贡献前自动验证其正确性，确保开放参与下的质量。 |
| Distributed formalization | 将形式化项目分解为独立任务，由多个贡献者并行完成，而非集中式团队处理。 |
📱 每天一份 AI 前沿日报
关注公众号，每天 09:00 推送 · 不错过任何重磅