Published papers

Research in AI using Large-Language Models (LLMs) is rapidly evolving, and the comparison of their performance with human reasoning has become a key concern. Prior studies have indicated that LLMs and humans share similar biases, such as dismissing logically valid inferences that contradict common beliefs. However, criticizing LLMs for these biases might be unfair, considering our reasoning not only involves formal deduction but also abduction, which draws tentative conclusions from limited information. Abduction can be regarded as the inverse form of syllogism in its basic structure, that is, a process of drawing a minor premise from a major premise and conclusion. This paper explores the accuracy of LLMs in abductive reasoning by converting a syllogistic dataset into one suitable for abduction. It aims to investigate whether the state-of-the-art LLMs exhibit biases in abduction and to identify potential areas for improvement, emphasizing the importance of contextualized reasoning beyond formal deduction. This investigation is vital for advancing the understanding and application of LLMs in complex reasoning tasks, offering insights into bridging the gap between machine and human cognition.

As large language models (LLMs) advance in linguistic competence, their reasoning abilities are gaining increasing attention. In humans, reasoning often performs well in domain specific settings, particularly in normative rather than purely formal contexts. Although prior studies have compared LLM and human reasoning, the domain specificity of LLM reasoning remains underexplored. In this study, we introduce a new Wason Selection Task dataset that explicitly encodes deontic modality to systematically distinguish deontic from descriptive conditionals, and use it to examine LLMs' conditional reasoning under deontic rules. We further analyze whether observed error patterns are better explained by confirmation bias (a tendency to seek rule-supporting evidence) or by matching bias (a tendency to ignore negation and select items that lexically match elements of the rule). Results show that, like humans, LLMs reason better with deontic rules and display matching-bias-like errors. Together, these findings suggest that the performance of LLMs varies systematically across rule types and that their error patterns can parallel well-known human biases in this paradigm.

This paper investigates whether current large language models exhibit biases in logical reasoning, similar to humans. Specifically, we focus on syllogistic reasoning, a well-studied form of inference in the cognitive science of human deduction. To facilitate our analysis, we introduce a dataset called NeuBAROCO, originally designed for psychological experiments that assess human logical abilities in syllogistic reasoning. The dataset consists of syllogistic inferences in both English and Japanese. We examine three types of biases observed in human syllogistic reasoning: belief biases, conversion errors, and atmosphere effects. Our findings demonstrate that current large language models struggle more with problems involving these three types of biases.

This paper explores the question of how accurately current large language models can perform logical reasoning in natural language, with an emphasis on whether these models exhibit reasoning biases similar to humans. Specifically, our study focuses on syllogistic reasoning, a form of deductive reasoning extensively studied in cognitive science as a natural form of human reasoning. We present a syllogism dataset called NeuBAROCO, which consists of syllogistic reasoning problems in English and Japanese. This dataset was originally designed for psychological experiments to assess human reasoning capabilities using various forms of syllogisms. Our experiments with leading large language models indicate that these models exhibit reasoning biases similar to humans, along with other error tendencies. Notably, there is significant room for improvement in reasoning problems where the relationship between premises and hypotheses is neither entailment nor contradiction. We also present experimental results and in-depth analysis using a new Chain-of-Thought prompting method, which asks LLMs to translate syllogisms into abstract logical expressions and then explain their reasoning process. Our analysis using this method suggests that the primary limitations of LLMs lie in the reasoning process itself rather than the interpretation of syllogisms.

We present a new semantics for first-order conditional logic, which is a generalization of that of Friedman, Halpern and Koller [7]. We utilize Fitting’s embedding of first-order classical logic in first-order S4 to define our semantics. We explain our semantics by showing how it works on the connective expressing “typically implies”. We argue that it has a number of good properties, in particular, it is more adjustable to special situations than that of [7]. For example, we can make sense of nested conditional implications even when a conditional implication does not necessarily hold on the entire set of possible worlds, but where-ever it is satisfied, the conclusion is typically satisfied.

Our previous research, aimed at improving the design of multi-attribute tables (such as product catalogs), found that black-and-white graphics aided decision-making more than numerical or textual formats (Ideno et al., Diagrams 2020). We extended these findings by examining how combining graphic and numerical presentation (highlighting the cells with superior values) influences decision-making. Twenty-one participants chose the most desirable digital cameras from five alternatives. Results showed faster decision-making with highlighted cells compared to non-highlighted ones. A two-stage decision strategy emerged, with more attribute-based gaze shifts initially and equal vertical and horizontal shifts later. We discussed the implications and prospects of highlighted multi-attribute tables.

