論文の概要: CktFormalizer: Autoformalization of Natural Language into Circuit Representations
- arxiv url: http://arxiv.org/abs/2605.07782v3
- Date: Tue, 12 May 2026 03:24:43 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-05-13 18:21:06.829379
- Title: CktFormalizer: Autoformalization of Natural Language into Circuit Representations
- Title（参考訳）: CktFormalizer: 自然言語の回路表現への自動変換
- Authors: Jing Xiong, Qi Han, Chenchen Ding, He Xiao, Zunhai Su, Chaofan Tao, Ngai Wong,
- Abstract要約: CktFormalizerは、Lean 4.0に組み込まれた依存型HDLを通じてハードウェア生成をリダイレクトするフレームワークである。
VerilogEval(156問題)、RTLLM(50問題)、ResBench(56問題)では、CktFormalizerは直接Verilog生成と競合するシミュレーションパスレートを達成する。
- 参考スコア（独自算出の注目度）: 23.44745731124114
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: LLMs can generate hardware descriptions from natural language specifications, but the resulting Verilog often contains width mismatches, combinational loops, and incomplete case logic that pass syntax checks yet fail in synthesis or silicon. We present CktFormalizer, a framework that redirects LLM-driven hardware generation through a dependently-typed HDL embedded in Lean 4. Lean serves three roles: (i) type checker:dependent types encode bit-width constraints, case coverage, and acyclicity, turning hardware defects into compile-time errors that guide iterative repair; (ii) correctness firewall:compiled designs are structurally free of defects that cause silent backend failures (the baseline loses 20% of correct designs during synthesis and routing; CktFormalizer preserves all of them); (iii) proof assistant:the agent constructs machine-checked equivalence proofs over arbitrary input sequences and parameterized widths, beyond the reach of bounded SMT-based checking. On VerilogEval (156 problems), RTLLM (50 problems), and ResBench (56 problems), CktFormalizer achieves simulation pass rates competitive with direct Verilog generation while delivering substantially higher backend realizability: 95--100% of compiled designs complete the full synthesis, place-and-route, DRC, and LVS flow. A closed-loop PPA optimization stage yields up to 35% area reduction and 30% power reduction through validated architecture exploration, with automated theorem proof ensuring that each optimized variant remains functionally equivalent to its formal specification.
- Abstract（参考訳）: LLMは自然言語仕様からハードウェア記述を生成することができるが、結果として生じるVerilogには、幅のミスマッチ、組み合わせループ、構文チェックをパスする不完全なケースロジックが含まれていることが多い。
CktFormalizerは、Lean 4.0に組み込まれた依存型HDLを通じてLCM駆動のハードウェア生成をリダイレクトするフレームワークである。
リーンは3つの役割を担います。
(i)型チェッカー:依存型は、ビット幅制約、ケースカバレッジ、非循環性をエンコードし、ハードウェア欠陥をコンパイル時のエラーに変換し、反復的な修復を誘導する。
(ii)正しさファイアウォール:コンパイルされた設計は、サイレントなバックエンド障害を引き起こす欠陥を構造的に含まない(ベースラインは、合成とルーティング中に正しい設計の20%を失う;CktFormalizerは、これらすべてを保存している)。
証明補助: エージェントは任意の入力シーケンスとパラメータ化された幅のマシンチェック等価性証明を, 境界付きSMTチェックの範囲を超えて構成する。
VerilogEval (156問題)、RTLLM (50問題)、ResBench (56問題)では、CktFormalizerは直接のVerilog生成と競合するシミュレーションパス率を実現し、より高いバックエンド実現性を実現している。
クローズドループのPPA最適化段階は、検証されたアーキテクチャ探索によって最大35%の面積削減と30%の電力削減をもたらす。
関連論文リスト
- Dynamic analysis enhances issue resolution [53.50448142467294]
DAIRA(Dynamic Analysis-enhanced Issue Resolution Agent)は、エージェントの推論サイクルに動的解析を組み込む自動修復フレームワークである。
テストトレース駆動の方法論によって駆動されるDAIRAは、軽量モニタを使用して重要なランタイムデータを抽出する。
Gemini 3 Flash Previewを使用すると、DAIRAは新たな最先端(SOTA)パフォーマンスを確立し、SWE-bench Verifiedデータセットで79.4%の解像度を達成する。
論文 参考訳（メタデータ） (2026-03-23T14:48:54Z) - SPARC: Scenario Planning and Reasoning for Automated C Unit Test Generation [1.0010193170880752]
本稿では,高レベルのプログラム意図とポインタ演算と手動メモリ管理の厳密な構文制約とのギャップを埋める,ニューロシンボリックなシナリオベースのフレームワークを提案する。
我々は、59の現実世界およびアルゴリズムの被験者で評価し、バニラプロンプト生成ベースラインを31.36%、分岐カバレッジ26.01%、突然変異スコア20.78%で上回り、シンボリック実行ツールKLEEに適合または超えている。
論文 参考訳（メタデータ） (2026-02-18T18:09:03Z) - ReLoop: Structured Modeling and Behavioral Verification for Reliable LLM-Based Optimization [6.572539312871392]
大規模言語モデル(LLM)は、自然言語を最適化コードに変換することができるが、サイレント障害は重大なリスクをもたらす。
2つの相補的な方向からサイレント障害に対処するReLoopを紹介します。
論文 参考訳（メタデータ） (2026-02-17T20:20:33Z) - Prism: Efficient Test-Time Scaling via Hierarchical Search and Self-Verification for Discrete Diffusion Language Models [96.0074341403456]
LLM推論を改善するための実用的な方法として、推論時計算が再導入されている。
テスト時間スケーリング(TTS)アルゴリズムの多くは、自動回帰デコーディングに依存している。
そこで我々は,dLLM のための効率的な TTS フレームワーク Prism を提案する。
論文 参考訳（メタデータ） (2026-02-02T09:14:51Z) - Scaling the Scaling Logic: Agentic Meta-Synthesis of Logic Reasoning [18.75349680577575]
SSLogicは、コントロール可能な困難を伴う継続的家族進化のためのフレームワークである。
SSLogicに進化したデータのトレーニングは、一致したステップでシードベースラインに対して一貫した利得を得る。
論文 参考訳（メタデータ） (2026-01-23T13:26:01Z) - BRIDGE: Building Representations In Domain Guided Program Verification [67.36686119518441]
BRIDGEは、検証をコード、仕様、証明の3つの相互接続ドメインに分解する。
提案手法は, 標準誤差フィードバック法よりも精度と効率を著しく向上することを示す。
論文 参考訳（メタデータ） (2025-11-26T06:39:19Z) - Unlocking Symbol-Level Precoding Efficiency Through Tensor Equivariant Neural Network [84.22115118596741]
シンボルレベルのプリコーディングにおいて,推論の複雑さの低いエンドツーエンドディープラーニング(DL)フレームワークを提案する。
提案手法は,従来の手法よりも約80倍の高速化を実現しつつ,SLPの大幅な性能向上を達成できることを示す。
論文 参考訳（メタデータ） (2025-10-02T15:15:50Z) - SymRTLO: Enhancing RTL Code Optimization with LLMs and Neuron-Inspired Symbolic Reasoning [30.938876549335067]
本稿では,新しいニューロン-シンボリックRTL最適化フレームワークであるSymRTLOを提案する。
有限状態機械(FSM)論理の解析と最適化のための記号モジュールを提案する。
Synopsys Design Compiler と Yosys による RTL-Rewriter ベンチマークの実験では、SymRTLO は 43.9% と 62.5% と 51.1% に向上している。
論文 参考訳（メタデータ） (2025-04-14T16:15:55Z) - COrAL: Order-Agnostic Language Modeling for Efficient Iterative Refinement [80.18490952057125]
反復改良は、複雑なタスクにおける大規模言語モデル(LLM)の能力を高める効果的なパラダイムとして登場した。
我々はこれらの課題を克服するために、コンテキストワイズ順序非依存言語モデリング(COrAL)を提案する。
当社のアプローチでは、管理可能なコンテキストウィンドウ内で複数のトークン依存関係をモデル化しています。
論文 参考訳（メタデータ） (2024-10-12T23:56:19Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。