Xuan-Bach Le

Abstract:

Multi-intent detection and slot filling are fundamental tasks of natural language understanding in task-oriented dialog systems. Early approaches treated them as separate tasks, which undermines the direct connection between intents and their associated slots. This limitation becomes more pronounced when multiple intents are expressed within a single utterance.

In the Vietnamese language landscape, research on this topic remains limited, largely due to its low-resource status. To address this gap, we introduce VSLIM, a joint model designed for multi-intent detection and slot filling in Vietnamese. Inspired by the SLIM framework, VSLIM builds on its foundation with a biaffine classifier that more directly captures the relationship between intents and slots. This design allows the model to better understand and represent the dependencies across sequence labels in multi-intent settings.

Experiments on the Vietnamese PhoATIS dataset and our newly introduced VPED corpus show that VSLIM outperforms strong NLU baselines, highlighting its potential for improving Vietnamese task-oriented dialog systems. Code & Data: https://github.com/dongphong543/VSLIM

Keywords: Multi-intent detection, Slot filling, Vietnamese language understanding, Joint learning, Explicit mapping

Abstract:

While Retrieval-Augmented Generation (RAG) pipelines often demonstrate strong performance in general settings, they struggle with legal texts, where interpreting structure and relationships between laws is crucial. To address this, we introduce SBV-LawGraph – a dual-retrieval framework designed specifically for Vietnamese legal documents.

It combines semantic retrieval with graph-based reasoning by integrating two modules: a Legal Retrieval module using sparse–dense reranking for textual accuracy, and a Relationship Retrieval module that traverses a curated Legal Knowledge Graph to capture links such as amendments, citations, and definitions.

This design enables SBV-LawGraph to generate responses that are not only relevant but also structurally grounded, addressing limitations of standard RAG systems. Evaluations on the ALQAC2025 and SBV Legal Questions datasets show it consistently outperforms strong baselines, highlighting its effectiveness for precise and explainable legal QA.

Keywords: Retrieval-Augmented Generation, Knowledge Graph, Natural Language Processing, Question-Answering Systems

Abstract:

Linear Temporal Logic (LTL) and, more generally, ω-regular objectives are alternatives to traditional discount-sum and average-reward objectives in reinforcement learning (RL), offering improved comprehensibility and explainability.

In this work, we study the relationship between these objectives. Our main result shows that each RL problem with ω-regular objectives can be reduced to a limit-average reward problem in an optimality-preserving manner via finite-memory reward machines.

Furthermore, we demonstrate the efficacy of this approach by showing that optimal policies for limit-average problems can be found asymptotically by solving a sequence of discount-sum problems approximately. Consequently, we resolve an open problem: optimal policies for LTL and ω-regular objectives can be learned asymptotically.

Abstract:

Quantum programs are not only complicated to design but also challenging to verify, as quantum states can have exponential size and require sophisticated mathematics to encode and manipulate. To address the state-space explosion problem in quantum reasoning, we propose a Hoare-style inference framework that supports local reasoning for quantum programs.

By providing a quantum interpretation of the separating conjunction, we integrate separation logic into our framework and enable local reasoning via a quantum frame rule analogous to the classical frame rule.

For evaluation, we apply our framework to verify representative quantum programs, including Deutsch–Jozsa's algorithm and Grover's algorithm.

Abstract:

Rely-Guarantee is a comprehensive technique that supports compositional reasoning for concurrent programs. However, specifying the Rely condition—environment interference—and the Guarantee condition—local transformation of thread state—remains challenging, making their construction a major bottleneck in automation.

To address this problem, we propose a verification framework that constructs correctness proofs for concurrent programs by automatically inferring suitable Rely-Guarantee conditions. Our framework first builds a Hoare-style sequential proof for each thread, and then applies abstraction refinement to lift these proofs into concurrent ones with appropriate Rely-Guarantee relations.

Experimental results demonstrate that our approach efficiently proves the correctness of multi-threaded programs.

Keywords: Rely-Guarantee, Concurrency, CEGAR

Abstract:

