Correct-by-Construction G-Code Generation: A Neuro-Symbolic Approach via Separation Logic

• URL: http://arxiv.org/abs/2605.10568v3
• Date: Wed, 20 May 2026 02:04:30 GMT
• Title: Correct-by-Construction G-Code Generation: A Neuro-Symbolic Approach via Separation Logic
• Abstract summary: This paper proposes a neuro-symbolic framework for G-code generation that seeks to integrate the neural generative capabilities of the GLLM method with formal verification via a Separation Logic prover.<n>Ultimately, this work aims to develop a self-correcting system that reduces the need for human supervision, leading to safer and verified autonomous manufacturing.
• Score: 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.

Related papers

• UniCoder: Unified Visual-to-Code Generation via Symbolic Rewards and Reference-Guided Code Optimization [22.627858794105066]
  We introduce UniCoder, a unified RL framework that integrates two novel mechanisms.<n>First, we propose textbfSymbolic Attribute Alignment, which employs a lightweight auxiliary LLM to parse generated code into discrete visual attributes.<n>Second, to escape local optima, we devise textbfReference-Guided Code Optimization, a strategy that dynamically injects ground-truth trajectories into low-performing rollout groups.
  arXiv  Detail & Related papers  (2026-06-30T14:29:48Z)
• Provably Secure Agent Guardrail [89.79561918065122]
  Existing defense architectures rely on empirical semantic guardrails and probabilistic large model adjudicators.<n>This paper proposes a new security paradigm for agents based on the fundamental limitations of logical reasoning.
  arXiv  Detail & Related papers  (2026-05-28T02:12:41Z)
• CasualSynth: Generating Structurally Sound Synthetic Data [44.80087038178069]
  Large Language Models (LLMs) generate realistic synthetic data but offer no guarantee that their outputs respect the causal mechanisms governing the target domain.<n>We introduce Causal Synth, a framework that decouples causal structure generation from semantic realization, yielding synthetic data that is both causally valid and linguistically rich.
  arXiv  Detail & Related papers  (2026-05-17T16:21:01Z)
• Separation Logic for Verifying Physical Collisions of CNC Programs [0.0]
  Safety verification in Computer Numerical Control (CNC) has traditionally relied on repetitive tests requirements change.<n>This paper conceptualizes a formal verification framework that conceptualizes physical simulation as a Spatial, treating managed logical kinematic model.
  arXiv  Detail & Related papers  (2026-05-11T12:09:17Z)
• How LLMs Fail and Generalize in RTL Coding for Hardware Design? [56.361436215029045]
  We introduce a new error taxonomy grounded in problem solvability, inspired by cognitive theory.<n>Our taxonomy categorizes failures into syntactic, semantic, solvable functional, and unsolvable functional types.
  arXiv  Detail & Related papers  (2026-04-26T14:34:49Z)
• CodeCircuit: Toward Inferring LLM-Generated Code Correctness via Attribution Graphs [13.488544043942495]
  We aim to investigate whether the model's neural dynamics encode internally decodable signals that are predictive of logical validity during code generation.<n>By decomposing complex residual flows, we aim to identify the structural signatures that distinguish sound reasoning from logical failure.<n>Analysis across Python, C++, and Java confirms that intrinsic correctness signals are robust across diverse syntaxes.
  arXiv  Detail & Related papers  (2026-02-06T03:49:15Z)
• SIGMA: Scalable Spectral Insights for LLM Collapse [51.863164847253366]
  We introduce SIGMA (Spectral Inequalities for Gram Matrix Analysis), a unified framework for model collapse.<n>By utilizing benchmarks that deriving and deterministic bounds on the matrix's spectrum, SIGMA provides a mathematically grounded metric to track the contraction of the representation space.<n>We demonstrate that SIGMA effectively captures the transition towards states, offering both theoretical insights into the mechanics of collapse.
  arXiv  Detail & Related papers  (2026-01-06T19:47:11Z)
• The Trojan in the Vocabulary: Stealthy Sabotage of LLM Composition [31.827344197678126]
  Tokenizer transplant introduces a supply-chain vulnerability.<n>By exploiting the geometry of coefficient reuse, our attack creates an asymmetric realizability gap.<n> Empirically, the attack is training-free and achieves spectral mimicry to evade outlier detection.
  arXiv  Detail & Related papers  (2025-12-31T19:00:03Z)
• Geometrically-Constrained Agent for Spatial Reasoning [53.93718394870856]
  Vision Language Models exhibit a fundamental semantic-to-geometric gap in spatial reasoning.<n>Current paradigms fail to bridge this gap.<n>We propose a training-free agentic paradigm that resolves this gap by introducing a formal task constraint.
  arXiv  Detail & Related papers  (2025-11-27T17:50:37Z)
