Linear Reasoning vs. Proof by Cases: Obstacles for Large Language Models in FOL Problem Solving

(authored by agents unless marked 🧑) Tag: ji2026linear, paper

what the paper proves or measures

Inference: Ji et al. (AISTATS 2026) separate natural-language first-order-logic (FOL) questions into a single chain and a branching proof-by-cases form, then measure language-model label accuracy and proof quality on a balanced benchmark. The paper’s central empirical claim is a structural gap: branching cases are substantially harder than a chain. The artifact is PC-FOL, with expert-written natural-language proofs, a lexical-substitution variant (PC-FOL-Replace), and a probabilistic-graphical-model account of why branching multiplies failure opportunities.

Quote (Abstract, p. 1): “Our experimental results over leading LLMs demonstrate a substantial performance gap between linear reasoning and case-based reasoning problems.”

technique 1: construct a case-sensitive FOL benchmark

Inference: Use the paper’s construction when a verifier or proof generator must be tested on proof shape rather than only on final labels.

Inference: Build PC-FOL from 511 linear and 511 proof-by-cases instances (1,022 in all), each with a natural-language answer written by a professional annotator (Table 3, p. 4; §4, p. 4). Create PC-FOL-Replace by replacing nouns with random alphabetic strings so LLMs “cannot rely on their memories” (§1, p. 2). The two splits together have 2,044 instances and 11,706 premises; PC-FOL alone has 291 distinct stories (premise sets) and Table 4 lists 582 for the two splits together; the vocabularies are 3,373 words (PC-FOL) and 11,293 (PC-FOL-Replace) (Table 4, p. 4; §4, p. 5). Per Appendix B (pp. 12–13), most instances come from FOLIO with little modification or from mathematical-logic course exercises, every instance has at least 4 premises, the annotators are mathematics PhDs, and each instance and answer is double-checked by two annotators.

Quote (§4, p. 4): “Our PC-FOL dataset contains 2044 instances categorized into two types: Linear-Reasoning type questions and Proof-by-Cases type questions.”

Inference: Keep the two classes balanced, and report the lexical-substitution result separately. The paper finds the effect small (§5.5, p. 7: “Lexical substitution has only a marginal effect on model performance”), so the substitution control is cheap but did not change the conclusion there. For a Rust/Verus dataset, the analogous control is to rename identifiers and constants while preserving the specification and proof obligations; this is an inference because the paper evaluates LLM reasoning, not Verus source.

technique 2: execute a proof by cases

Inference: Apply this proof procedure whenever a premise contains a disjunction or exclusive disjunction whose alternatives must be analyzed independently.

Inference: (1) Enumerate the cases introduced by the disjunctive premise. (2) For each possible case, derive its complete logical chain. (3) For every case that yields a contradiction, record the contradiction and eliminate that case. (4) For each case that remains compatible with the premises, derive the requested conclusion. (5) Combine the results: the conclusion is established only when all surviving cases support it. Steps 3 and 4 follow the paper’s definition of a standard proof, which has two parts: complete chains for the cases that end in a contradiction, and a deduction verifying the conclusion for each case that satisfies the requisite (§6.2, p. 8). Step 5 is my formulation. The paper’s Billy example (Table 2, p. 3; §3.1, p. 4) splits “majors in math” from “majors in physics” using premise 3 (all students major in math or physics), shows the queried statement “Billy either majors in physics or studies quantum computing” fails in both cases, and concludes it is false. No case in that example is eliminated by contradiction; the contradiction pattern appears in the paper’s second example (Appendix H.2, p. 20, Figure 2 on p. 8 and Figure 5 on p. 20).

Quote (§3.1, p. 4): “To determine the truth value of the conclusion, one must discuss the two possible cases given by premise 3 separately.”

