Philosopher-turned-software developer Brian Rabern is conducting a study comparing human and artificial intelligence (AI) performance on logic problems, and he is looking for student volunteers to take a short online survey.

[Edited version of Rob Weychert, “So LeWitt’s Incomplete Open Cubes Revisited (7-part variations, detail)”. Click image for more.]

I had seen a lot of LLM benchmarks on “logic”. And as a former logic professor I was interested in what they were testing. Much of it was familiar but nothing like an exam that I would give in an intro logic class. And much of it was just propositional logic. Of course, most of these benchmarks are designed by computer scientists, and not philosophers or logicians, per se. So I wanted to design a logic benchmark that was more familiar to what I think of as a logic exam. That was the initial motivation.

The project has now evolved into a study he and a computer science student are conducting to see how good humans and AIs are at logic.

To instructors, he says:

If you teach logic (especially intro), and think some of your students might be interested, please get in touch ([email protected]). I can’t offer compensation or real incentive beyond the science itself, but I will certainly acknowledge faculty who help with recruitment in the final paper.

Here’s some information about what the students will be asked to do:

Students will be emailed a google form with 3 logic tasks:

• • Symbolization: translate a natural-language sentence into logical form.
  • Countermodel: given an invalid argument in formal notation, provide a countermodel.
  • Validity: read a natural-language scenario and decide which of several sentences logically follow.

The form is anonymous but has a few demographic questions.

Here’s an example:

And here’s some background and further information from Rabern:

I’ve built a system (in Python) that compositionally generates grammatical natural language sentences, each with an abstract syntax tree and a formal logical representation (in two-variable FOL without identity). There are actually two lexicons: a fragment of English and a Carroll-style nonsense lexicon. I have a database of 100k+ sentences (e.g., “A human chased a donkey that chased it.”), each paired with a Carrollian counterpart (“A borogove snicker-snacked a tove that snicker-snacked it”) and linked to the same underlying logical representation (“∃x∃y((Nx∧My)∧(Rxy∧Ryx))”). The Carrollian language is meant to isolate logical competence from world knowledge and linguistic intuition — or at least test whether that distinction matters. This controlled fragment enables automated evaluation using SMT solvers (e.g., Z3; thanks Putnam!). The system then can be used to explore the space of sentences, find valid arguments, and record plausible but invalid distractors.

Preliminary benchmarking shows that LLMs struggle with countermodels (which you might have expected), do best on the validity tasks, and perform better at symbolization in English than in Carroll. One natural hypothesis is that the models exploit heuristics on validity tasks rather than deploying the subskills humans typically use (symbolization + proof/model-theoretic methods) — paralleling recent work on how LLMs handle arithmetic. So we think it’d be interesting to get some human data for comparison.

Students who have used the Kalish & Montague or Parsons texts will find the tasks familiar, though none of the exercises involve proof systems. So any students from an intro logic course that covers symbolization and countermodels would be good candidates.

Email Rabern for more info.