In recent years, research on large language models (LLMs) has been advancing rapidly, making the evaluation of their reasoning abilities a crucial issue. Within cognitive science, there has been extensive research on human reasoning biases. It is widely observed that humans often use graphical representations as auxiliary tools during inference processes to avoid reasoning biases. However, currently, the evaluation of LLMs’ reasoning abilities has largely focused on linguistic inferences, with insufficient attention given to inferences using diagrams. In this study, we concentrate on syllogisms, a basic form of logical reasoning, and evaluate the reasoning abilities of LLMs supplemented by Euler diagrams. We systematically investigate how accurately LLMs can perform logical reasoning when using diagrams as auxiliary input and whether they exhibit similar reasoning biases to those of humans. Our findings indicate that, overall, providing diagrams as auxiliary input tends to improve models’ performance, including in problems that show reasoning biases, but the effect varies depending on the conditions, and the improvement in accuracy is not as high as that seen in humans. We present results from experiments conducted under multiple conditions, including a Chain-of-Thought setting, to highlight where there is room to improve logical diagrammatic reasoning abilities of LLMs.

There have been some important methods of combining a recursive path ordering and Tait-Girard’s computability argument to provide an ordering for termination proofs of higher-order rewrite systems. The higher-order recursive path ordering HORPO by Jouannaud and Rubio and the computability path ordering CPO by Blanqui, Jouannaud and Rubio are examples of such an ordering. In this paper, we give a case study of yet another direction of such extension of recursive path ordering, avoiding Tait-Girard’s computability method plugged in the above mentioned works. This motivation comes from Lévy’s question in the RTA open problem 19, which asks for a reasonably straightforward interpretation of simply typed λ -calculus λ in a certain well founded ordering. As in the cases of HORPO and CPO, the addition of λ -abstraction and application into path orderings might be considered as one solution, but the following question still remains; can the termination of λ be proved by an interpretation in a first-order well founded ordering in the sense that λ -abstraction/application are not directly built in the ordering? Reconsidering one of Howard’s works on proof-theoretic studies, we introduce the path ordering with Howard algebra as a case study towards further studies on Lévy’s question. → →

© M. Okada & Y. Takahashi. The purposes of this note are the following two; we first generalize Okada-Takeuti’s well quasi ordinal diagram theory, utilizing the recent result of Dershowitz-Tzameret’s version of tree embedding theorem with gap conditions. Second, we discuss possible use of such strong ordinal notation systems for the purpose of a typical traditional termination proof method for term rewriting systems, especially for second-order (pattern-matching-based) rewriting systems including a rewrite-theoretic version of Buchholz’s hydra game.

© 2019 Copyright held by the owner/author(s). In recent years, a new approach has been developed for verifying security protocols with the aim of combining the benefits of symbolic attackers and the benefits of unconditional soundness: the technique of the computationally complete symbolic attacker of Bana and Comon (BC) [8]. In this article, we argue that the real breakthrough of this technique is the recent introduction of its version for indistinguishability [9], because, with the extensions we introduce here, for the first time, there is a computationally sound symbolic technique that is syntactically strikingly simple, to which translating standard computational security notions is a straightforward matter, and that can be effectively used for verification of not only equivalence properties but trace properties of protocols as well. We first fully develop the core elements of this newer version by introducing several new axioms. We illustrate the power and the diverse use of the introduced axioms on simple examples first. We introduce an axiom expressing the Decisional Diffie-Hellman property. We analyze the Diffie-Hellman key exchange, both in its simplest form and an authenticated version as well. We provide computationally sound verification of real-or-random secrecy of the Diffie-Hellman key exchange protocol formultiple sessions, without any restrictions on the computational implementation other than the DDH assumption. We also show authentication for a simplified version of the station-to-station protocol using UF-CMA assumption for digital signatures. Finally, we axiomatize IND-CPA, IND-CCA1, and IND-CCA2 security properties and illustrate their usage. We have formalized the axiomatic system in an interactive theorem prover, Coq, and have machine-checked the proofs of various auxiliary theorems and security properties of Diffie-Hellman and station-to-station protocol.

© The Author(s) 2020. The Keio Twin Research Center (KoTReC) was established in 2009 at Keio University to combine two longitudinal cohort projects - the Keio Twin Study (KTS) for adolescence and adulthood and the Tokyo Twin Cohort Project (ToTCoP) for infancy and childhood. KoTReC also conducted a two-time panel study of self-control and psychopathology in twin adolescence in 2012 and 2013 and three independent anonymous cross-sectional twin surveys (ToTcross) before 2012 - the ToTCross, the Junior and Senior High School Survey and the High School Survey. This article introduces the recent research designs of KoTReC and its publications.

Hilbert remarked in the introductory part of his most famous finitism address (1925 [1]) that “[t]he infinite divisibility of a continuum is an operation that is present only in our thought”, which means that no natural event or matter is infinitely divisible in reality. We recall that Scedrov’s group including the author started logical analysis of real time systems with the principle similar to Hilbert’s no-infinite divisibility claim, in [2]. The author would like to note some early history of the group’s work on logical analysis of real time system as well as some remark related to Hilbert’s claim of no-infinite divisibility.