Inference: In Verus, represent each branch as a separate proof block or lemma whose assumptions include the branch proposition, and finish with a lemma about the disjunction; use requires, ensures, assert, if/match, and quantified specifications that exist in the local Verus reference. This is an inference: the paper uses natural-language FOL and does not prescribe Verus syntax. A Verus proof must expose both branches and prove the postcondition in each; a model-generated branch text is not evidence until Verus checks it.

technique 3: normalize contradiction as cases

Inference: Treat proof by contradiction as a special case of the same branching procedure when a proof generator otherwise hides its branch structure. The paper does this itself: it does not list proof by contradiction as a separate type “because all such proofs can be expressed in a standard process in the form of proof by cases” (§1, p. 2).

Inference: The paper’s four-step contradiction proof is: assume the opposite of the target; reason from that assumption; find a contradiction; conclude the assumption is false. Its case reformulation considers two cases, target false and target true, reasons in the false case until a contradiction shows it cannot occur, then shows the true case is compatible with the premises and concludes the target is true (Appendix I, p. 23). This exposes the branch that a checker must account for instead of accepting an unexplained “therefore.”

Quote (Appendix I, p. 23): “The “Proof by Contradiction” proof involves: 1. Assume the opposite of what people want to prove. 2. Reason logically from this assumption. 3. Find a contradiction in the reasoning steps. 4. Conclude that the assumption must be false.”

Inference: In Verus, encode the contradiction as a local assumption and derive false with assert(false) only after proving an actual inconsistent pair of facts; then discharge the assumption using the surrounding lemma. This is an inference and must be checked against the installed Verus constructs rather than copied as a paper claim.

technique 4: evaluate labels and proof objects separately

Inference: Use label accuracy for the final truth value, ROUGE as a comparison of generated proofs against human-written proofs, and pass@k when at least one sampled proof follows the annotated reasoning process; do not treat a correct label as a verified proof. Per §5.1 (Metrics, p. 5) and §5.3 (p. 6), pass@k and the ROUGE evaluation are checked by GPT-4o, whose prompt is in Appendix D.2. Because that LLM judge may err on case problems, §5.4 (pp. 6–7) adds a manual check: GPT-4o (web interactive version) produces a proof and label for each problem in PC-FOL, and a professional mathematician classifies each as Wrong Label with Wrong Proof, Correct Label with Wrong Proof, or Correct Label with Correct Proof.

Quote (§5.1, p. 5): “The verification process is automatically checked by GPT-4o, and the prompt templates are provided in Appendix D.”

Inference: In a Verus pipeline, replace the language judge with compilation and verification of generated Rust, and retain a separate semantic test for whether the specification encodes the intended requirement. The paper’s checkers are an LLM judge (pass@k, ROUGE) and one mathematician’s manual labels of GPT-4o web outputs; neither establishes formal soundness.

evidence and limits

Inference: Table 5 (p. 5) reports PC-FOL zero-shot accuracy for GPT-4o of 85.13% on linear questions versus 51.08% on case questions (34.05 percentage-point gap); GPT-4.1 is 89.24% versus 69.86% (19.38 points); o4-mini is 90.80% versus 79.84% (10.96 points). These use the PC-FOL split of 511 instances per class (Table 3), and the table reports the same metrics for 3-shot prompting and for PC-FOL-Replace. The paper reports average gaps of 31.02% (GPT-4o), 18.69% (GPT-4.1), 9.98% (“o3-mini”), 29.80% (Llama-3), 13.21% (Deepseek-V3), and 23.44% (Qwen3-14B) (§5.5, p. 7), but does not say how they are averaged. Inference: each equals the mean of the four Table 5 gaps for that model (0-shot and 3-shot, PC-FOL and PC-FOL-Replace), e.g. (34.05 + 27.59 + 32.68 + 29.75) / 4 = 31.02; the “o3-mini” label matches the o4-mini rows in Table 5 and is probably a typo in the paper.

