Enumerating Minimal Unsatisfiable Cores of LTLf formulas

• URL: http://arxiv.org/abs/2409.09485v1
• Date: Sat, 14 Sep 2024 17:15:30 GMT
• Title: Enumerating Minimal Unsatisfiable Cores of LTLf formulas
• Authors: Antonio Ielo, Giuseppe Mazzotta, Rafael Peñaloza, Francesco Ricca,
• Abstract summary: Linear Temporal Logic over finite traces ($textLTL_f$) is a widely used formalism with applications in AI, process mining, model checking, and more. This paper introduces a novel technique for enumerating minimal unsatisfiable cores (MUCs) of an $textLTL_f$ specification.
• Score: 8.650929640364593
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Linear Temporal Logic over finite traces ($\text{LTL}_f$) is a widely used formalism with applications in AI, process mining, model checking, and more. The primary reasoning task for $\text{LTL}_f$ is satisfiability checking; yet, the recent focus on explainable AI has increased interest in analyzing inconsistent formulas, making the enumeration of minimal explanations for infeasibility a relevant task also for $\text{LTL}_f$. This paper introduces a novel technique for enumerating minimal unsatisfiable cores (MUCs) of an $\text{LTL}_f$ specification. The main idea is to encode a $\text{LTL}_f$ formula into an Answer Set Programming (ASP) specification, such that the minimal unsatisfiable subsets (MUSes) of the ASP program directly correspond to the MUCs of the original $\text{LTL}_f$ specification. Leveraging recent advancements in ASP solving yields a MUC enumerator achieving good performance in experiments conducted on established benchmarks from the literature.

Related papers

• ConvexBench: Can LLMs Recognize Convex Functions? [70.53167848190624]
  Convex analysis is a modern branch of mathematics with many applications.<n>As Large Language Models (LLMs) start to automate research-level math and sciences, it is important for LLMs to demonstrate the ability to understand and reason with convexity.<n>We introduce cb, a scalable and mechanically verifiable benchmark for testing textitwhether LLMs can identify the convexity of a symbolic objective under deep functional composition.
  arXiv  Detail & Related papers  (2026-02-01T07:41:17Z)
• $\texttt{SEM-CTRL}$: Semantically Controlled Decoding [53.86639808659575]
  $texttSEM-CTRL$ is a unified approach that enforces rich context-sensitive constraints and task- and instance-specific semantics directly on an LLM decoder. texttSEM-CTRL$ allows small pre-trained LLMs to efficiently outperform larger variants and state-of-the-art reasoning models.
  arXiv  Detail & Related papers  (2025-03-03T18:33:46Z)
• FLARE: Faithful Logic-Aided Reasoning and Exploration [50.9814063216852]
  We introduce a novel approach for traversing the problem space using task decompositions. We use the Large Language Models to plan a solution, soft-formalise the query into facts and predicates using a logic programming code. Our method allows us to compute the faithfulness of the reasoning process w.r.t. the generated code and analyse the steps of the multi-hop search without relying on external solvers.
  arXiv  Detail & Related papers  (2024-10-14T19:39:11Z)
• Benchmarking Uncertainty Quantification Methods for Large Language Models with LM-Polygraph [83.90988015005934]
  Uncertainty quantification (UQ) is a critical component of machine learning (ML) applications. We introduce a novel benchmark that implements a collection of state-of-the-art UQ baselines. We conduct a large-scale empirical investigation of UQ and normalization techniques across nine tasks, and identify the most promising approaches.
  arXiv  Detail & Related papers  (2024-06-21T20:06:31Z)
• Transfer Q Star: Principled Decoding for LLM Alignment [105.89114186982972]
  Transfer $Q*$ estimates the optimal value function for a target reward $r$ through a baseline model. Our approach significantly reduces the sub-optimality gap observed in prior SoTA methods.
  arXiv  Detail & Related papers  (2024-05-30T21:36:12Z)
• Evaluating and Improving Tool-Augmented Computation-Intensive Math Reasoning [75.74103236299477]
  Chain-of-thought prompting(CoT) and tool augmentation have been validated as effective practices for improving large language models. We propose a new approach that can deliberate the reasoning steps with tool interfaces, namely textbfDELI. Experimental results on CARP and six other datasets show that the proposed DELI mostly outperforms competitive baselines.
  arXiv  Detail & Related papers  (2023-06-04T17:02:59Z)
• SatLM: Satisfiability-Aided Language Models Using Declarative Prompting [68.40726892904286]
  We propose a new satisfiability-aided language modeling (SatLM) approach for improving the reasoning capabilities of large language models (LLMs) We use an LLM to generate a declarative task specification rather than an imperative program and leverage an off-the-shelf automated theorem prover to derive the final answer. We evaluate SATLM on 8 different datasets and show that it consistently outperforms program-aided LMs in the imperative paradigm.
  arXiv  Detail & Related papers  (2023-05-16T17:55:51Z)
• A Few Expert Queries Suffices for Sample-Efficient RL with Resets and Linear Value Approximation [16.29514743112387]
  We study sample-efficient Reinforcement Learning (RL) in settings where only the optimal value function is assumed to be linearlyrealizable. We present a statistically and computationally efficient algorithm (Delphi) for blending exploration with expert queries. Delphi requires $tildemathcalO(d)$ expert queries and a $textttpoly(d,|mathcalA|,1/varepsilon)$ amount of exploratory samples to provably recover an $varepsilon$suboptimal policy.
  arXiv  Detail & Related papers  (2022-07-18T01:39:13Z)
• Linear Temporal Logic Modulo Theories over Finite Traces (Extended Version) [72.38188258853155]
  This paper studies Linear Temporal Logic over Finite Traces (LTLf) proposition letters are replaced with first-order formulas interpreted over arbitrary theories. The resulting logic, called Satisfiability Modulo Theories (LTLfMT), is semi-decidable.
  arXiv  Detail & Related papers  (2022-04-28T17:57:33Z)
• Computing unsatisfiable cores for LTLf specifications [3.251765107970636]
  Linear-time temporal logic on finite traces (LTLf) is rapidly becoming a de-facto standard to produce specifications in many application domains. We provide four algorithms for extracting an unsatisfiable core using state-of-the-art approaches to satisfiability checking. The results show the feasibility, effectiveness, and complementarities of the different algorithms and tools.
  arXiv  Detail & Related papers  (2022-03-09T16:08:43Z)
• Learning to extrapolate using continued fractions: Predicting the critical temperature of superconductor materials [5.905364646955811]
  In the field of Artificial Intelligence (AI) and Machine Learning (ML), the approximation of unknown target functions $y=f(mathbfx)$ is a common objective. We refer to $S$ as the training set and aim to identify a low-complexity mathematical model that can effectively approximate this target function for new instances $mathbfx$.
  arXiv  Detail & Related papers  (2020-11-27T04:57:40Z)

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.