CktFormalizer: Autoformalization of Natural Language into Circuit Representations
إن CktFormalizer هو إطار عمل يستفيد من لغة وصف العتاد (HDL) ذات النوع التابع في لغة Lean 4 لتوجيه النماذج اللغوية الكبيرة (LLMs) نحو توليد أوصاف للعتاد مضمونة من حيث الصحة النحوية، وخالية من العيوب التي تكسر عملية التصنيع (synthesis)، ومحققة للتحقق الوظيفي من خلال براهين مدققة آلياً، مما يحقق قابلية تنفيذ تقترب من المثالية في الواجهة الخلفية ويسمح بالتحسين الآمن والآمن لمقاييس الأداء واستهلاك الطاقة والمساحة (PPA).