論文の概要: Correct-by-Construction G-Code Generation: A Neuro-Symbolic Approach via Separation Logic

• arxiv url: http://arxiv.org/abs/2605.10568v1
• Date: Mon, 11 May 2026 13:38:51 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-05-12 23:28:50.854717
• Title: Correct-by-Construction G-Code Generation: A Neuro-Symbolic Approach via Separation Logic
• Title（参考訳）: 正しい構成Gコード生成:分離論理によるニューロシンボリックアプローチ
• Abstract要約: 本稿では,GLLMが創造的生成器として機能し,SL Proverが決定論的検証器として機能する2成分アーキテクチャを提案する。 このシナジーは自己修正生成サイクルを確立し、手動による監視の必要性を減らす。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: This paper proposes a neuro-symbolic framework for G-code generation by integrating the GLLM neural method (Abdelaal et al., 2025) with our established Separation Logic (SL) verifier. We introduce a two-component architecture where GLLM serves as a creative generator and the SL Prover, utilizing the Spatial Heap model, acts as a deterministic verifier. By defining physical collisions as logical Spatial Data Races - violations of the separating conjunction in SL - the framework translates proof failures into structured mathematical feedback. These failures are condensed into minimal bounding boxes that act as precise spatial directives for GLLM's iterative self-correction. This synergy establishes a self-correcting generative cycle that reduces the need for manual oversight, supporting the production of verified G-code to enhance safety in autonomous manufacturing.
• Abstract（参考訳）: 本稿では,GLLMニューラルメソッド(Abdelaal et al , 2025)を確立された分離論理(SL)検証器と統合することにより,G符号生成のためのニューロシンボリックフレームワークを提案する。 本稿では,GLLMが創造的生成器として機能し,SL Proverが空間ヒープモデルを利用して決定論的検証器として機能する2成分アーキテクチャを提案する。 物理的衝突を論理的空間データレース - SLにおける分離結合の違反 - として定義することで、このフレームワークは証明失敗を構造化された数学的フィードバックに変換する。 これらの故障は、GLLMの反復自己補正の正確な空間指示として機能する最小限の有界箱に凝縮される。 このシナジーは、手動監視の必要性を減らす自己補正生成サイクルを確立し、検証されたGコードの生成をサポートし、自律的な製造の安全性を高める。

関連論文リスト

• UniCoder: Unified Visual-to-Code Generation via Symbolic Rewards and Reference-Guided Code Optimization [22.627858794105066]
  2つの新しいメカニズムを統合する統一RLフレームワークであるUniCoderを紹介する。 まず,生成されたコードを個別の視覚属性に解析するために,軽量な補助LCMを用いたtextbfSymbolic Attribute Alignmentを提案する。 第二に、局所最適化から逃れるために、低パフォーマンスなロールアウトグループに地上軌道を動的に注入する戦略である textbfReference-Guided Code Optimization を考案した。
  論文  参考訳（メタデータ） (2026-06-30T14:29:48Z)
• Provably Secure Agent Guardrail [89.79561918065122]
  既存の防衛アーキテクチャは経験的セマンティックガードレールと確率論的大モデル調整器に依存している。 本稿では,論理的推論の基本的制約に基づくエージェントのための新しいセキュリティパラダイムを提案する。
  論文  参考訳（メタデータ） (2026-05-28T02:12:41Z)
• CasualSynth: Generating Structurally Sound Synthetic Data [44.80087038178069]
  大言語モデル(LLM)は、現実的な合成データを生成するが、その出力がターゲットドメインを管理する因果的メカニズムを尊重することを保証しない。 本稿では,意味的実現から因果構造の生成を分離するフレームワークCausal Synthを紹介し,因果的妥当性と言語学的にリッチな合成データを生成する。
  論文  参考訳（メタデータ） (2026-05-17T16:21:01Z)
