CktFormalizer：将自然语言自动形式化为电路表示

针对大语言模型生成的 Verilog 代码常存在位宽不匹配等隐蔽错误的问题，本文提出 CktFormalizer 框架。该框架将生成过程重定向至嵌入 Lean 4 的依赖类型硬件描述语言中，利用其作为类型检查器、正确性防火墙和证明助手，将硬件缺陷转化为编译时错误并指导迭代修复。实验表明，该方法在保证仿真通过率的同时，显著提升了后端综合与布局布线的可实现性，并通过形式化验证支持闭环优化。