# Towards Neuro-symbolic Causal Rule Synthesis, Verification, and Evaluation Grounded in Legal and Safety Principles
**Authors**: Zainab Rehan, Christian Medeiros Adriano, Sona Ghahremani, Holger Giese
none [NEXUS ’26]Proc. of the Neurosymbolic eXplainable Trustworthy Systems Workshop (NEXUS 2026)May 25 – 26, 2026Paphos, Cyprus,https://nexus.telecom-paris.frBakirtzis, Fridovich-Keil , Kakas, Theodorou, Li, McKinlay (eds.) 2026 2026 printacmref=false ¡¡submission id¿¿ 0009-0005-9336-9505 Hasso Plattner Institute University of Potsdam Prof.-Dr.-Helmert Str. 2-3, D-14482 Potsdam, Germany 0000-0003-2588-9937 Hasso Plattner Institute University of Potsdam Prof.-Dr.-Helmert Str. 2-3, D-14482 Potsdam, Germany 0000-0003-0697-9195 Hasso Plattner Institute University of Potsdam Prof.-Dr.-Helmert Str. 2-3, D-14482 Potsdam, Germany IEEE and ACM Member 0000-0002-4723-730X Hasso Plattner Institute University of Potsdam Prof.-Dr.-Helmert Str. 2-3, D-14482 Potsdam, Germany
## Abstract
Rule-based systems remain central in safety-critical domains but often struggle with scalability, brittleness, and goal misspecification. These limitations can lead to reward hacking and failures in formal verification, as AI systems tend to optimize for narrow objectives. In previous research, we developed a neuro-symbolic causal framework that integrates first-order logic abduction trees, structural causal models, and deep reinforcement learning within a MAPE-K loop to provide explainable adaptations under distribution shifts. In this paper, we extend that framework by introducing a meta-level layer designed to mitigate goal misspecification and support scalable rule maintenance. This layer consists of a Goal/Rule Synthesizer and a Rule Verification Engine, which iteratively refine a formal rule theory from high-level natural-language goals and principles provided by human experts. The synthesis pipeline employs large language models (LLMs) to: (1) decompose goals into candidate causes, (2) consolidate semantics to remove redundancies, (3) translate them into candidate first-order rules, and (4) compose necessary and sufficient causal sets. The verification pipeline then performs (1) syntax and schema validation, (2) logical consistency analysis, and (3) safety and invariant checks before integrating verified rules into the knowledge base. We evaluated our approach with a proof-of-concept implementation in two autonomous driving scenarios. Results indicate that, given human-specified goals and principles, the pipeline can successfully derive minimal necessary and sufficient rule sets and formalize them as logical constraints. These findings suggest that the pipeline supports incremental, modular, and traceable rule synthesis grounded in established legal and safety principles.
Key words and phrases: Rule synthesis, Neuro-symbolic methods, Software verification, Causality, Goal specification
## 1. Introduction
Context – Rule-based systems liu2016rulebased are specified and constructed from existing domain knowledge about desired and undesired (forbidden, unsafe) behavior, often as logical if–then statements. Rule-based approaches remain central in many safety- and mission-critical contexts because rules make system behavior observable at runtime and open to formal verification hayesroth1983rulebased; musen1989brittleness.
In self-adaptive and autonomic systems, the MAPE-K feedback loop kephart2003autonomic represents monitoring, analysis, planning, and execution as activities over a shared knowledge base (of rules and representation models). These systems often rely on runtime enforcement components that supervise primary controllers and trigger predefined mitigation actions when rules are violated musen1989brittleness; almeida2017mapekguidelines.
Challenges – However, rule-based and expert systems are widely recognized for their brittleness and limited scalability. As new requirements emerge, even minor changes can cause cascading revisions across numerous interdependent rules. Managing and tracking these evolving rules places a significant cognitive and organizational burden on human experts, often becoming a central bottleneck and increasing the risk of unexpected failures musen1989brittleness; greene1987automated. Classic analyses of earlier expert systems highlight the exponential increase in maintenance effort and the well-known “knowledge acquisition bottleneck.” In practice, large rule sets are inherently difficult to extend or adapt without unintentionally disrupting existing behaviors greene1987automated; musen1989brittleness. These issues were prominent in large, early AI expert-system projects, which helped motivate later shifts toward methods that combine statistical learning with more scalable forms of knowledge representation lenat1990using; musen1989brittleness.
Approach – We extend a prior neuro-symbolic causal framework for self-adaptive, learning-enabled systems with a meta-level synthesis and verification layer that incrementally refines the governing rule theory. A Goal/Rule Synthesizer uses large language models to decompose high-level, natural-language goals and principles into candidate causes, consolidate their semantics, and translate them into candidate first-order rules while identifying necessary and sufficient cause sets. A complementary Rule Verification Engine then enforces syntax and schema correctness, logical consistency, and safety and invariant constraints before integrating only verified rules into the knowledge base. Together, these components realize an incremental, modular, and traceable pipeline from human-specified legal and safety principles to formally verified rule sets, demonstrated on autonomous driving scenarios.
Evaluation – We present an application in the domain of autonomous driving, where safety goals are systematically decomposed into subgoals and translated into corresponding rules. The mapping between goals and rules is realized via simulated abduction that produces explanations of an effect from its causes, while rule refinement is performed through deductive reasoning, de-duplicating rules and combining them into necessary and sufficient sets. We evaluated our approach with a proof-of-concept implementation in two autonomous driving scenarios, showing that, given human-specified goals and principles, the pipeline can successfully derive minimal necessary and sufficient rule sets and formalize them as logical constraints. These findings suggest that the pipeline supports incremental, modular, and traceable rule synthesis grounded in established legal and safety principles.
Contributions – By structuring rule maintenance as an incremental, meta-level synthesis-and-verification loop, the approach directly attacks the scalability and brittleness problems of classic rule-based systems. First, high-level goals are decomposed into modular sets of necessary and sufficient rules per goal, so extensions localize to specific goal-linked modules instead of triggering cascading revisions across a monolithic rule base. Second, semantic consolidation, de-duplication, and explicit traceability from each rule back to its originating goal and principles reduce redundancy and make large rule sets easier to understand, audit, and evolve. Third, the Rule Verification Engine systematically filters new rules through syntax, consistency, and safety checks before reintegration, preventing brittle, ad hoc patches and enabling controlled growth of the theory over time. Reproduction package is available at repo2026rulesynthesis.
## 2. State of the Art
Goal Decomposition with LLMs – LLMs can decompose complex goals into structured subgoals for planning and assistance. Multi-step plans are generated, refined, and evaluated aghzal2025survey. SGA-ACR fan2025subgoal produces verifiable sub-goal chains for RL agents, while DELTA liu2025delta leverages scene graphs for efficient long-horizon task decomposition. Hierarchical LLM agents improve tractability and interpretability hill2025generativeworldmodelstasks, and human-centered methods wen2024learning learn decompositions that enhance non-expert performance on complex programming tasks.
Abduction and Rule Synthesis – Abductive reasoning generates explanatory hypotheses and candidate symbolic rules Aliseda2017, providing a principled path from observations to minimal assumptions and compact rule-like hypotheses paul1993approaches. Statistical learning links, via inductive logic programming and statistical relational learning, allow frequent patterns or abductive explanations to become human-interpretable if–then rules DeRaedtKersting2008; hitzler2022neural. Contemporary neuro-symbolic approaches use abduction as structured prior knowledge to guide neural learners, improving sample efficiency. Extracted hypotheses can be refined and pruned to produce robust, generalizable adaptation rules, bridging observed outcomes and formalized reusable knowledge for self-adaptive systems Aliseda2017; DeRaedtKersting2008; hitzler2022neural.
Causal-Neuro-Symbolic Reasoning - Causal neuro-symbolic AI combines the strengths of causal inference, symbolic reasoning, and deep learning to produce models that are both adaptable and explanatory jaimini2024causal. In such hybrid frameworks, symbolic structures (e.g., causal graphs or abduction trees) provide interpretable scaffolding for interventions and counterfactual reasoning while neural components supply flexible function approximation for perception and policy learning. Recent work demonstrates how causal abstractions can be learned or exploited by agents to accelerate adaptation and to ground symbolic recovery strategies in measurable causal effects jaimini2024causal; korte2025causal. Applications in multi-agent reinforcement learning show further promise: transferable macro-actions or recovery primitives can be represented as compact causal rules that capture cause & effect pathways linking failures to corrective actions, enabling agents to exchange and re-use causal knowledge across contexts korte2025causal; yang2018peorl. Integrating such transferable causal experiences into symbolic abduction structures enriches the abductive search space with empirical, distributed evidence, thereby improving both the quality of synthesized rules and their generalizability across agents and environments.
Knowledge Representation in Rule-based Systems Rule-based systems and first-order logic support complex and commonsense reasoning but often incur high computational costs kernisberner2020syntax; murali2023firstorder. To improve scalability, global theories are partitioned into context-specific modules, enabling local reasoning while maintaining overall consistency beierle2024conditional; oikarinen2006modular; eiter2016model. Techniques such as monotonic and nonmonotonic reasoning, syntax splitting, modular answer set programming, and context-oriented logics support efficient reasoning and inter-context communication kernisberner2020syntax; beierle2024conditional; oikarinen2006modular; murali2023firstorder; eiter2016model. Probabilistic graphical models and related network structures integrate local results into coherent global knowledge, balancing expressiveness with computational manageability korte2025causal.
## 3. Research Problems
Humans often state goals imprecisely, while AI systems pursue them with strict literalism. This can lead to unintended outcomes, because AI models may exploit loopholes to technically complete a task rather than follow the user’s true intent. Moreover, human communication relies on shared context that AI systems typically lacks. Therefore, vague instructions are particularly hazardous, because cannot be easily confirmed and disambiguated by external sources.
These issues manifest in concrete failure modes such as formal proof cheating and reward hacking. Formal proof cheating occurs when an AI produces a proof that technically satisfies formal criteria but does so by altering axioms or definitions, ignoring the genuine mathematical intent brodsky2025mathematicians. Reward hacking skalse2022defining occurs when an AI system exploits imperfections in a proxy reward function, achieving high measured performance while violating the underlying goal.
Goal misspecification is therefore a central problem in AI safety amodei2016concrete, especially when formal objectives diverge from the informal intent of system designers. Goodhart’s law in machine learning further predicts that proxy metrics tend to degrade when heavily optimized lesswrong2023rewardmisspecification; weng2024reward, whether the goals are misspecified or merely underspecified.
Even when designers choose the right high-level goals, they may still encode them in ways that are too narrow or incomplete, leading AI systems to optimize the measurable formal metric rather than the broader human objective it was meant to approximate. Essentially, humans rely on vague, context-dependent, and partly unconscious goals castrellon2021dopamine; hu2025goals; fiedler2014limits. Conversely, AI systems require precise, formal, and loophole-free specifications to behave as intended amodei2016concrete.
Accordingly, humans need support tools that help them articulate more precise and robust specifications that reduce misinterpretation or manipulative compliance by AI systems. This support must go beyond traditional verification and validation. In this paper, we propose a vision of goal-specification assistance centered on explicit rules and their systematic composition. We explore these fundamental challenges through two research questions.
- RP.1 – What are the current capabilities of generative AI to support the synthesis of rules in a principled way that minimizes redundancies and ambiguities while maintaining traceability to system goals? Our approach – Establish operations that refine rules via deduction and explain their effect via abduction.
- RP.2 – How can rule synthesis be automatically evaluated in incremental and modular ways? Our approach – Search for sufficient and necessary rule sets that satisfy a given goal.
General Insight – We consider goals and subgoals as effects of rules (causes) and their preconditions (controls). Moreover, will rely on causal representations and fundamental domain laws to constrain reasoning about rules and their effects with respect to system adaptations that preserve performance and safety adriano2025neuro; ghahremani2021hybrid.
## 4. Approach
The proposed approach builds on our previous work adriano2025neuro, which is a neuro-symbolic (NeSy) causal reasoning framework for learning-enabled self-adaptive systems ghahremani2018training; gheibi2021applying in particular when operating under distribution shifts gheibi2024dealing and under safety-critical goals hansel2020collective —see Section 4.1. As depicted in Figure 1, the approach comprises a Goal/Rule Synthesizer and a Rule Verification Engine on top of the NeSy framework—see Section 4.2.
### 4.1. NeSy Causal Framework
The Neuro-Symbolic (NeSy) causal framework integrates three complementary representations: (1) Symbolic Abduction Trees (SAT) grounded in first-order logic (FOL) to formally encode domain knowledge, system constraints, and adaptation rules, enabling logical abduction to explain observed violations; (2) a structural causal model (SCM) that represents dependencies between environment and system variables and supports intervention and counterfactual reasoning; and (3) a deep reinforcement learning (DRL) policy responsible for operational decision-making–see Figure 1 for a reference. The three representation spaces are embedded within the MAPE-K (Monitor-Analyze-Plan-Execute) feedback loop as the reference model for self-adaptive systems kephart2003autonomic. The process begins with monitoring execution traces from the DRL agent to detect distribution shifts and safety-constraint violations. In the analysis and planning phases, FOL-based abductive reasoning identifies candidate explanations, while the causal model evaluates intervention effects and selects minimal, high-explanatory-power configuration changes. These interventions guide knowledge transfer and warm-start retraining of the DRL agent, whose updated behavior produces new traces that refine both symbolic and causal knowledge. The framework thus interleaves logical reasoning, causal inference, and learning to enable explainable, constraint-aware adaptation rather than reactive retraining.
<details>
<summary>2604.28087v1/x1.png Details</summary>
### Visual Description
## Diagram: NeSy Causal Framework Architecture
### Overview
The image presents a high-level system architecture diagram for a "NeSy Causal Framework" (Neural-Symbolic Causal Framework). The diagram is vertically bifurcated into two primary functional levels: the "Synthesis & Verification Level" at the top and the "NeSy Causal Framework" at the bottom. It illustrates the data flow and logical relationships between rule synthesis, verification, causal reasoning, and environmental interaction, utilizing components like Deep Reinforcement Learning (DRL), Satisfiability (SAT), and Structural Causal Models (SCM).
### Components/Axes
**1. Synthesis & Verification Level (Top Section)**
* **New Rules:** A database icon (light red) located at the top-left.
* **Rule Verification Engine:** A blue rectangle located at the top-center.
* **Goal/Rule Synthesizer:** A purple rectangle located below "New Rules".
* **Verified rules:** A database icon (light red) located below the "Rule Verification Engine".
* **Theory (Top-Right):** A grey box containing a database icon labeled "Theory" and three overlapping circles labeled "SAT", "SCM", and "DRL".
* **Label:** "Synthesis & Verification Level" is written vertically on the far right.
**2. NeSy Causal Framework (Bottom Section)**
* **Theory (Top-Center):** A database icon (dark blue) located at the top of the main framework box.
* **Knowledge:** A central grey box containing three overlapping circles labeled "DRL", "SAT", and "SCM".
* **Analyze:** A white rectangle to the left of the "Knowledge" box.
* **Monitor:** A white rectangle below "Analyze".
* **Causal Reasoning Engine:** A dark grey rectangle to the right of the "Knowledge" box.
* **Plan:** A label positioned to the right of the "Causal Reasoning Engine".
* **Execute:** A white rectangle below the "Causal Reasoning Engine".
* **Self-adaptive DRL agent:** A white rectangle in the bottom-center.
* **Environment:** A white rectangle at the very bottom.
* **Label:** "NeSy Causal Framework" is written vertically on the far right.
### Detailed Analysis
**Flow and Connectivity:**
* **Synthesis Path:** "New Rules" flows into the "Rule Verification Engine" and the "Goal/Rule Synthesizer". The "Goal/Rule Synthesizer" feeds back into the "Rule Verification Engine".
* **Verification Path:** The "Rule Verification Engine" interacts with the top-right "Theory" block. It outputs to "Verified rules".
* **Integration Path:** "Verified rules" feeds into the central "Theory" database icon (top of the bottom section).
* **Operational Path (AKPE):** The central "Theory" database feeds into the "Analyze" component and the "Causal Reasoning Engine".
* The "Knowledge" block acts as the central hub for "Analyze", "Monitor", "Causal Reasoning Engine", and "Execute".
* The "Self-adaptive DRL agent" has a bidirectional relationship with the "Knowledge" block and the "Environment".
**Acronym Definitions (Inferred from context):**
* **DRL:** Deep Reinforcement Learning
* **SAT:** Satisfiability (Boolean Satisfiability Problem)
* **SCM:** Structural Causal Model
### Key Observations
* **Modularity:** The architecture clearly separates the *creation* of rules (Synthesis & Verification) from the *application* of rules (NeSy Causal Framework).
* **Centrality of Theory:** The "Theory" component appears twice, acting as the bridge between the verification level and the operational framework.
* **The AKPE Pattern:** The central framework is organized around four key functions: **A**nalyze, **K**nowledge (central hub), **P**lan (associated with Causal Reasoning), and **E**xecute.
* **Feedback Loops:** The "Self-adaptive DRL agent" is the only component with direct, bidirectional interaction with the "Environment," suggesting it is the active controller of the system.
### Interpretation
This diagram illustrates a **Neural-Symbolic (NeSy) architecture** designed to make AI agents more robust and explainable.
* **The Problem Solved:** Pure Deep Reinforcement Learning (DRL) is often a "black box" and can behave unpredictably. By introducing a "Synthesis & Verification Level," the system ensures that the rules governing the agent are mathematically verified (using SAT/SCM) before they are deployed.
* **The Mechanism:** The system uses "Theory" as a grounding mechanism. The "Knowledge" block serves as the repository where neural learning (DRL) is constrained or guided by symbolic logic (SAT/SCM).
* **Peircean/Logical Flow:** The system follows a logical progression:
1. **Abduction/Induction:** "New Rules" are synthesized.
2. **Deduction/Verification:** Rules are verified against "Theory."
3. **Execution:** The "Self-adaptive DRL agent" applies this verified knowledge to the "Environment," monitors the results, and potentially updates its strategy via the "Causal Reasoning Engine."
* **Significance:** This architecture is likely intended for high-stakes environments (e.g., robotics, autonomous systems) where the agent must adhere to strict safety or operational rules while still benefiting from the adaptive capabilities of reinforcement learning.
</details>
Figure 1. Extending NeSy Causal Framework with Rule-synthesis and Verification
### 4.2. Synthesis $\&$ Verification Level
The Synthesis $\&$ Verification Level extends the original NeSy framework by introducing a meta-self-aware synthesis and verification layer on top of the operational adaptation cycle. In contrast to the earlier framework, the outputs of causal explanation are no longer used solely for policy adaptation. Instead, anomaly reports are forwarded to the higher synthesis $\&$ verification level. This level contains a Goal/Rule Synthesizer and a Rule Verification Engine that collectively update the theory that comprises domain knowledge, system constraints, and adaptation rules. Verified rules are reintegrated into the knowledge base, thereby modifying future analysis and planning steps. The architecture, therefore, introduces a closed meta-loop in which the system adapts not only its behavior but also its governing symbolic FOL theory, enabling progressive self-improvement and increased explainability.
Goal/Rule Synthesizer – The pipeline (see Figure 2) receives as input the high-level goals and governing principles provided by a human expert expressed in natural language (natural-language based, NLB) rather than as formal constraints, following the detection of a drift or anomaly. The first step uses a large language model (LLM) to decompose each high-level goal into a set of lower-level candidate causes, representing concrete conditions, behaviors, or system properties that collectively could realize or justify the intended goal. These generated causes are then reprocessed by the LLM in a semantic consolidation step, where overlapping, redundant, or semantically equivalent causes are identified and merged. This normalization produces a consistent set of unique causes, ensuring that the emerging theory avoids duplication and ambiguity. In the next step, the consolidated causes are again provided to the LLM for symbolic translation, mapping natural-language concepts into candidate logical predicates and relations and producing a set of new, unverified rules (causes) expressed in FOL. The resulting logical rules enable formal reasoning during the Rule Verification pipeline, e.g., using a verification solver such as Z3 de2008z3. The goal/rule synthesizer pipeline analyzes combinations of causes to determine subsets of necessary and sufficient conditions that adequately justify the original synthesized Goal (more details in Section 4.3). The output of this pipeline is a set of newly synthesized but still unverified logical rules representing intended behavior derived jointly from empirical evidence and human intent.
<details>
<summary>2604.28087v1/x2.png Details</summary>
### Visual Description
## Process Flow Diagram: Goal / Rule Synthesizer
### Overview
The image depicts a logical workflow diagram titled "Goal / Rule Synthesizer." It illustrates a multi-stage process for transforming high-level human goals and principles into verified logical rules. The diagram utilizes a left-to-right primary flow, supplemented by various data inputs (yellow artifacts) and feedback loops (dashed lines).
### Components/Axes
The diagram is organized into a linear process flow with auxiliary data inputs.
**1. Primary Process Nodes (White Rectangles):**
* **Decomposition to Causes:** The first processing step.
* **Semantic Consolidation:** The second processing step.
* **Symbolic Translation:** The third processing step.
**2. Specialized Process Nodes:**
* **Evaluate Necessary & Sufficient Causes (Green Rectangle):** Located in the bottom-right quadrant, this acts as a decision or evaluation gate.
* **Rule Verification Engine (Blue Rectangle):** The final stage of the process, located at the bottom right.
**3. Data/Artifact Inputs (Yellow Document Icons):**
* **Principles** (Top-left)
* **High-level Goal** (Top-left)
* **Candidate Causes** (Top-center)
* **Unique Causes (NLB)** (Top-right)
* **New Unverified Rules (FOL)** (Center)
* **Necessary Causes** (Bottom-left)
* **Sufficient Causes** (Bottom-center)
**4. Flow Indicators:**
* **Solid Arrows:** Represent the primary, sequential progression of the workflow.
* **Dashed Arrows:** Represent dependencies, data inputs, or feedback loops.
* **Start Point:** A black dot on the far left initiates the flow.
* **User Icon:** A stylized human figure represents the source of the initial input.
### Detailed Analysis
**The Workflow Sequence:**
1. **Initiation:** The process begins at the black dot. A user provides input, which is informed by "Principles" and "High-level Goal" (indicated by dashed arrows pointing to the main flow line).
2. **Decomposition:** The flow enters the "Decomposition to Causes" node. A dashed arrow points upward to "Candidate Causes," suggesting this node generates or identifies these causes.
3. **Consolidation:** The flow proceeds to "Semantic Consolidation." A dashed arrow points upward to "Unique Causes (NLB)."
4. **Translation:** The flow proceeds to "Symbolic Translation." A dashed arrow points upward to "New Unverified Rules (FOL)."
5. **Evaluation:** The output of "Symbolic Translation" flows downward into the green "Evaluate Necessary & Sufficient Causes" node.
* This node receives additional inputs from "Necessary Causes" and "Sufficient Causes" (dashed arrows pointing rightward into the node).
* There is a feedback loop (dashed arrow) pointing from the green node back to "Semantic Consolidation," suggesting that if evaluation fails, the system iterates.
6. **Verification:** The final output flows from the green node into the blue "Rule Verification Engine."
### Key Observations
* **Terminology:**
* **NLB:** Likely refers to "Natural Language Base" or "Natural Language Bridge," given the context of semantic consolidation.
* **FOL:** Standard abbreviation for "First-Order Logic," confirming the transition from semantic/natural language to formal logic.
* **Iterative Design:** The presence of dashed feedback loops (specifically from the "Evaluate" node back to "Semantic Consolidation" and from "New Unverified Rules" back to "Semantic Consolidation") indicates that this is a recursive or iterative system rather than a strictly linear one.
* **Color Coding:**
* **Yellow:** Represents external inputs, knowledge bases, or intermediate artifacts.
* **White:** Represents core processing logic.
* **Green:** Represents the evaluation/validation logic.
* **Blue:** Represents the final execution/verification environment.
### Interpretation
This diagram represents a system architecture designed to bridge the gap between human intent and machine-executable logic.
The process demonstrates a "translation pipeline":
1. **Abstraction to Concrete:** It starts with abstract human concepts ("High-level Goal," "Principles") and decomposes them into concrete "Causes."
2. **Semantic to Symbolic:** It moves from "Semantic Consolidation" (likely handling natural language or conceptual grouping) to "Symbolic Translation" (converting concepts into formal logic, i.e., FOL).
3. **Validation:** The system does not assume the generated rules are correct. It explicitly includes an "Evaluate Necessary & Sufficient Causes" step, which acts as a quality control gate before the rules reach the "Rule Verification Engine."
The architecture suggests a robust, iterative approach where the system refines its rule set based on the evaluation of necessary and sufficient conditions, ensuring that the final rules are logically sound before they are verified.
</details>
Figure 2. Pipeline for Goal/Rule Synthesizer
Rule Verification Engine - The synthesized rule candidates are forwarded to the Rule Verification Engine, where formal consistency and safety validation are performed to ensure that synthesized rules can be safely incorporated into the system theory–see Figure 3. The layered pipeline consists of (1) syntactic and schema validation, ensuring that generated rules conform to the logical language and domain ontology together with semantic grounding checks, confirming that predicates and variables correspond to valid system entities; (2) logical consistency analysis, where candidate rules are evaluated against the existing FOL knowledge base to detect contradictions; and (3) safety and invariant verification, which formally checks whether the rules preserve required system properties. The pipeline employs an automated reasoning tool to perform satisfiability and entailment checks. Only rules that satisfy all verification stages are promoted to a verified theory and committed to the knowledge repository. This verified knowledge is then fed back into the adaptive loop, ensuring that future adaptations are guided by formally verified, explainable principles rather than purely data-driven updates.
### 4.3. Illustrative Scenario for Goal/Rule Synthesis Pipeline
We demonstrate the Goal/Rule Synthesis Pipeline based on an application in the domain of autonomous driving.
Decomposition to Causes - The high-level goal (effect) represents a scenario derived from everyday driving tasks. The objective is to generate candidate causes that explain how the effect may occur. For example, the effect “respond correctly to a sudden obstacle on the road” may be explained by the cause “the driver applies emergency braking.” The LLM decomposes the effect into candidate causes required to achieve it while ensuring safety and compliance with traffic regulations. The synthesis process is strictly constrained to limit hallucinations and unrelated reasoning, resulting in causes that are logically consistent with the effect and with the defined constraints.
<details>
<summary>2604.28087v1/x3.png Details</summary>
### Visual Description
## Process Flow Diagram: Rule Verification Engine
### Overview
The image displays a linear workflow diagram titled "Rule Verification Engine." It illustrates the lifecycle of a rule, starting from an unverified state, passing through three distinct verification stages, and concluding as a verified rule. The entire process is contained within a light blue rounded rectangular background.
### Components/Axes
The diagram is organized horizontally from left to right.
* **Header/Title:** "Rule Verification Engine" (centered at the top).
* **Input Component (Top-Left):** A pink, document-shaped box labeled "New Rules (Unverified)."
* **Start Node:** A solid black circle located on the far left of the main flow line.
* **Process Steps (Main Flow, Left to Right):**
1. **Syntax & Schema Verification:** A white rectangular box.
2. **Logical Consistency Check:** A white rectangular box.
3. **Safety Invariant Verification:** A white rectangular box.
* **Output Component (Top-Right):** A pink, document-shaped box labeled "New Rules (Verified)."
* **End Node:** A hollow circle located on the far right of the main flow line.
* **Connectors:**
* **Solid lines with arrows:** Indicate the primary left-to-right progression of the process.
* **Dashed lines with arrows:** Indicate the injection of input data (from the unverified box) and the extraction of output data (to the verified box).
### Detailed Analysis
The process flow follows a sequential, unidirectional path:
1. **Initialization:** The process begins at the solid black circle.
2. **Input Injection:** A dashed arrow points from the "New Rules (Unverified)" box to the main flow line, immediately following the start node.
3. **Stage 1 (Syntax & Schema Verification):** The flow enters the first white box. This stage likely validates the structural integrity and formatting of the rules.
4. **Stage 2 (Logical Consistency Check):** The flow proceeds to the second white box. This stage likely validates the semantic correctness or logical soundness of the rules.
5. **Stage 3 (Safety Invariant Verification):** The flow proceeds to the final white box. This stage likely validates that the rules adhere to predefined safety constraints.
6. **Output Extraction:** A dashed arrow points from the main flow line (after the final verification step) to the "New Rules (Verified)" box.
7. **Termination:** The process concludes at the hollow circle on the far right.
### Key Observations
* **Linearity:** The diagram represents a "happy path" workflow. There are no visible feedback loops, error-handling branches, or rejection paths shown.
* **Color Coding:** The use of pink for the input/output states and white for the processing steps creates a clear visual distinction between data states and functional operations.
* **Hierarchy of Verification:** The placement of "Safety Invariant Verification" as the final step suggests it is the most critical or perhaps the most computationally intensive check, performed only after the rule has passed structural and logical validation.
### Interpretation
This diagram represents a high-level architectural abstraction of a rule-processing pipeline.
* **Functional Logic:** The engine acts as a filter. By placing "Syntax & Schema" first, the system ensures that only well-formed data reaches the more complex "Logical" and "Safety" checks, optimizing computational resources.
* **Safety-Critical Design:** The inclusion of a specific "Safety Invariant Verification" step implies that this engine is likely used in a high-stakes environment (such as industrial control systems, autonomous vehicle logic, or financial compliance) where rule correctness is not just about logic, but about preventing catastrophic outcomes.
* **Missing Information:** As a "happy path" diagram, it omits the "what happens if it fails" scenario. In a real-world implementation, there would necessarily be exit points or error-handling branches from each of the three verification boxes to handle invalid rules. The absence of these suggests this is a conceptual model rather than a complete system architecture diagram.
</details>
Figure 3. Pipeline for Rule verification Engine
Semantic Consolidation – Although the focus is restricted at the first step, there is still a need to merge causes that refer to similar concepts to reduce general statements that overlap into a set of unique causes. The semantic consolidation step is carried out to combine causes that describe the same underlying condition. ”Driver maintains control of the vehicle” and ”Driver is aware of surrounding traffic” are combined into a cause as ”Driver maintains control of the vehicle and is aware of surrounding traffic”.
Symbolic Translation – After generating unique causes, each cause is translated from natural language to formal symbolic (FOL) form to enable structured reasoning and systematic subset evaluation. Although this step follows semantic unification in Figure 2, it can be applied at any stage without altering content. Subsequent analysis uses the natural language causes for stronger LLM reasoning, with FOL forms used only in the rule verification pipeline Figure 3. This decision is based on the observation that LLMs demonstrate stronger reasoning performance when operating on natural language inputs. To ensure consistency and avoid ambiguity, a formal grammar is defined in the prompt, and the model is instructed to strictly follow it. Each cause is thus mapped to a structured logical form that preserves its meaning while remaining machine-interpretable.
Alongside the FOL rule, the LLM also provides a brief explanation of its translation, detailing how the natural language condition was interpreted and which predicates and operators were chosen. This enhances transparency, verifies semantic alignment, and improves interpretability of the symbolic mapping.
Evaluate Necessary $\&$ Sufficient Causes – After obtaining a set of unique causes, the next step involves assessing the necessity and sufficiency of each cause with respect to the main goal (effect). We break this down into three steps described below:
1. Individual Necessity Evaluation is concerned with whether each cause is essential and provides a justification, citing specific legal or safety conditions that would be violated if absent. Each cause is assessed independently, and the output is a structured list recording the cause, its necessity, and the rationale.
1. Subset Necessity Evaluation identifies causes that are essential only in combination. Starting with the full set, causes are removed one at a time, and the feasibility of the effect is confirmed. A cause is deemed necessary if after its removal, the effect is judged unachievable. A removed cause or set of causes is recorded as a minimal necessary subset if no smaller subset produces the same effect. To improve efficiency, the candidate subsets containing already identified minimal subsets are skipped, and the outcomes of previous evaluations are cached. This bottom-up approach ensures that all truly minimal necessary combinations are captured while reducing computational effort.
1. Minimal Sufficient Set Evaluation aims at identifying the subsets of causes that are individually sufficient to produce a given effect. We start with single causes and test their sufficiency, incrementally adding additional causes if the effect does not occur. This process continues until a sufficient subset is found, and is repeated across all relevant combinations. To reduce computational effort, supersets of already identified sufficient subsets are skipped, as sufficiency is preserved under addition. Once all minimal sufficient sets are determined, they can be combined into a necessary-and-sufficient set, which guarantees the effect and is required for its occurrence. This set unifies all alternative minimal sufficient causes, capturing every pathway to the effect within a single comprehensive framework.
## 5. proof of concept
Experimental Setup - We design a controlled experiment to show how Large Language Models (LLMs) can help automate parts of the Goal/Rule Synthesizer pipeline illustrated in Figure 2. The objective of this setup is to evaluate realistic driving scenarios in which an intended effect (Goal) must be explained by a set of underlying causes (Rules). The intent is not to verify causality in a statistical sense, but to show how LLMs can be guided to perform structured abductive and deductive reasoning. The scope of the setup is constrained by a predefined set of legal and safety regulations that define the boundaries within which the synthesis and reasoning process operates.
### 5.1. Implementation Overview
The pipeline is implemented by leveraging the OpenAI GPT-4o Mini model openai2025 to perform all processing tasks. Step by step, the process transforms an human stated goal (effect) description into a set of candidate causes. The process begins with cause generation, followed by consolidation of overlapping causes, then individual evaluation, and finally, subset analysis for necessity and sufficiency. This iterative design ensures that the reasoning is incremental, traceable, and easy to interpret at every step. The legal and safety regulations that guide the process are defined prior to the first stage. These regulations serve as the sole reference for the model throughout the pipeline. For details on how these principles were sourced and compiled–see Section 5.2.
### 5.2. Data Sources
Legal Principles:
The legal Principles used in this work are derived from a formalized set of German traffic regulations designed for machine interpretability. These regulations define rules such as maintaining vehicle control, adhering to speed limits, and keeping safe distances. We selected the most relevant laws from this formalized research esterle2020formalizing. To cover broader scenarios encountered in everyday driving, we then extended the set using generative AI, specifically ChatGPT. This ensures that the legal knowledge can guide the model in a variety of realistic situations while remaining interpretable and precise.
Safety Principles:
The safety principles capture physical principles of vehicle motion. Initially, we developed a basic set of rules representing logical and physics-based constraints. Examples include limits on friction, constraints on braking distance, and conditions that increase the risk of losing traction at high speeds. To expand coverage, ChatGPT was used to generate additional rules representing general principles, e.g., as ”collision_if_obstacles”, which states that a vehicle may collide if obstacles are present. This expanded set allows the model to account for a wider variety of practical driving scenarios while remaining grounded in physical feasibility.
Grammar and Symbolic Rule Language:
The symbolic grammar used for translating natural language causes into formal rules is based on the same formalization framework presented in esterle2020formalizing. The original predicate set is extended to incorporate additional predicates related to fundamental speed and friction properties in order to capture physics-based safety constraints. Moreover, the grammar specifies the allowed rule forms, comparison operators, and logical operators that may be used in rule construction.
All reasoning carried out by the LLM is grounded in these curated laws, which serve as the primary reference for evaluating causes. External knowledge or assumptions beyond this curated set are not used. This guarantees that all cause & effect evaluations remain valid, consistent, and reproducible. A complete listing of all legal and safety laws used is provided in the Appendix repo2026rulesynthesis.
### 5.3. Results
We analyze two illustrative scenarios to demonstrate the outputs of the pipeline. For each scenario, candidate causes were generated, semantically consolidated, individually evaluated for necessity, and subsequently analyzed to identify minimal necessary subsets and sufficient subsets..
#### 5.3.1. Scenario 1: Successfully Merge into Heavy Traffic
Decomposition and Consolidation
Eight candidate causes were initially generated. After semantic de-duplication, four unique consolidated causes remained:
1. Driver maintains control of the vehicle and is aware of surrounding traffic.
1. Vehicle is traveling at a speed that allows for safe merging and adheres to traffic laws regarding merging.
1. Sufficient distance is kept from other vehicles to merge safely, and no vehicles are overtaking on the right.
1. Traffic conditions allow for merging without impeding flow, and no sudden obstacles in the merging path.
Individual Necessity Evaluation
Each consolidated cause was evaluated independently against the relevant safety and legal constraints. Only the first two were classified as individually necessary. This approach makes its reasoning both interpretable and actionable, providing a clear understanding of the underlying dynamics.
- Driver control and awareness: Without maintaining control and awareness, safe merging is not possible, violating safety constraints related to vehicle stability and collision avoidance.
- Vehicle speed within safe limits: Appropriate speed is essential for lawful and safe merging. Deviations from safe speed ranges can violate legal constraints and create unsafe conditions.
Minimal Necessary Sets
Four minimal necessary sets were identified. Each set represents a core condition that cannot be removed without rendering the effect impossible:
- Necessary Set 1: Driver maintains control of the vehicle and is aware of surrounding traffic.
- Necessary Set 2: Vehicle is traveling at a speed that allows for safe merging and adheres to traffic laws regarding merging.
- Necessary Set 3: Sufficient distance from other vehicles to merge safely and no vehicles are overtaking on the right.
- Necessary Set 4: Traffic conditions allow for merging without impeding flow and no sudden obstacles in the merging path.
Minimal Sufficient Sets
Sufficient sets represent combinations of causes that guarantee successful merging. One minimal sufficient set was identified:
- Sufficient Set 1:
- Driver maintains control of the vehicle and is aware of surrounding traffic.
- Vehicle is traveling at a speed that allows for safe merging and adheres to traffic laws regarding merging.
- Sufficient distance from other vehicles to merge safely and no vehicles are overtaking on the right.
- Traffic conditions allow for merging without impeding flow and no sudden obstacles in the merging path.
These findings highlight an important structural property: while some causes are not individually necessary, they become indispensable within certain minimal necessary sets. Moreover, every minimal necessary cause is included within sufficient sets that ensure the effect occurs, illustrating how necessary and sufficient conditions are systematically linked.
#### 5.3.2. Scenario 2: Maintain a Constant Speed on a Highway Segment
Decomposition and Consolidation
Eight candidate causes were initially generated. After deduplication, six unique causes remained:
1. Driver maintains vehicle control and is attentive and responsive to road conditions.
1. Vehicle speed is within legal limits and above minimum required speed.
1. Sufficient friction between tires and road.
1. No obstacles on the highway segment.
1. No sudden changes in traffic conditions.
1. No emergency situations requiring sudden braking.
Individual Necessity Evaluation
Each cause was evaluated individually against safety and legal constraints. The first three were classified as individually necessary:
- Driver control and attentiveness: Without stable control and responsiveness, maintaining constant speed violates vehicle control safety requirements.
- Vehicle speed within limits: Operating outside legal speed bounds violates regulatory constraints and invalidates the effect.
- Sufficient friction: Adequate tire–road friction is required to maintain speed safely and preserve traction.
Minimal Necessary Sets
Three minimal necessary sets were identified, corresponding to the causes that were also individually necessary:
- Necessary Set 1: Driver maintains vehicle control and is attentive and responsive to road conditions.
- Necessary Set 2: Vehicle speed is within legal limits and above minimum required speed.
- Necessary Set 3: Sufficient friction between tires and road.
Minimal Sufficient Sets
Two minimal sufficient sets were identified:
- Sufficient Set 1:
- Driver maintains vehicle control and is attentive and responsive to road conditions.
- Vehicle speed is within legal limits and above minimum required speed.
- Sufficient friction between tires and road.
- No obstacles on the highway segment.
- Sufficient Set 2:
- Driver maintains vehicle control and is attentive and responsive to road conditions.
- Vehicle speed is within legal limits and above minimum required speed.
- Sufficient friction between tires and road.
- No sudden changes in traffic conditions.
These results demonstrate that, while certain causes may not be required on their own to produce the effect, they play a crucial role when combined with other factors. In these sufficient combinations, their presence helps ensure that the effect reliably occurs. This highlights how individual causes can contribute indirectly, supporting the overall outcome even if they are not strictly necessary in isolation.
#### 5.3.3. Symbolic Translation
To illustrate the formal translation step, each unique cause was converted into a symbolic rule for both scenarios using the predefined grammar. The following examples show how natural language conditions are mapped into formally constrained logical representations.
”Driver maintains control of the vehicle”
$$
∀ x(¬ collide(x)← sd\_front(x)∧ sd\_rear(x)∧¬ lane\_change(x))
$$
This rule formalizes vehicle control through safe longitudinal distances (sd) and the absence of destabilizing lane changes, ensuring collision avoidance.
”Sufficient distance from other vehicles to merge safely”
$$
∀ x(sd\_front(x)∧ sd\_rear(x)←¬ dense(x))
$$
Low traffic density implies that safe distances (sd) can be maintained both in front of and behind the vehicle.
These examples demonstrate how rich driving conditions are systematically reduced to formally constrained logical rules within the reasoning framework. A key takeaway is that the LLM can interpret nuanced, context-dependent descriptions and convert them into precise symbolic forms. It effectively bridges human-readable reasoning with formal, machine-interpretable logic, keeping both meaning and structure intact. For a comprehensive presentation of the generated candidate causes, intermediate evaluation steps, full subset analyses, and complete symbolic translations for both scenarios, refer to the Appendix repo2026rulesynthesis, where detailed end-to-end examples of the pipeline execution are provided.
## 6. Discussion
The pipeline provides a structured way to analyze cause & effect relationships in driving scenarios, directly informing how Generative AI can support the synthesis of rules in a principled, traceable manner (RP.1). Each stage contributes unique insights into the reasoning process. The initial decomposition highlights the potential factors that could lead to the effect, ensuring that no obvious candidate cause is missed and that high-level goals are systematically unpacked into concrete rule candidates. De-duplication then reduces redundancy, merging overlapping causes while preserving meaning, which directly addressing the need to minimize ambiguities and redundancies in synthesized rules. This simplifies the reasoning and prevents inflated or repetitive outputs, thereby improving the clarity and manageability of the rule space at scale.
Individual necessity evaluation assesses each cause in isolation and shows which factors are critical on their own, providing a first approximation of how candidate rules relate to system goals (RP.1). However, this step alone cannot capture conditional relationships. Subset evaluation addresses this by considering combinations of causes. Interestingly, some causes initially marked as not necessary were required when combined with other factors. This demonstrates the importance of examining interactions and conditional dependencies rather than relying solely on isolated assessments and shows how rule evaluation must account for contextual dependencies to remain faithful to the desired specified goals (RP.2).
Sufficiency analysis further emphasizes flexible pathways to the effect and operationalizes the search for sufficient and necessary sets of rules that satisfy a given goal (RP.2). Minimal sufficient sets include the necessary causes and may also incorporate additional factors to guarantee the effect. This reflects real-world complexity, where multiple combinations of conditions can produce the same outcome similar to Scenario 2. Some causes that seemed irrelevant individually were shown to be sufficient only in combination, highlighting the subtlety of causal relationships. Together, the necessity and sufficiency analyses provide an incremental and modular way to evaluate rules: incremental, because causes and subsets are assessed stepwise; modular, because minimal sets can be associated with specific goals and reused as distinct rule components (RP.2).
Despite its strengths in addressing RP.1 and RP.2, the approach has limitations. The model functions as a black box, so the internal reasoning is not fully transparent. Moreover, there is a reliance on the predefined set of regulations, which may not cover all possible scenarios. Additionally, the outputs are highly sensitive to how the prompts are formulated, which can influence the adaptability of the model’s responses. These factors constrain the completeness and robustness of the synthesized rule sets and their evaluations and indicate that principled rule synthesis and modular evaluation still depend heavily on the quality and coverage of the underlying knowledge base (RP.1, RP.2).
However, these challenges point toward opportunities for improvement. Expanding the set of rules, introducing probabilistic reasoning, or incorporating multiple model perspectives could enhance robustness. Iterative refinement of prompts and providing feedback to the model can further reduce errors. Such extensions would not only broaden the domain coverage but also strengthen the principled nature of rule synthesis and the reliability of incremental, modular rule evaluation with respect to evolving goals (RP.1, RP.2). Overall, the pipeline demonstrates a form of abductive reasoning. It identifies likely causes, evaluates their necessity and sufficiency, and uncovers conditional dependencies. The structured, stepwise process makes the reasoning traceable and interpretable while capturing complex interactions between factors, thereby providing concrete evidence that LLM-based pipelines can support goal-based, legally and safety-informed rule synthesis (RP.1) and in a systematic, incremental, and modular way (RP.2).
## 7. Conclusion and Future Work
The proposed framework demonstrates how neuro-symbolic causal reasoning, combined with large language models, can support incremental and modular rule synthesis grounded in legal and safety principles. By decomposing high-level goals into candidate causes, consolidating them semantically, translating them into formal rules, and then analyzing necessary and sufficient cause sets, the pipeline yields traceable and interpretable rule sets that capture complex causal interactions in domains such as autonomous driving. The subsequent verification stages—covering syntax and schema checks, logical consistency, and safety and invariant preservation—ensure that only rules compatible with an existing knowledge base and domain constraints are integrated back into the system, thereby strengthening reliability and explainability across the MAPE-K loop. Together, these elements illustrate how abductive and deductive reasoning can be orchestrated to reduce brittleness, improve goal alignment, and provide a principled pathway from natural-language specifications to formally verified rule theories.
In future work, we plan to deepen the integration between causal models and rule synthesis to derive more expressive sets of necessary and sufficient rules, and to broaden the coverage of domain principles beyond the current set of traffic regulations. We also plan to incorporate automated solvers to detect and resolve conflicts between newly synthesized rules and existing knowledge, enabling systematic management of inconsistencies at the theory level. This will support the design of richer feedback loops that jointly exploit formal verification, causal path analysis, and effect estimation, with the goal of informing more robust synthesis, composition, and adaptation strategies in safety-critical, learning-enabled systems.
## References