• Separation Logic for Verifying Physical Collisions of CNC Programs [0.0]
  コンピュータ数値制御(CNC)の安全性検証は、伝統的に反復的なテスト要求の変更に依存してきた。 本稿では,物理シミュレーションを空間的,管理された論理力学モデルとして概念化する形式的検証フレームワークを概念化する。
  論文  参考訳（メタデータ） (2026-05-11T12:09:17Z)
• How LLMs Fail and Generalize in RTL Coding for Hardware Design? [56.361436215029045]
  我々は,認知理論に触発された問題解決性に基づく新しい誤り分類法を導入する。 我々の分類学は、障害を構文、意味、解決可能な機能、解決不可能な機能タイプに分類する。
  論文  参考訳（メタデータ） (2026-04-26T14:34:49Z)
• CodeCircuit: Toward Inferring LLM-Generated Code Correctness via Attribution Graphs [13.488544043942495]
  本研究の目的は、コード生成中に論理的妥当性を予測可能な内部デオード可能な信号が、モデル内のニューラルダイナミクスで符号化されているかどうかを検討することである。 複雑な残留流を分解することにより,音の推論と論理的失敗を区別する構造的シグネチャを同定することを目的とする。 Python、C++、Javaでの分析では、固有の正当性信号が多様な構文で堅牢であることが確認されている。
  論文  参考訳（メタデータ） (2026-02-06T03:49:15Z)
• SIGMA: Scalable Spectral Insights for LLM Collapse [51.863164847253366]
  SIGMA(Spectral Inequalities for Gram Matrix Analysis)は,モデル崩壊のための統一的なフレームワークである。 行列のスペクトル上の決定論的境界を導出するベンチマークを利用することで、SIGMAは表現空間の収縮を追跡するために数学的に基底化された計量を提供する。 我々は、SIGMAが状態への遷移を効果的に捉え、崩壊のメカニズムに関する理論的知見の両方を提供することを示した。
  論文  参考訳（メタデータ） (2026-01-06T19:47:11Z)
• The Trojan in the Vocabulary: Stealthy Sabotage of LLM Composition [31.827344197678126]
  トケナイザー移植はサプライチェーンの脆弱性を導入する。 係数再利用の幾何学を利用して、我々の攻撃は非対称的な実現可能性ギャップを生み出す。 実験的に、攻撃は訓練なしで、スペクトルの模倣を達成し、異常検出を回避する。
  論文  参考訳（メタデータ） (2025-12-31T19:00:03Z)
• Geometrically-Constrained Agent for Spatial Reasoning [53.93718394870856]
  視覚言語モデルは空間的推論において基本的な意味-幾何学的ギャップを示す。 現在のパラダイムは、このギャップを埋めることに失敗します。 本稿では,形式的タスク制約を導入することにより,このギャップを解消する学習自由エージェントパラダイムを提案する。
  論文  参考訳（メタデータ） (2025-11-27T17:50:37Z)
• LLM-Empowered Event-Chain Driven Code Generation for ADAS in SDV systems [24.318466695095026]
  本稿では、自然言語要求から検証済みの自動車コードを生成するためのイベントチェーン駆動LLM駆動ワークフローを提案する。 LLMの再トレーニングなしに、有効な信号利用と一貫したコード生成を実現しました。
  論文  参考訳（メタデータ） (2025-11-26T19:53:04Z)
• When LLMs Copy to Think: Uncovering Copy-Guided Attacks in Reasoning LLMs [30.532439965854767]
  大規模言語モデル(LLM)は、脆弱性検出やコード理解といったタスクを可能にする自動コード解析に不可欠なものになっている。 本稿では,CGA(Copy-Guided Attacks)と呼ばれる,新たなプロンプトベースの攻撃のクラスを特定し,検討する。 CGAは、コード解析タスクにおいて、無限ループ、早期終了、偽の拒絶、意味的歪みを確実に誘導することを示す。
  論文  参考訳（メタデータ） (2025-07-22T17:21:36Z)
• AutoLayout: Closed-Loop Layout Synthesis via Slow-Fast Collaborative Reasoning [102.71841660031065]
  Autoは、クローズドループの自己検証プロセスをデュアルシステムフレームワークに統合する、完全に自動化された方法である。 Autoの有効性は8つの異なるシナリオで検証され、SOTA法よりも10.1%改善された。
  論文  参考訳（メタデータ） (2025-07-06T08:35:22Z)
