2024-10-29 | | Total: 9
People increasingly use digital platforms to exchange resources in accordance to some policies stating what resources users offer and what they require in return. In this paper, we propose a formal model of these environments, focussing on how users' policies are defined and enforced, so ensuring that malicious users cannot take advantage of honest ones. To that end, we introduce the declarative policy language MuAC and equip it with a formal semantics. To determine if a resource exchange is fair, i.e., if it respects the MuAC policies in force, we introduce the non-standard logic MuACL that combines non-linear, linear and contractual aspects, and prove it decidable. Notably, the operator for contractual implication of MuACL is not expressible in linear logic. We define a semantics preserving compilation of MuAC policies into MuACL, thus establishing that exchange fairness is reduced to finding a proof in MuACL. Finally, we show how this approach can be put to work on a blockchain to exchange non-fungible tokens.
A process model is called sound if it always terminates properly and each model activity can occur in a process instance. Conducting soundness verification right after process design allows to detect and eliminate design errors in a process to be implemented. Deadlocks, livelocks, and unlimited resource growth are examples of critical design errors that must be addressed before process implementation.However, eliminating such failure points is usually a time-consuming and error-prone task even for modeling experts. This task becomes even more complicated in a data-aware setting when both control and data flows are represented in a model. In this paper, we introduce an algorithm that allows to repair soundness property of data-aware process models, represented as data Petri nets (DPNs), that preserves the correct behavior of the source model. In DPNs, each transition is associated with a guard that includes input and output conditions on process variables.Our algorithm restricts transition guards of a DPN so that executions that previously led to improper termination become prohibited.The algorithm does not require the underlying control flow of the net to be sound and can be applied to the models that have at least one execution leading to the final marking. The algorithm is implemented and results of the preliminary evaluation demonstrate its applicability on process models of moderate sizes.
Formal verification using proof assistants, such as Coq, is an effective way of improving software quality, but it is expensive. Writing proofs manually requires both significant effort and expertise. Recent research has used machine learning to automatically synthesize proofs, reducing verification effort, but these tools are able to prove only a fraction of the desired software properties. We introduce Cobblestone, a new proof-synthesis approach that improves on the state of the art by taking advantage of partial progress in proof synthesis attempts. Unlike prior tools, Cobblestone can produce multiple unsuccessful proofs using a large language model (LLM), identify the working portions of those proofs, and combine them into a single, successful proof, taking advantage of internal partial progress. We evaluate Cobblestone on two benchmarks of open-source Coq projects, controlling for training data leakage in LLM datasets. Fully automatically, Cobblestone can prove 48% of the theorems, while Proverbot9001, the previous state-of-the-art, learning-based, proof-synthesis tool, can prove 17%. Cobblestone establishes a new state of the art for fully automated proof synthesis tools for Coq. We also evaluate Cobblestone in a setting where it is given external partial proof progress from oracles, serving as proxies for a human proof engineer or another tool. When the theorem is broken down into a set of subgoals and Cobblestone is given a set of relevant lemmas already proven in the project, it can prove up to 58% of the theorems. We qualitatively study the theorems Cobblestone is and is not able to prove to outline potential future research directions to further improve proof synthesis, including developing interactive, semi-automated tools. Our research shows that tools can make better use of partial progress made during proof synthesis to more effectively automate formal verification.
Logic programs are a powerful approach for solving NP-Hard problems. However, due to their declarative nature, debugging logic programs poses significant challenges. Unlike procedural paradigms, which allow for step-by-step inspection of program state, logic programs require reasoning about logical statements for fault localization. This complexity is amplified in learning environments due to students' inexperience. We introduce FormHe, a novel tool that combines logic-based techniques and Large Language Models to identify and correct issues in Answer Set Programming submissions. FormHe consists of two components: a fault localization module and a program repair module. First, the fault localizer identifies a set of faulty program statements requiring modification. Subsequently, FormHe employs program mutation techniques and Large Language Models to repair the flawed ASP program. These repairs can then serve as guidance for students to correct their programs. Our experiments with real buggy programs submitted by students show that FormHe accurately detects faults in 94% of cases and successfully repairs 58% of incorrect submissions.
When validated neural networks (NNs) are pruned (and retrained) before deployment, it is desirable to prove that the new NN behaves equivalently to the (original) reference NN. To this end, our paper revisits the idea of differential verification which performs reasoning on differences between NNs: On the one hand, our paper proposes a novel abstract domain for differential verification admitting more efficient reasoning about equivalence. On the other hand, we investigate empirically and theoretically which equivalence properties are (not) efficiently solved using differential reasoning. Based on the gained insights, and following a recent line of work on confidence-based verification, we propose a novel equivalence property that is amenable to Differential Verification while providing guarantees for large parts of the input space instead of small-scale guarantees constructed w.r.t. predetermined input points. We implement our approach in a new tool called VeryDiff and perform an extensive evaluation on numerous old and new benchmark families, including new pruned NNs for particle jet classification in the context of CERN's LHC where we observe median speedups >300x over the State-of-the-Art verifier alpha,beta-CROWN.
With the rapid growth of social media usage, a common trend has emerged where users often make sarcastic comments on posts. While sarcasm can sometimes be harmless, it can blur the line with cyberbullying, especially when used in negative or harmful contexts. This growing issue has been exacerbated by the anonymity and vast reach of the internet, making cyberbullying a significant concern on platforms like Reddit. Our research focuses on distinguishing cyberbullying from sarcasm, particularly where online language nuances make it difficult to discern harmful intent. This study proposes a framework using natural language processing (NLP) and machine learning to differentiate between the two, addressing the limitations of traditional sentiment analysis in detecting nuanced behaviors. By analyzing a custom dataset scraped from Reddit, we achieved a 95.15% accuracy in distinguishing harmful content from sarcasm. Our findings also reveal that teenagers and minority groups are particularly vulnerable to cyberbullying. Additionally, our research uncovers coordinated graphs of groups involved in cyberbullying, identifying common patterns in their behavior. This research contributes to improving detection capabilities for safer online communities.
Many uncontrollable disease outbreaks of the past exposed several vulnerabilities in the healthcare systems worldwide. While advancements in technology assisted in the rapid creation of the vaccinations, there needs to be a pressing focus on the prevention and prediction of such massive outbreaks. Early detection and intervention of an outbreak can drastically reduce its impact on public health while also making the healthcare system more resilient. The complexity of disease transmission dynamics, influence of various directly and indirectly related factors and limitations of traditional approaches are the main bottlenecks in taking preventive actions. Specifically, this paper implements deep learning algorithms and LLM's to predict the severity of infectious disease outbreaks. Utilizing the historic data of several diseases that have spread in India and the climatic data spanning the past decade, the insights from our research aim to assist in creating a robust predictive system for any outbreaks in the future.
This proceedings contains abstracts and position papers for the work to be presented at the fourth Logic and Practice of Programming (LPOP) Workshop. The workshop is to be held in Dallas, Texas, USA, and as a hybrid event, on October 13, 2024, in conjunction with the 40th International Conference on Logic Programming (ICLP). The focus of this workshop is integrating reasoning systems for trustworthy AI, especially including integrating diverse models of programming with rules and constraints.
In the past few years, Large Language Models (LLMs) have exploded in usefulness and popularity for code generation tasks. However, LLMs still struggle with accuracy and are unsuitable for high-risk applications without additional oversight and verification. In particular, they perform poorly at generating code for highly complex systems, especially with unusual or out-of-sample logic. For such systems, verifying the code generated by the LLM may take longer than writing it by hand. We introduce a solution that divides the code generation into two parts; one to be handled by an LLM and one to be handled by formal methods-based program synthesis. We develop a benchmark to test our solution and show that our method allows the pipeline to solve problems previously intractable for LLM code generation.