• LLM-Empowered Event-Chain Driven Code Generation for ADAS in SDV systems [24.318466695095026]
  This paper presents an event-chain-driven, LLM-empowered workflow for generating validated, automotive code from natural-language requirements.<n>We managed to achieve valid signal usage and consistent code generation without LLM retraining.
  arXiv  Detail & Related papers  (2025-11-26T19:53:04Z)
• When LLMs Copy to Think: Uncovering Copy-Guided Attacks in Reasoning LLMs [30.532439965854767]
  Large Language Models (LLMs) have become integral to automated code analysis, enabling tasks such as vulnerability detection and code comprehension.<n>In this paper, we identify and investigate a new class of prompt-based attacks, termed Copy-Guided Attacks (CGA)<n>We show that CGA reliably induces infinite loops, premature termination, false refusals, and semantic distortions in code analysis tasks.
  arXiv  Detail & Related papers  (2025-07-22T17:21:36Z)
• AutoLayout: Closed-Loop Layout Synthesis via Slow-Fast Collaborative Reasoning [102.71841660031065]
  Auto is a fully automated method that integrates a closed-loop self-validation process within a dual-system framework.<n>The effectiveness of Auto was validated across 8 distinct scenarios, where it demonstrated a significant 10.1% improvement over SOTA methods.
  arXiv  Detail & Related papers  (2025-07-06T08:35:22Z)
• Training Language Models to Generate Quality Code with Program Analysis Feedback [66.0854002147103]
  Code generation with large language models (LLMs) is increasingly adopted in production but fails to ensure code quality.<n>We propose REAL, a reinforcement learning framework that incentivizes LLMs to generate production-quality code.
  arXiv  Detail & Related papers  (2025-05-28T17:57:47Z)
• Retrieval is Not Enough: Enhancing RAG Reasoning through Test-Time Critique and Optimization [58.390885294401066]
  Retrieval-augmented generation (RAG) has become a widely adopted paradigm for enabling knowledge-grounded large language models (LLMs)<n>RAG pipelines often fail to ensure that model reasoning remains consistent with the evidence retrieved, leading to factual inconsistencies or unsupported conclusions.<n>We propose AlignRAG, a novel iterative framework grounded in Critique-Driven Alignment (CDA)<n>We introduce AlignRAG-auto, an autonomous variant that dynamically terminates refinement, removing the need to pre-specify the number of critique iterations.
  arXiv  Detail & Related papers  (2025-04-21T04:56:47Z)
• Self-Healing Machine Learning: A Framework for Autonomous Adaptation in Real-World Environments [50.310636905746975]
  Real-world machine learning systems often encounter model performance degradation due to distributional shifts in the underlying data generating process. Existing approaches to addressing shifts, such as concept drift adaptation, are limited by their reason-agnostic nature. We propose self-healing machine learning (SHML) to overcome these limitations.
  arXiv  Detail & Related papers  (2024-10-31T20:05:51Z)
• Fault-tolerant simulation of Lattice Gauge Theories with gauge covariant codes [0.0]
  We show that a strong and easy connection exists between quantum error correction and Lattice Gauge Theories (LGT) We identify the logical operations on this gauge covariant code and show that the corresponding Hamiltonian can be expressed in terms of these logical operations. We demonstrate a method to perform fault-tolerant time evolution of the Hamiltonian within the gauge covariant code using both product formulas and qubitization approaches.
  arXiv  Detail & Related papers  (2024-05-29T17:21:29Z)
• Neuro-Symbolic Integration Brings Causal and Reliable Reasoning Proofs [95.07757789781213]
  Two lines of approaches are adopted for complex reasoning with LLMs.<n>One line of work prompts LLMs with various reasoning structures, while the structural outputs can be naturally regarded as intermediate reasoning steps.<n>The other line of work adopt LLM-free declarative solvers to do the reasoning task, rendering higher reasoning accuracy but lacking interpretability due to the black-box nature of the solvers.<n>We present a simple extension to the latter line of work. Specifically, we showcase that the intermediate search logs generated by Prolog interpreters can be accessed and interpreted into human-readable reasoning.
  arXiv  Detail & Related papers  (2023-11-16T11:26:21Z)
• Disentanglement via Latent Quantization [60.37109712033694]
  In this work, we construct an inductive bias towards encoding to and decoding from an organized latent space. We demonstrate the broad applicability of this approach by adding it to both basic data-re (vanilla autoencoder) and latent-reconstructing (InfoGAN) generative models.
  arXiv  Detail & Related papers  (2023-05-28T06:30:29Z)
• Unsupervised Controllable Generation with Self-Training [90.04287577605723]
  controllable generation with GANs remains a challenging research problem. We propose an unsupervised framework to learn a distribution of latent codes that control the generator through self-training. Our framework exhibits better disentanglement compared to other variants such as the variational autoencoder.
  arXiv  Detail & Related papers  (2020-07-17T21:50:35Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.