• Training Language Models to Generate Quality Code with Program Analysis Feedback [66.0854002147103]
  大規模言語モデル(LLM)によるコード生成は、ますます本番環境で採用されているが、コード品質の保証には失敗している。 実運用品質のコードを生成するためにLLMにインセンティブを与える強化学習フレームワークであるREALを提案する。
  論文  参考訳（メタデータ） (2025-05-28T17:57:47Z)
• Retrieval is Not Enough: Enhancing RAG Reasoning through Test-Time Critique and Optimization [58.390885294401066]
  Retrieval-augmented Generation (RAG) は知識基底型大規模言語モデル(LLM)を実現するためのパラダイムとして広く採用されている。 RAGパイプラインは、モデル推論が得られた証拠と整合性を維持するのに失敗することが多く、事実上の矛盾や否定的な結論につながる。 批判駆動アライメント(CDA)に基づく新しい反復的枠組みであるAlignRAGを提案する。 AlignRAG-autoは、動的に洗練を終了し、批判的な反復回数を事前に指定する必要がなくなる自律的な変種である。
  論文  参考訳（メタデータ） (2025-04-21T04:56:47Z)
• Self-Healing Machine Learning: A Framework for Autonomous Adaptation in Real-World Environments [50.310636905746975]
  実世界の機械学習システムは、基礎となるデータ生成プロセスの分散シフトによって、モデルの性能劣化に遭遇することが多い。 概念のドリフト適応のような既存のシフトへのアプローチは、その理性に依存しない性質によって制限される。 我々はこれらの制限を克服するために自己修復機械学習(SHML)を提案する。
  論文  参考訳（メタデータ） (2024-10-31T20:05:51Z)
• Fault-tolerant simulation of Lattice Gauge Theories with gauge covariant codes [0.0]
  量子誤り訂正と格子ゲージ理論(LGT)の間には、強くて簡単な接続が存在することを示す。 このゲージ共変符号上の論理演算を同定し、対応するハミルトニアンがこれらの論理演算の項で表現できることを示す。 積公式と量子化法の両方を用いて、ゲージ共変符号内でハミルトニアンのフォールトトレラント時間進化を行う方法を示す。
  論文  参考訳（メタデータ） (2024-05-29T17:21:29Z)
• Neuro-Symbolic Integration Brings Causal and Reliable Reasoning Proofs [95.07757789781213]
  LLMの複雑な推論には2行のアプローチが採用されている。 1行の作業は様々な推論構造を持つLLMを誘導し、構造出力は自然に中間推論ステップと見なすことができる。 他方の行では、LCMのない宣言的解法を用いて推論処理を行い、推論精度は向上するが、解法のブラックボックスの性質により解釈性に欠ける。 具体的には,Prologインタプリタが生成した中間検索ログにアクセスし,人間可読推論に解釈可能であることを示す。
  論文  参考訳（メタデータ） (2023-11-16T11:26:21Z)
• Disentanglement via Latent Quantization [60.37109712033694]
  本研究では,組織化された潜在空間からの符号化と復号化に向けた帰納的バイアスを構築する。 本稿では,基本データレコーダ (vanilla autoencoder) と潜時再構成 (InfoGAN) 生成モデルの両方に追加することで,このアプローチの広範な適用性を実証する。
  論文  参考訳（メタデータ） (2023-05-28T06:30:29Z)
• Unsupervised Controllable Generation with Self-Training [90.04287577605723]
  GANによる制御可能な世代は依然として困難な研究課題である。 本稿では,自己学習を通じてジェネレータを制御する潜伏符号の分布を学習するための教師なしフレームワークを提案する。 我々のフレームワークは、変分オートエンコーダのような他の変種と比較して、より良い絡み合いを示す。
  論文  参考訳（メタデータ） (2020-07-17T21:50:35Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。