Peter Baumgartner 0001

LPAR Conference 2024 Conference Paper

Automated Theorem Provers Help Improve Large Language Model Reasoning

• Lachlan McGinness
• Peter Baumgartner 0001

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 PRON- TOQA benchmark. We show how accuracy can be improved with a neuro-symbolic ar- chitecture 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. How- ever, 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 er- ror 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 contribu- tion. We demonstrate that this approach reduces semantic errors significantly and further increases the accurracy of LLM logical reasoning.

LPAR Conference 2013 Conference Paper

Proving Infinite Satisfiability

• Peter Baumgartner 0001
• Joshua Bax

Abstract We consider the problem of automatically disproving invalid conjectures over data structures such as lists and arrays over integers, in the presence of additional hypotheses over these data structures. We investigate a simple approach based on refutational theorem proving. We assume that the data structure axioms are satisfiable and provide a template language for additional hypotheses such that satisfiability is preserved. Then disproving is done by proving that the negated conjecture follows. By means of examples we demonstrate that our template language is reasonably expressive and that our approach works well with current theorem provers (Z3, SPASS+T and Beagle).

LPAR Conference 2012 Conference Paper

The TPTP Typed First-Order Form with Arithmetic

• Geoff Sutcliffe
• Stephan Schulz 0001
• Koen Claessen
• Peter Baumgartner 0001

Abstract The TPTP World is a well established infrastructure supporting research, development, and deployment of Automated Theorem Proving systems. Recently, the TPTP World has been extended to include a typed first-order logic, which in turn has enabled the integration of arithmetic. This paper describes these developments.

LPAR Conference 2008 Conference Paper

(LIA) - Model Evolution with Linear Integer Arithmetic Constraints

• Peter Baumgartner 0001
• Alexander Fuchs 0003
• Cesare Tinelli

Abstract Many applications of automated deduction require reasoning modulo some form of integer arithmetic. Unfortunately, theory reasoning support for the integers in current theorem provers is sometimes too weak for practical purposes. In this paper we propose a novel calculus for a large fragment of first-order logic modulo Linear Integer Arithmetic (LIA) that overcomes several limitations of existing theory reasoning approaches. The new calculus — based on the Model Evolution calculus, a first-order logic version of the propositional DPLL procedure — supports restricted quantifiers, requires only a decision procedure for LIA-validity instead of a complete LIA-unification procedure, and is amenable to strong redundancy criteria. We present a basic version of the calculus and prove it sound and (refutationally) complete.

LPAR Conference 2006 Conference Paper

Lemma Learning in the Model Evolution Calculus

• Peter Baumgartner 0001
• Alexander Fuchs 0003
• Cesare Tinelli

Abstract The Model Evolution \(\mathcal{ME}\) Calculus is a proper lifting to first-order logic of the DPLL procedure, a backtracking search procedure for propositional satisfiability. Like DPLL, the ME calculus is based on the idea of incrementally building a model of the input formula by alternating constraint propagation steps with non-deterministic decision steps. One of the major conceptual improvements over basic DPLL is lemma learning, a mechanism for generating new formulae that prevent later in the search combinations of decision steps guaranteed to lead to failure. We introduce two lemma generation methods for \(\mathcal{ME}\) proof procedures, with various degrees of power, effectiveness in reducing search, and computational overhead. Even if formally correct, each of these methods presents complications that do not exist at the propositional level but need to be addressed for learning to be effective in practice for \(\mathcal{ME}\). We discuss some of these issues and present initial experimental results on the performance of an implementation of the two learning procedures within our \(\mathcal{ME}\) prover Darwin.

JELIA Conference 2004 Conference Paper

Logic Programming Infrastructure for Inferences on FrameNet

• Peter Baumgartner 0001
• Aljoscha Burchardt

Abstract The growing size of electronically available text corpora like companies’ intranets or the WWW has made information access a hot topic within Computational Linguistics. Despite the success of statistical or keyword based methods, deeper Knowledge Representation (KR) techniques along with “inference” are often mentioned as mandatory, e. g. within the Semantic Web context, to enable e. g. better query answering based on “semantical” information. In this paper we try to contribute to the open question how to operationalize semantic information on a larger scale. As a basis we take the frame structures of the Berkeley FrameNet II project, which is a structured dictionary to explain the meaning of words from a lexicographic perspective. Our main contribution is a transformation of the FrameNet II frames into the answer set programming paradigm of logic programming. Because a number of different reasoning tasks are subsumed under “inference” in the context of natural language processing, we emphasize the flexibility of our transformation. Together with methods for automatic annotation of text documents with frame semantics which are currently developed at various sites, we arrive at an infrastructure that supports experimentation with semantic information access as is currently demanded for.

ECAI Conference 1994 Conference Paper

Refinements of Theory Model Elimination and a Variant without Contrapositives

• Peter Baumgartner 0001

LPAR Conference 1992 Conference Paper

An Order Theory Resolution Calculus

• Peter Baumgartner 0001

Abstract In this paper we present an ordered theory resolution calculus and prove its completeness. Theory reasoning means to relieve a calculus from explicitly drawing inferences in a given theory by special purpose inference rules (e. g. E-resolution for equality reasoning). We take advantage of orderings (e. g. simplification orderings) by disallowing to resolve upon clauses which violate certain maximality constraints; stated positively, a resolvent may only be built if all the selected literals are maximal in their clauses. By this technique the search space is drastically pruned. As an instantiation for theory reasoning we show that equality can be built in by rigid E-unification.