論文の概要: Natural Synthesis: Outperforming Reactive Synthesis Tools with Large Reasoning Models
- arxiv url: http://arxiv.org/abs/2605.15131v1
- Date: Thu, 14 May 2026 17:39:58 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-05-15 21:45:34.989836
- Title: Natural Synthesis: Outperforming Reactive Synthesis Tools with Large Reasoning Models
- Title（参考訳）: 自然合成:大規模共振モデルによる反応合成ツールの性能向上
- Authors: Frederik Schmitt, Matthias Cosler, Niklas Metzger, Julian Siber, Vladimir Krsmanovic, Mohamed Ghanem, Bernd Finkbeiner,
- Abstract要約: リアクティブ合成は論理仕様からハードウェア回路を自動構築する問題である。
本稿では, モデルチェッカーと大規模推論モデルを結合した反応合成へのニューロシンボリックアプローチを提案する。
仕様面では、仕様タスクを時間論理から自然言語にシフトする自動形式化ステップを導入する。
- 参考スコア（独自算出の注目度）: 7.768952514701895
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Reactive synthesis, the problem of automatically constructing a hardware circuit from a logical specification, is a long-standing challenge in formal verification. It is elusive for two reasons: It is algorithmically hard, and writing formal specifications by hand is notoriously difficult. In this paper, we tackle both sides of the problem. For the algorithmic side, we present a neuro-symbolic approach to reactive synthesis that couples large reasoning models with model checkers to iteratively repair a synthesized Verilog implementation via sound symbolic feedback. Our approach solves more benchmarks than the best dedicated tools in the annual synthesis competition and extends to constructing parameterized systems, a problem known to be undecidable. On the specification side, we introduce an autoformalization step that shifts the specification task from temporal logic to natural language by introducing a hand-authored dataset of natural-language specifications for evaluation. We demonstrate performance comparable to that of starting from formal specifications, establishing natural synthesis as a viable end-to-end workflow.
- Abstract（参考訳）: 論理的仕様からハードウェア回路を自動構築するという問題であるリアクティブ合成は、形式的検証において長年の課題である。
アルゴリズム的に困難であり、手作業で正式な仕様を書くことは、非常に難しい。
本稿では,この問題の両側面に対処する。
本稿では, モデルチェッカーと大きな推論モデルを結合させて, 音のシンボリックフィードバックによって合成されたVerilogの実装を反復的に修復する, 反応合成に対するニューロシンボリックアプローチを提案する。
提案手法は, 年次合成競争における最高の専用ツールよりも多くのベンチマークを解決し, パラメータ化システムの構築に拡張する。
仕様面では、仕様タスクを時相論理から自然言語にシフトする自動形式化ステップを導入し、評価のための自然言語仕様のハンドオーサリングデータセットを導入する。
我々は、形式的な仕様から始まり、自然な合成を実行可能なエンドツーエンドワークフローとして確立するパフォーマンスを実証する。
関連論文リスト
- MathAgent: Adversarial Evolution of Constraint Graphs for Mathematical Reasoning Data Synthesis [26.328617109421327]
本稿では、教師なし最適化問題としてデータ合成を定式化する階層型フレームワークを提案する。
立法者は、問題の制約をコードする構造化された世代図を逆向きに進化させ、執行者はこれらの仕様をさまざまな自然言語シナリオにインスタンス化する。
Qwen, Llama, Mistral, Gemmaの各シリーズの合計10モデルを用いて行った実験により, 本手法が顕著な結果が得られることを示した。
論文 参考訳（メタデータ） (2026-04-13T08:48:12Z) - CircuitSynth: Reliable Synthetic Data Generation [44.80087038178069]
大規模言語モデル(LLM)は、しばしば幻覚、論理的不整合、構造化された生成をタスクする場合のモード崩壊に悩まされる。
既存のアプローチ、例えば、プロンプトや検索強化ジェネレーションは、言語表現性と、妥当性とカバレッジに関する正式な保証のバランスをとるメカニズムを欠いている。
サーキットシンス(Circuit Synth)は,表面実現から意味論的推論を分離する新しいニューロシンボリックフレームワークである。
論文 参考訳（メタデータ） (2026-04-11T09:18:52Z) - Autoformalizer with Tool Feedback [52.334957386319864]
自動形式化は、数学的問題を自然言語から形式的ステートメントに変換することによって、ATP(Automated Theorem Proving)のデータ不足に対処する。
既存のフォーミュラライザは、構文的妥当性とセマンティック一貫性を満たす有効なステートメントを一貫して生成することに苦慮している。
本稿では,ツールフィードバックを用いたオートフォーマライザ (ATF) を提案する。
論文 参考訳（メタデータ） (2025-10-08T10:25:12Z) - Controlled Agentic Planning & Reasoning for Mechanism Synthesis [18.8323743697237]
本研究は、自動平面機構合成のための二重エージェントアクラムに基づく推論フレームワークを提案する。
自然言語によるタスク記述から、システムはシンボリック制約と方程式を構成し、シミュレーションコードを生成し、パラメタライズし、批判駆動のフィードバックを通じて設計を反復的に洗練する。
論文 参考訳（メタデータ） (2025-05-23T08:16:32Z) - RV-Syn: Rational and Verifiable Mathematical Reasoning Data Synthesis based on Structured Function Library [58.404895570822184]
RV-Synは、新しい数学的合成手法である。
このライブラリからPython形式の関数を組み合わせることで、グラフをソリューションとして生成する。
構築したグラフに基づいて,解誘導論理認識問題生成を実現する。
論文 参考訳（メタデータ） (2025-04-29T04:42:02Z) - The Role of Foundation Models in Neuro-Symbolic Learning and Reasoning [54.56905063752427]
Neuro-Symbolic AI(NeSy)は、AIシステムの安全なデプロイを保証することを約束している。
ニューラルネットワークとシンボリックコンポーネントを順次トレーニングする既存のパイプラインは、広範なラベリングを必要とする。
新しいアーキテクチャであるNeSyGPTは、生データから象徴的特徴を抽出する視覚言語基盤モデルを微調整する。
論文 参考訳（メタデータ） (2024-02-02T20:33:14Z) - ExeDec: Execution Decomposition for Compositional Generalization in Neural Program Synthesis [54.18659323181771]
プログラム合成において望ましいいくつかの異なる構成一般化形式を特徴付ける。
本稿では,ExeDecを提案する。ExeDecは,実行サブゴールを予測し,各ステップでプログラム実行によって段階的に通知される問題を解くための,新しい分解ベースの戦略である。
論文 参考訳（メタデータ） (2023-07-26T01:07:52Z) - Neural Circuit Synthesis from Specification Patterns [5.7923858184309385]
ハードウェア回路を高レベル論理仕様から直接合成するタスクにおいて階層変換器を訓練する。
機械学習を使った新しいアプローチは、この分野で多くの可能性を開くかもしれないが、十分な量のトレーニングデータが不足している。
この合成データに基づいて訓練された階層変換器は,合成競合による問題の大部分を解消することを示す。
論文 参考訳（メタデータ） (2021-07-25T18:17:33Z) - CounterExample Guided Neural Synthesis [12.742347465894586]
プログラム合成は困難であり、形式的な保証を提供する方法はスケーラビリティの問題に悩まされる。
ニューラルネットワークとフォーマルな推論を組み合わせることで、論理的な仕様をニューラルネットワークを正しい解へと導く一連の例に変換する。
この結果から,形式的推論に基づくガイダンスにより,ニューラルネットワークの性能が大幅に向上することが示唆された。
論文 参考訳（メタデータ） (2020-01-25T01:11:53Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。