Harmonic 将在 REACH 2026 演讲：用 AI 定理证明器无幻觉合成硬件

satnam6502 · x · 2026-11-03

satnam6502 将于 11 月 10 日在伦敦 REACH 2026 会议发表演讲「Synthesizing Correct Hardware Without Hallucination」。脉络：自 1937 年香农证明布尔代数可描述开关电路以来，数学一直是数字设计的基础；形式化验证把这一思想推到极致——把电路需满足的性质写成定理，再对电路数学模型加以证明。障碍始终是成本：交互式证明需要定理证明与硬件设计的双重稀缺专长，模型检查器/等价性检查器等自动化工具在乘法器等算术电路上扩展性差。演讲将展示 Harmonic 基于 Lean 4 的 AI 定理证明器 Aristotle 如何大幅降低这一成本，实现无幻觉的正确硬件合成。