This paper investigates the logical reasoning capabilities of large language models (LLMs). For a precisely defined yet tractable formulation, we choose the conceptually simple but technically complex task of constructing proofs in Boolean logic. A trained LLM receives as input a set of assumptions and a goal, and produces as output a proof that formally derives the goal from the assumptions. Incorrect proofs are caught by an automated proof checker. A critical obstacle for training is the scarcity of real-world proofs. We propose an efficient, randomized procedure for synthesizing valid proofs and introduce Template Transformation, a data augmentation technique that enhances the model's ability to handle complex logical expressions. The central evaluation question is whether an LLM has indeed learned to reason. We propose tests to measure the reasoning ability of a black-box LLM. By these measures, experiments demonstrate strong reasoning capabilities for assertions with short proofs, which decline with proof complexity. Notably, template transformation improves accuracy even for smaller models, suggesting its effectiveness across model scales.

Homo Sapiens, "wise human" in Latin, is the taxonomic species name for modern humans. But observing the current state of the world and its trajectory, it is hard for me to accept the description "wise." I am not the first to object to the "sapiens" descriptor. The French philosopher Henri-Louis Bergson argued in 1911 that a better term would be Homo Faber, referring to human tool-making ability. This ability goes back to early humans, about three million years ago. Most importantly, human tools got better and better due to innovation and cultural transmission.

Dense retrieval, which aims to encode the semantic information of arbitrary text into dense vector representations or embeddings, has emerged as an effective and efficient paradigm for text retrieval, consequently becoming an essential component in various natural language processing systems. These systems typically focus on optimizing the embedding space by attending to the relevance of text pairs, while overlooking the Boolean logic inherent in language, which may not be captured by current training objectives. In this work, we first investigate whether current retrieval systems can comprehend the Boolean logic implied in language. To answer this question, we formulate the task of Boolean Dense Retrieval and collect a benchmark dataset, BoolQuestions, which covers complex queries containing basic Boolean logic and corresponding annotated passages. Through extensive experimental results on the proposed task and benchmark dataset, we draw the conclusion that current dense retrieval systems do not fully understand Boolean logic in language, and there is a long way to go to improve our dense retrieval systems. Furthermore, to promote further research on enhancing the understanding of Boolean logic for language models, we explore Boolean operation on decomposed query and propose a contrastive continual training method that serves as a strong baseline for the research community.

We introduce SetBERT, a fine-tuned BERT-based model designed to enhance query embeddings for set operations and Boolean logic queries, such as Intersection (AND), Difference (NOT), and Union (OR). SetBERT significantly improves retrieval performance for logic-structured queries, an area where both traditional and neural retrieval methods typically underperform. We propose an innovative use of inversed-contrastive loss, focusing on identifying the negative sentence, and fine-tuning BERT with a dataset generated via prompt GPT. Furthermore, we demonstrate that, unlike other BERT-based models, fine-tuning with triplet loss actually degrades performance for this specific task. Our experiments reveal that SetBERT-base not only significantly outperforms BERT-base (up to a 63% improvement in Recall) but also achieves performance comparable to the much larger BERT-large model, despite being only one-third the size.

It is a well-known story that theoretical computer science and biology have been drawing inspiration from each other for decades. While computer science has tried to mimic the functioning of living systems to develop computing models, including automata, artificial neural networks, and evolutionary algorithms, biology has used computing as a metaphor to explain the functioning of living systems.4 For example, biologists have used Boolean logic to conceptualize gene regulation since early 1970s, when Jacques Monod wrote the inspirational statement "… like the workings of computers."40 This article contends that information processing is the link between computer science and molecular biology. In computer science, a model of computation such as finite state machines or Turing machines defines how to generate output from a set of inputs and a set of rules or instructions.

Training machine learning models can often be a very challenging process, requiring significant computational resources and time. The use of DNNs on computing hardware such as mobile and IoT devices is becoming increasingly important. IoT devices often have limitations in terms of memory and computational capacity. Quantization is a potential solution to this problem (Courbariaux et al., 2015; Chmiel et al., 2021; Leconte et al., 2023). And in particular, Binary Neural Networks (BNNs) is a remarkably promising direction because it reduces both memory and inference latency simultaneously (Nguyen, 2023). Formaly, BNN training can be formulated as minimising the training loss with binary weights, i.e., min f(w); f(w) = E

Beyond the great cognitive powers showcased by language models, it is crucial to scrutinize whether their reasoning capabilities stem from strong generalization or merely exposure to relevant data. As opposed to constructing increasingly complex logic, this paper probes into the boolean logic, the root capability of a logical reasoner. We find that any pre-trained language models even including large language models only behave like a random selector in the face of multi-nested boolean logic, a task that humans can handle with ease. To empower language models with this fundamental capability, this paper proposes a new self-supervised learning method \textit{Curriculum Logical Reasoning} (\textsc{Clr}), where we augment the training data with nested boolean logic chain step-by-step, and program the training from simpler logical patterns gradually to harder ones. This new training paradigm allows language models to effectively generalize to much harder and longer-hop logic, which can hardly be learned through naive training. Furthermore, we show that boolean logic is a great foundation for improving the subsequent general logical tasks.

Plotkin, M. Binary codes with specified minimum distance.

We introduce epistemic quantified boolean logic (EQBL), an extension of propositional epistemic logic with quantification over propositions. We show that EQBL can express relevant properties about agents' knowledge in multi-agent contexts, such as "agent a knows as much as agent b". We analyse the expressiveness of EQBL through a translation into monadic second-order logic, and provide completeness results w.r.t.

The term DNA immediately calls to mind the double-stranded helix that contains all our genetic information. But the individual units of its two strands are pairs of molecules bonded with each other in a selective, complementary fashion. Turns out, one can take advantage of this pairing property to perform complex mathematical calculations, and this forms the basis of DNA computing. Since DNA has only two strands, performing even a simple calculation requires multiple chemical reactions using different sets of DNA. In most existing research, the DNA for each reaction are added manually, one by one, into a single reaction tube, which makes the process very cumbersome.