检索结果-内蒙古大学图书馆

Automated Theorem Provers Help Improve Large Language Model Reasoning

学校读者我要写书评

暂无评论

arXiv 2024年

作者： McGinness, Lachlan Baumgartner, Peter School of Computer Science Australian National University Data61 CSIRO Australia Data61 CSIRO School of Computer Science Australian National University Australia

In this paper we demonstrate how logic programming systems and Automated first-order logic Theorem Provers (ATPs) can improve the accuracy of Large Language Models (LLMs) for logical reasoning tasks where the baseline performance is given by direct LLM solutions. We first evaluate LLM reasoning on steamroller problems using the PRONTOQA benchmark. We show how accuracy can be improved with a neuro-symbolic architecture where the LLM acts solely as a front-end for translating a given problem into a formal logic language and an automated reasoning engine is called for solving it. However, this approach critically hinges on the correctness of the LLM translation. To assess this translation correctness, we secondly define a framework of syntactic and semantic error categories. We implemented the framework and used it to identify errors that LLMs make in the benchmark domain. Based on these findings, we thirdly extended our method with capabilities for automatically correcting syntactic and semantic errors. For semantic error correction we integrate first-order logic ATPs, which is our main and novel contribution. We demonstrate that this approach reduces semantic errors significantly and further increases the accurracy of LLM logical reasoning. © 2024, CC BY.

关键词： logic programming

Which programming Language and What Features at Pre-training Stage Affect Downstream logical Inference Performance?

学校读者我要写书评

暂无评论

arXiv 2024年

作者： Uchiyama, Fumiya Kojima, Takeshi Gambardella, Andrew Cao, Qi Iwasawa, Yusuke Matsuo, Yutaka The University of Tokyo Japan

Recent large language models (LLMs) have demonstrated remarkable generalization abilities in mathematics and logical reasoning tasks. Prior research indicates that LLMs pre-trained with programming language data exhibit high mathematical and reasoning abilities;however, this causal relationship has not been rigorously tested. Our research aims to verify which programming languages and features during pre-training affect logical inference performance. Specifically, we pre-trained decoder-based language models from scratch using datasets from ten programming languages (e.g., Python, C, Java) and three natural language datasets (Wikipedia, Fineweb, C4) under identical conditions. Thereafter, we evaluated the trained models in a few-shot in-context learning setting on logical reasoning tasks: FLD and bAbi, which do not require commonsense or world knowledge. The results demonstrate that nearly all models trained with programming languages consistently outperform those trained with natural languages, indicating that programming languages contain factors that elicit logic inference performance. In addition, we found that models trained with programming languages exhibit a better ability to follow instructions compared to those trained with natural languages. Further analysis reveals that the depth of Abstract Syntax Trees representing parsed results of programs also affects logical reasoning performance. These findings will offer insights into the essential elements of pre-training for acquiring the foundational abilities of LLMs.1 © 2024, CC BY.

关键词： logic programming

Computation and Complexity of Preference Inference Based on Hierarchical Models

学校读者我要写书评

暂无评论

arXiv 2024年

作者： Wilson, Nic George, Anne-Marie O’Sullivan, Barry Insight Centre for Data Analytics School of Computer Science and IT University College Cork Ireland

Preference Inference involves inferring additional user preferences from elicited or observed preferences, based on assumptions regarding the form of the user’s preference relation. In this paper we consider a situation in which alternatives have an associated vector of costs, each component corresponding to a different criterion, and are compared using a kind of lexicographic order, similar to the way alternatives are compared in a Hierarchical Constraint logic programming model. It is assumed that the user has some (unknown) importance ordering on criteria, and that to compare two alternatives, firstly, the combined cost of each alternative with respect to the most important criteria are compared;only if these combined costs are equal, are the next most important criteria considered. The preference inference problem then consists of determining whether a preference statement can be inferred from a set of input preferences. We show that this problem is coNP-complete, even if one restricts the cardinality of the equal-importance sets to have at most two elements, and one only considers non-strict preferences. However, it is polynomial if it is assumed that the user’s ordering of criteria is a total ordering;it is also polynomial if the sets of equally important criteria are all equivalence classes of a given fixed equivalence relation. We give an efficient polynomial algorithm for these cases, which also throws light on the structure of the inference. © 2024, CC BY.

关键词： logic programming

A Fuzzy Expert System Based Extension of SWI-Prolog for Evaluating AI Ethics

学校读者我要写书评

暂无评论

A Fuzzy Expert System Based Extension of SWI-Prolog for Eval...

International IEEE Conference on Intelligent Systems, IS

作者： Harriet Griffin Mani Ghahremani Alexander Gegov University of Portsmouth Portsmouth England

ISBN: (数字)9798350350982

ISBN: (纸本)9798350350999

The rapid expansion of the AI market has outpaced the development of adequate regulations and guidelines, resulting in deficiencies in tools for practitioners and stakeholders in AI systems (AIS). These guidelines are re-evaluated and re-scoped to emphasise positive ethical design and supporting operationalisation, resulting in an actionable, concrete, and accessible toolkit. The work aims to contribute to the optimisation of SWI-Prolog fuzzy systems extended over a new problem domain. The work further introduces the integration of Explainable AI (XAI) principles within the proposed ethical framework as an extension of current XAI research. A novel fuzzy expert system is presented with a proposed system algorithm, employing SWI-Prolog extended through the Constraint logic programming library for membership function constraint propagation. A Command Line Interface (CLI) is presented for user interaction, with functionality to allow users to store and load data locally.

关键词： Ethics logic programming Regulation Libraries Stakeholders Expert systems Intelligent systems Optimization Guidelines Fuzzy systems