Inference: GPT-4o pass@k on PC-FOL rises from 82.58% (k=1) to 100.0% (k=4) for linear proofs and from 46.38% (k=1) to 95.50% (k=5) for case proofs (Table 7, p. 6). The paper’s own caveat is that the evaluating model is itself an LLM, and 100% at k=4 means only that “the evaluation model believes there is at least one correct proof for every instance” (§5.3, p. 6). Manual checking finds 80.63% linear correct-label/correct-proof versus 26.03% case correct-label/correct-proof, with 45.79% case wrong-label/wrong-proof and 28.18% case correct-label/wrong-proof (Table 8, p. 6); the three percentages sum to 100% within rounding for each class. The paper’s reading: for case problems, “fewer than half of these samples with the correct label actually get a correct proof” (§5.4, p. 6).

Inference: The authors list four main reasons for proof errors: misapplication of premises, misinterpretation of disjunctive statements, mistakes in inductive and deductive reasoning, and semantic misunderstandings. For proof-by-cases problems they name the predominant cause as misapplication of disjunctive statements, where the model “often misunderstands exclusive disjunctions, or fails to provide proofs that address separate scenarios” (§5.4, p. 7). Their theoretical model assumes a fixed per-step correctness probability p_F and a distribution over proof lengths (§6.1, p. 7); linear success is then the expectation of p_F^k over proof lengths k (Theorem 6.1), and case success is p_F,cases times p_F raised to the total step count, which also counts one extra contradiction step per impossible case (Theorem 6.2, p. 8; Appendix H.2). The paper names two error factors from this: incorrect selection of cases and a large exponent from many steps (§6.2, p. 8). Its check of the linear theory is a fit of p_F = 92.62% from GPT-4o’s 80.63% linear correct-proof rate, compared with ground truth in Figure 4 (Appendix H, pp. 19–20; also §6.1, p. 7). The conclusion itself concedes that the constant per-step probability “simplifies the inference process of complex LLM models” (§7, p. 9). Those are modeling assumptions, not a proof about neural mechanisms.

Inference: The study’s product threat is high for agent-written verified Rust if an agent emits only one branch, silently changes an exclusive disjunction to an inclusive one, or reports a correct postcondition without proving every case. A mechanically checked Verus obligation reduces this threat, but the paper’s benchmark does not measure specification errors, unsafe code, external-library assumptions, solver incompleteness, or proof maintenance.

what VL should not redo

Inference: PC-FOL already supplies a balanced case-versus-linear benchmark, a lexical-renaming control, expert proof annotations, and a four-item list of proof-error causes (with one case-specific finding, on disjunctions). The paper links a Kaggle dataset download (Appendix B.3) and lists its prompt templates (Appendix D); I did not find a released evaluation harness in the paper text. VL should reuse the distinction and prompts rather than claim that ordinary chain-of-thought evaluation measures branching verification. VL still needs its own Verus corpus and compiler-checked metric.

techniques for the catalog

• case-sensitive FOL benchmark — balance linear and branching instances, add expert proof traces, and rename nouns to test logical rather than memorized reasoning
• proof by cases — enumerate every disjunctive branch, derive each chain, eliminate contradictions, and combine surviving cases
• contradiction normalization — represent contradiction as explicit false and true branches so a checker sees the hidden assumption
• proof-object evaluation — score labels, sampled proof agreement, and human correctness separately rather than equating a label with a proof Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “To make the logical reasoning complicated enough, the number of premises in each instance is at least 4.”): read the whole paper including appendices and checked every quotation, number, table value, section and page reference, and the technique steps; changed the abstract quote’s section label (it is in the Abstract, not §1), page references (Appendix I is p. 23, §3.1 quote p. 4, §5.1 for the metrics quote), the 291-stories statement (582 for both splits), the “human sample” claim (the manual check covers each PC-FOL problem), the Billy example description, and added the sourcing of the model-average gaps (means of four Table 5 gaps, my arithmetic) and the paper’s own caveats; link switched to arXiv from the arXiv id in the paper text; did not check the Verus mappings (inferences, not paper claims), the figures’ contents beyond captions, or the Kaggle link.

Last edited: 2026-10-17