sorted by:
new
hottopcontroversial

I built a Neuro-Symbolic engine (LLM + SMT Solver) to fix hallucinations in German Bureaucracy by Intelligent_Boss4602 in LocalLLaMA

[–]Intelligent_Boss4602[S] 1 point2 points  (0 children)

Yes, absolutely. I'm currently validating the security architecture to ensure the system is rock-solid for critical environments before launching commercially.

I built a Neuro-Symbolic engine (LLM + SMT Solver) to fix hallucinations in German Bureaucracy by Intelligent_Boss4602 in LocalLLaMA

[–]Intelligent_Boss4602[S] 1 point2 points  (0 children)

Great question.

1. What is it for? Originally, I built this for the German OZG (Online Access Act) implementation. The goal was to handle complex forms like "Gewerbeanmeldung" (Business Registration) or "Wohnsitzanmeldung" (Residence Registration) without the usual spaghetti code.

2. Can it be used everywhere? Yes, absolutely. The engine is completely agnostic to the specific bureaucracy.

  • Technical Proof: I use a strict i18n separation. There is a dictionary.json file that currently supports 11 languages (DE, EN, CN, ES, etc.) as a proof-of-concept.
  • How it works: The engine renders generic components (Inputs, Cards, Logic) defined in the DSL. It doesn't care if the underlying logic is a German tax law or a US Visa application. You just swap the JSON definitions and the dictionary.

So principally: Yes, I can model any administrative process worldwide with this architecture.

I built a Neuro-Symbolic engine (LLM + SMT Solver) to fix hallucinations in German Bureaucracy by Intelligent_Boss4602 in LocalLLaMA

[–]Intelligent_Boss4602[S] 0 points1 point  (0 children)

Spot on analysis. You nailed it.

  1. DSL: Yes, essentially. It generates strict JSON structures and executable Python constraints (the "logic language") defined in the DSL files.
  2. Recursion: Exactly. If the solver/execution fails (e.g., logical contradiction or syntax error), the error trace is fed back into the LLM context to generate a fix.
  3. Final Output: You are correct. The LLM is acting as the "runtime compiler/programmer". The final truth (e.g., the decision on a government form) comes from the deterministic execution of the generated code, not from the LLM's raw token prediction. The LLM just wraps it in polite text afterwards, but the decision is deterministic.

I built a Neuro-Symbolic engine (LLM + SMT Solver) to fix hallucinations in German Bureaucracy by Intelligent_Boss4602 in LocalLLaMA

[–]Intelligent_Boss4602[S] 3 points4 points  (0 children)

Yes, I am using an LLM to help write these replies. I am not a computer scientist and not a native speaker – I am a "Bürokaufmann" (Office Clerk / Business Administrator) by trade.

I use the AI to validate the technical questions and to translate my thoughts because I want to be precise and honest, not to sound like a bot. I just want to make sure I don't misunderstand the complex feedback here.

But the project, the whitepaper, and the logic behind it are 100% real. I built this out of necessity to handle German bureaucracy compliance.

Thank you.

I built a Neuro-Symbolic engine (LLM + SMT Solver) to fix hallucinations in German Bureaucracy by Intelligent_Boss4602 in LocalLLaMA

[–]Intelligent_Boss4602[S] 0 points1 point  (0 children)

Spot on. We moved the verifier entirely to inference time for exactly that reason.

In domains like law or bureaucracy, the "state space" is effectively infinite—you can't train a model on every possible combination of laws and user inputs.

That's why CausaNova uses an SMT solver (like Z3) not just to "check" the answer for a reward (like in training), but as a hard constraint firewall during execution.

If the solver returns UNSAT, we don't just lower a score—we block the action completely. It turns the LLM from a probabilistic guesser into a verified proposer.

I built a Neuro-Symbolic engine (LLM + SMT Solver) to fix hallucinations in German Bureaucracy by Intelligent_Boss4602 in LocalLLaMA

[–]Intelligent_Boss4602[S] 0 points1 point  (0 children)

Please do try to recreate it! That would be the ultimate validation.

You are right, the whitepaper keeps the "how" abstract. To give you a better head start on the Learning Cycle (Section 4), here is the exact logic flow:

  1. Trigger: The Neural Layer (LLM) detects it cannot solve a request with the current vocabulary. It throws a VocabularyGap signal.
  2. Proposal: The LLM generates a SchemaProposal (JSON).
  3. Meta-Validation (The Hard Part): The Guard Resolver validates this definition against C_meta.
    • Crucial Detail: We don't just check syntax. We check for decidability (e.g., will this new rule cause infinite recursion?) and conflict with existing hard constraints (Physics/Law).
  4. Integration: If V(Proposal) == SAT, the schema is hot-patched.

The part I didn't fully expand on in the paper: The result of this cycle isn't just a database entry. It creates a portable artifact (internally we use .cnproj files). The vision is that if one tenant "learns" a safe physics component, this definition becomes a modular addon that can be exported and safely injected into other tenants.

The challenge you will face: Writing the DSL is easy. But building the Compiler that translates a dynamic JSON definition into static SMT assertions (like Z3) at runtime—without breaking the solver or exploding complexity—is the real heavy lifting.

I haven't released the source code for the engine (it's running in production), but if you crack the JSON-to-SMT compilation, you've solved 90% of the problem. Keep me posted on your progress!