論文の概要: Correct-by-Construction G-Code Generation: A Neuro-Symbolic Approach via Separation Logic
- arxiv url: http://arxiv.org/abs/2605.10568v3
- Date: Wed, 20 May 2026 02:04:30 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-05-21 14:55:43.998741
- Title: Correct-by-Construction G-Code Generation: A Neuro-Symbolic Approach via Separation Logic
- Title(参考訳): 正しい構成Gコード生成:分離論理によるニューロシンボリックアプローチ
- Authors: Yeonseok Lee,
- Abstract要約: 本稿では,GLLM法の神経生成能力を分離論理証明器による形式的検証と統合することを目的とした,G符号生成のためのニューラルシンボリックフレームワークを提案する。
最終的にこの研究は、人間の監督の必要性を減らし、より安全で確実な自動製造を実現する自己修正システムを開発することを目指している。
- 参考スコア(独自算出の注目度): 0.0
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: This paper proposes a neuro-symbolic framework for G-code generation that seeks to integrate the neural generative capabilities of the GLLM method (Abdelaal et al., 2025) with formal verification via a Separation Logic (SL) prover. To establish a reliable physical baseline, the framework extracts deterministic boundary representations from 3D CAD models (STEP files) using the OpenCASCADE framework. This extracted geometric data supports a two-component architecture: the LLM serves as an initial code generator, while the SL Prover, utilizing a Spatial Heap model, evaluates the output. By conceptualizing physical collisions as logical Spatial Data Races -- violations of the separating conjunction in SL -- our framework translates proof failures into structured mathematical feedback. These failures are condensed into bounding boxes that serve as directives for the LLM's iterative self-correction. Ultimately, this work aims to develop a self-correcting system that reduces the need for human supervision, leading to safer and verified autonomous manufacturing.
- Abstract(参考訳): 本稿では,GLLM法(Abdelaal et al , 2025)の神経生成能力と分離論理(SL)証明器による形式的検証を統合することを目的とした,G符号生成のためのニューロシンボリックフレームワークを提案する。
信頼性の高い物理ベースラインを確立するために,OpenCASCADEフレームワークを用いて3次元CADモデル(STEPファイル)から決定論的境界表現を抽出する。
LLMは初期コードジェネレータとして機能し、SL Proverは空間ヒープモデルを利用して出力を評価する。
物理的衝突を論理的空間データレースとして概念化し、SLの分離接続に違反することで、我々のフレームワークは証明失敗を構造化された数学的フィードバックに変換する。
これらの故障は LLM の反復自己補正の指示となる有界箱に凝縮される。
最終的にこの研究は、人間の監督の必要性を減らし、より安全で確実な自動製造を実現する自己修正システムを開発することを目指している。
関連論文リスト
- 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) - 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) - 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) - Unsupervised Controllable Generation with Self-Training [90.04287577605723]
GANによる制御可能な世代は依然として困難な研究課題である。
本稿では,自己学習を通じてジェネレータを制御する潜伏符号の分布を学習するための教師なしフレームワークを提案する。
我々のフレームワークは、変分オートエンコーダのような他の変種と比較して、より良い絡み合いを示す。
論文 参考訳(メタデータ) (2020-07-17T21:50:35Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。