Monadic decomposability — the ability to determine whether a formula in a given logical theory can be decomposed into a Boolean combination of monadic formulas — is a powerful tool for devising decision procedures. In this paper, we revisit a classical decision problem in automata theory: given a regular (synchronized rational) relation, determine whether it is recognizable, i.e., whether it admits a monadic decomposition as a Boolean combination of Cartesian products of regular languages.

Regular relations are highly expressive and, under suitable encodings, capture relations definable in Presburger Arithmetic. Their expressive power coincides with relations definable in universal automatic structures, equivalently those definable by finite set interpretations in WS1S (Weak Second Order Theory of One Successor).

While decidability of this problem was known (and exponential time for binary relations), its exact complexity remained open. Our main contribution is to fully settle the complexity of this decision problem by developing new techniques based on infinite Ramsey theory. We show that the problem is NLOGSPACE-complete for DFA representations and PSPACE-complete for NFA representations of regular relations.

Abstract:

The tree share structure proposed by Dockins et al. provides an elegant model for tracking disjoint ownership in concurrent separation logic. However, decision procedures for tree shares are difficult to implement due to the lack of a systematic theoretical study.

We show that the first-order theory of the full Boolean algebra of tree shares (with all tree-share constants) is decidable and has the same complexity as the first-order theory of Countable Atomless Boolean Algebras.

We further prove that combining this additive structure with a constant-restricted unary multiplicative "relativization" operator yields a non-elementary lower bound. We analyze the source of this lower bound and demonstrate that it arises from the interaction between the two theories, by establishing an upper bound for a generalization of the restricted multiplicative theory in isolation.

Abstract:

Resource sharing is a fundamental phenomenon in concurrent programming, where multiple threads hold permissions to access a common resource. Verification logics must therefore capture permission ownership and transfer.

A common approach is to use rational numbers in $(0,1]$ as permissions, where 1 represents full permission and fractional values represent partial ownership. However, rational permissions are not a natural fit for separation logic, as they weaken its essential notion of disjointness.

We propose a general logical framework that supports permission reasoning in separation logic while preserving disjointness. Our framework enables sophisticated verification tasks such as induction over heap finiteness within the object logic, biabductive inference, and proofs of precision for recursive predicates within the object logic.

We introduce scaling separation algebras, a compositional extension of separation algebras, to model our logic and construct a concrete semantic model. We also developed the ShareInfer tool to benchmark our techniques.

Abstract:

We develop a certified decision procedure for reasoning about systems of equations over the "tree share" fractional permission model of Dockins et al. Fractional permissions provide a principled way to reason about shared ownership of resources, particularly in concurrent programs.

We formally verified our decision procedure and integrated it into the HIP/SLEEK verification system. During integration, we discovered bugs in both the previous uncertified decision procedure and HIP/SLEEK itself.

Beyond certification, our new procedure improves prior work by correctly handling negative clauses and achieving better performance.

Abstract:

Fractional share models are used to reason about how multiple actors share ownership of resources. We study the decidability and complexity of reasoning over the tree share model of Dockins et al. using first-order logic and its fragments.

We identify a connection between the basic Boolean operations on trees — union (t), intersection (u), and complement — and countable atomless Boolean algebras. This connection allows us to establish decidability results with precise complexity bounds for both the full first-order theory and its existential fragment over the tree share model with these operations.

We further relate the multiplication operation (bowtie) on trees to the theory of word equations, deriving decidability for its existential theory and undecidability for its full first-order theory.

Finally, we show that the full first-order theory over the model combining Boolean operations with restricted multiplication (./ with constants on the right-hand side) remains decidable via an embedding into tree-automatic structures.

Abstract:

Fractional permissions enable sophisticated management of resource access in both sequential and concurrent programs. Entailment checkers for separation logic formulas containing fractional permissions must therefore reason precisely about such permissions.

We show how entailment checkers for separation logic with fractional permissions can extract equation systems over fractional shares. We develop a set of decision procedures for equations arising from the sophisticated Boolean binary tree fractional permission model of Dockins et al.

We prove that our procedures are sound and complete and analyze their computational complexity. We describe our implementation, provide performance benchmarks, and detail its integration into the HIP/SLEEK verification toolset. Our results are supported by machine-checked proofs in Coq.