Al-Ghasali：用有限状态自动机约束 LLM 模拟伊斯兰教法裁决
Al-Ghasali: A Computational Framework for Simulating Islamic Jurisprudential Rulings via Finite State Automata and Large Language Models
搞约束解码或神经符号结合的人可以看这篇：作者把教法规则编译成有限状态自动机，再用文法约束解码管住 LLM，数学证明能彻底消除决策性幻觉。思路对任何需要 LLM 严格按规则输出、不能瞎编结论的场景都有参考价值。
一篇 arXiv 论文提出 Al-Ghasali 框架，证明封闭 Fiqh（伊斯兰教法）章节的语义可完全坍缩为确定性有限状态自动机（FSA），并建立形式化计算层级：只要形式化限定在有限命题 Horn 理论内，离线编译后即可保证可判定性与 O(1) 常数时间的裁决提取。
架构上，确定性 FSA 严格控制概率性 LLM：系统从 FSA 执行历史动态构造无歧义的右线性文法，通过 Grammar Guided Constrained Decoding 机制约束解码，配合 Bounded Neutral Lexicon 与 Valence Locking。论文给出 FSA-LLM 集成的充分设计安全条件，确保输出不越过 Usul al Fiqh 的认识论边界，并数学证明该架构可消除裁决性幻觉、教法事实性幻觉与语义反转。
对从事 RAG、约束解码或神经符号系统的开发者，这篇论文提供了一个可借鉴的范式：把 LLM 降格为确定性事实的纯语言变换器，而非决策者。Tartib（顺序）等时序教法要求被确定性展平为静态本体状态，保留自动机的无记忆性质，层级组合的子章节 FSA 仍保持 O(1) 复杂度。
Al-Ghasali: A Computational Framework for Simulating Islamic Jurisprudential Rulings via Finite State Automata and Large Language Models
This paper presents Al Ghasali, a computational framework designed to formalize and simulate Islamic jurisprudential (Fiqh) rulings. Building upon recent set theoretic formalizations of al sabr wa al Taqsim that extract minimal operational rules as simple Horn clause logical programs, this work proves that the semantics of closed Fiqh chapters collapse completely to deterministic Finite State Automata (FSA). We establish a formal computational hierarchy, demonstrating that restricting formalization to finite propositional Horn theories guarantees decidability and constant time (O(1)) verdict extraction after offline compilation. The framework formally proves that hierarchical compositions of sub-chapter FSAs preserve this O(1) complexity, and that temporal juristic requirements, such as Tartib (order), are deterministically flattened into static ontological states, preserving the memoryless property of the automaton. To generate human-readable juristic summaries, Al Ghasali incorporates Large Language Models (LLMs) via an architecture where the deterministic FSA strictly controls the probabilistic LLM. Crucially, the paper formulates sufficient design safety conditions for this FSA LLM integration, ensuring strict adherence to the epistemological boundaries of Usul al Fiqh. To neutralize the risk of LLM hallucination, the system employs a Grammar Guided Constrained Decoding mechanism. We formally define the mapping function that dynamically constructs unambiguous right linear grammars from the FSA execution history. The paper mathematically proves that this architecture, augmented by a Bounded Neutral Lexicon and Valence Locking, guarantees the absolute absence of Decisional Hallucination, Juristic Factual Hallucination, and Semantic Inversion reducing the LLM to a pure linguistic transformer of deterministic juristic facts
This report is categorized under AITOP's "Papers" desk. Within our cross-regional analytical framework, it directly maps to AI developer toolchains, coding agents, and engineering workflows. Key entities and technical topics under continuous tracking include LLM, 约束解码, 神经符号, 形式化验证.
Source attribution: curated from arXiv cs.AI (@Elnaserledinellah Mahmoud Abdelwahab).