The B2Scala Tool: Integrating Bach in Scala with Security in Mind

学校读者我要写书评

暂无评论

arXiv 2024年

作者： Ouardi, Doha Barkallah, Manel Jacquet, Jean-Marie Nadi Research Institute Faculty of Computer Science University of Namur Namur Belgium

Process algebras have been widely used to verify security protocols in a formal manner. However they mostly focus on synchronous communication based on the exchange of messages. We present an alternative approach relying on asynchronous communication obtained through information available on a shared space. More precisely this paper first proposes an embedding in Scala of a Linda-like language, called Bach. It consists of a Domain Specific Language, internal to Scala, that allows us to experiment programs developed in Bach while benefiting from the Scala eco-system, in particular from its type system as well as program fragments developed in Scala. Moreover, we introduce a logic that allows to restrict the executions of programs to those meeting logic formulae. Our work is illustrated on the Needham-Schroeder security protocol, for which we manage to automatically rediscover the man-in-the-middle attack first put in evidence by G. Lowe. © 2024, CC BY.

关键词： logic programming

On the generalization of learned constraints for ASP solving in temporal domains

学校读者我要写书评

暂无评论

arXiv 2024年

作者： Romero, Javier Schaub, Torsten Strauch, Klaus University of Potsdam Germany

The representation of a temporal problem in ASP usually boils down to using copies of variables and constraints, one for each time stamp, no matter whether it is directly encoded or expressed via an action or temporal language. The multiplication of variables and constraints is commonly done during grounding and the solver is completely ignorant about the temporal relationship among the different instances. On the other hand, a key factor in the performance of today’s ASP solvers is conflict-driven constraint learning. Our question in this paper is whether a constraint learned for particular time steps can be generalized and reused at other time steps, and ultimately whether this enhances the overall solver performance on temporal problems. Knowing well the domain of time, we study conditions under which learned dynamic constraints can be generalized. Notably, we identify a property of temporal representations that enables the generalization of learned constraints across all time steps. It turns out that most ASP planning encodings either satisfy this property or can be easily adapted to do so. In addition, we propose a general translation that transforms programs to fulfill this property. Finally, we empirically evaluate the impact of adding the generalized constraints to an ASP solver. Under consideration in Theory and Practice of logic programming (TPLP) © 2024, CC BY.

关键词： logic programming

Six Ways to Implement Divisibility by Three in miniKanren

学校读者我要写书评

暂无评论

arXiv 2024年

作者： Schreiber, Brett Pfingsten, Brysen Hemann, Jason United States Seton Hall University United States

This paper explores options for implementing the relation n ≡ 0 (mod 3) within miniKanren using miniKanren numbers and its arithmetic suite. We examine different approaches starting from straightforward implementations to more optimized versions. The implementations discussed include brute-force arithmetic methods, divisibility tricks, and derivation from a finite automaton. Our contributions include an in-depth look at the process of implementing a miniKanren relation and observations on benchmarking defrels. This study aims to provide practical insights for miniKanren programmers on both performance and implementation techniques. © 2024, CC BY.

关键词： logic programming

Automated Completion of Statements and Proofs in Synthetic Geometry: An Approach based on Constraint Solving

学校读者我要写书评

暂无评论

arXiv 2024年

作者： Gonzalez, Salwa Tabet Janičić, Predrag Narboux, Julien UMR 7357 CNRS University of Strasbourg Pôle API Bd Sébastien Brant BP 10413 Illkirch67412 France Department for Computer Science Faculty of Mathematics University of Belgrade Studentski trg 16 Belgrade11000 Serbia

Conjecturing and theorem proving are activities at the center of mathematical practice and are difficult to separate. In this paper, we propose a framework for completing incomplete conjectures and incomplete proofs. The framework can turn a conjecture with missing assumptions and with an under-specified goal into a proper theorem. Also, the proposed framework can help in completing a proof sketch into a human-readable and machine-checkable proof. Our approach is focused on synthetic geometry, and uses coherent logic and constraint solving. The proposed approach is uniform for all three kinds of tasks, flexible and, to our knowledge, unique such approach. Copyright © 2024, The Authors. All rights reserved.

关键词： logic programming

Design of Joint Simulation System of Industrial Robot Training Equipment Based on RobotStudio and TIA Portal

学校读者我要写书评

暂无评论

Design of Joint Simulation System of Industrial Robot Traini...

Intelligent Robotics and Systems (ISoIRS), International Symposium on

作者： Li Zhou Liangyou Che Zehao Dong Mingzhang Mo Interdisciplinary Research Institute Guangdong Polytechnic Normal University Guangzhou China Research Institute of Guangdong Polytechnic Normal University in Heyuan City Heyuan China School of Mechatronical Engineering Guangdong Polytechnic Normal University Guangzhou China

ISBN: (数字)9798350364798

ISBN: (纸本)9798350364804

To address the shortage of industrial robotics training equipment in vocational colleges, a collaborative simulation system has been developed to emulate the integrated operations of industrial robots, PLCs, and HMI touchscreens. Centered around the RobotStudio 6.08 and TIA Portal V18 software platforms, this system achieves seamless communication between the platforms by establishing simulation models and configuring the S7-PLCSIM Advanced V5.0 software along with the RSConnectDIOToSnap7 Smart communication component. Through meticulous design of control programs and HMI interfaces, the system has been successfully established as a comprehensive simulation platform for industrial robotics training. Extensive simulation testing and validation have confirmed that this system effectively replicates the dynamic interactions of industrial robots, PLCs, and HMI touchscreens, providing a training experience that closely mirrors that of actual industrial robotics equipment.

关键词： Training Solid modeling Service robots logic programming Touch sensitive screens Industrial robots Software