Evaluating language models for mathematics through interactions

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

what the paper measures

This paper evaluates language models as interactive mathematics assistants rather than as isolated answer generators. It introduces CheckMate, runs a mixed-cohort study with InstructGPT, ChatGPT, and GPT-4 on undergraduate proofs, releases 261 human-model interactions as MathConverse, derives a ten-category query taxonomy, and adds free-form expert case studies. It does not prove new mathematical theorems or verify Rust, and it does not discuss formal verification beyond a primer on proof assistants (SI A). Inference: the lesson for formal verification is an evaluation protocol that combines interactive traces, correctness ratings, helpfulness ratings, and expert checking.

The abstract states that static input/output pairs are insufficient because they miss deployment interaction: “Static assessment fails to account for the essential interactive element in LLM deployment, and therefore limits how we understand language model capabilities.” (Abstract, p.1). The authors explicitly caution that “humans should be aware of language models’ algebraic fallibility and discern where they are appropriate to use.” (Abstract, p.1).

technique 1: CheckMate interactive trace evaluation

what it is: let a participant work with a model for up to 20 exchanges, record every query and answer, then have the participant rate each query-generation pair on two dimensions (mathematical correctness and perceived helpfulness, each a 7-point scale from 0 to 6, SI E.1) and, after three models, rank the models.

when to use (Inference): when a proof assistant is used in a loop of clarification, correction, and lemma decomposition, where a static benchmark hides whether the assistant recovers from an error.

how to do it:

1. give the participant one proof problem and hide model identity
2. allow free-form interaction for at most 20 exchanges (Methods 6.1, p.16; the paper’s longest observed interaction was 12 steps, SI E.2)
3. record the full interaction trace, including user corrections and model responses
4. have the participant rate mathematical correctness and perceived helpfulness for each generation and rank models after separate tasks
5. keep the per-step ratings and the cross-model preference ranks as separate outputs; the paper argues for “multi-factorial LLM evaluations, beyond a single scalar “goodness” score” (Results 2.1, p.6)

The methods say: “Humans can interact with and rate text generated by language models, and CheckMate records the ‘interaction traces’.” (Methods 6.1, p.15). Participants were blind to model identity and the study used 54 ProofWiki problems, nine from each of six topics (Methods 6.1, pp.16–17). MathConverse contains 261 human-model interactions from 25 entries; the paper cannot confirm these are 25 distinct people because no participant identifier was stored (Introduction, p.5; Methods 6.1, p.17). Generations rated 0 for correctness were filtered out of the quantitative analyses, except the stopping analysis (Methods 6.1, p.17). SI F speaks of 256 human queries annotated, a number that differs from 261 and is not explained in the paper.

Verus form (Inference): instrument a VL proof session with the same trace boundary: source prompt, generated Rust/Verus patch, Verus diagnostics, user edits, and final verification result. Record correctness as independent Verus pass/fail plus contract-review status, and helpfulness as whether the patch reduces proof effort. Keep these measures separate because the paper observed a proof response rated “Multiple critical maths errors” yet “Somewhat useful” (Results 2.1, p.6). The paper does not prescribe Verus instrumentation; this mapping is an inference.

technique 2: interaction-behaviour taxonomy

what it is: manually code each user query into broad behaviour categories, then compare category frequencies across interaction steps and across participants’ prior experience with AI systems (Results 2.3, p.8-9).

how to do it:

1. inspect a sample of traces and identify categories
2. annotate each query by marking which of the 10 buckets it falls into, with an “Other” bucket and an option to mark unsure; SI F says a query may fall into more than one bucket, though most are expected to fall into one
3. have annotators discuss confusion or discrepancies and release the coding (Methods 6.2, p.18)
4. compare first and later turns; the paper lists definitions, general questions, pasted problem statements, and single-step requests as common first moves
5. use later categories—clarification, correction, asking why, examples, and continuation—to design assistant affordances

The paper reports: “over 90% of participants’ first interaction for each problem fall into one of the following interaction behaviour types” (Results 2.2, p.6). Four authors annotated queries; each interaction had one annotator, with discussion for disagreements (Methods 6.2, p.18). The paper says users with minimal prior AI experience were more likely to paste the full prompt, while more experienced users more often asked for decomposed tasks (Results 2.3, p.9).

Verus form (Inference): classify agent requests and responses into proof-level actions: ask for a definition/specification, paste a failing obligation, request one lemma, report a counterexample, correct a generated invariant, ask why a trigger is needed, or request a concrete instance. Use the taxonomy to test whether VL can accept corrections and recover, rather than counting only final proof success.

technique 3: multi-factor correctness and helpfulness analysis

what it is: measure mathematical correctness and perceived helpfulness separately and examine their correlation and divergences.

how to do it:

1. collect per-generation correctness and helpfulness ratings
2. plot correctness against helpfulness by model (Figure 2c) and the ratings by interaction step (SI Figure 9)
3. compute Pearson correlation over all interactions
4. inspect outliers where a response is wrong but useful scaffolding, or correct but unhelpful and verbose
5. add expert case studies to determine whether the response’s reasoning generalizes beyond memorized patterns

The authors report a Pearson correlation of r = 0.83 across all interactions (Results 2.6, p.11), but also state that “These instances reveal that to create useful assistants, increasing the mathematical correctness of these models alone is not sufficient.” (Results 2.6, p.12). They report that participants who indicated low confidence (confidence <= 3) sometimes rated an incorrect generation as completely correct (Results 2.6, p.12).

Verus form (Inference): require a mechanical Verus result for correctness, then separately score whether the proof is maintainable, explanatory, and responsive to the requested change. A green check cannot serve as a helpfulness proxy: a proof may compile because a specification was weakened. Independent review of requires, ensures, invariants, and assumptions is part of the product’s trusted process.

technique 4: expert perturbation and boundary probing

what it is: ask expert mathematicians to test GPT-4 on definitions, concrete instantiations, perturbed problems, and full proofs to locate capability boundaries.

how to do it:

1. choose a solved or familiar problem and ask for the full proof
2. perturb a condition (loosen an assumption, instantiate a variable with concrete values) or ask for a definition or an example
3. ask the model to explain a proof step and to respond to a correction
4. have an expert inspect algebra, strategy, and generalization, not only fluent prose
5. include the complete transcript as qualitative evidence

The methods explain that the case studies seek “the boundary between problems that GPT-4 finds easy and those it finds hard” (Methods 6.3, p.18). The results observe that models can supply useful scaffolding while details of a full proof are incorrect (Results 2.6, p.12), and can over-rely on plausibly memorised examples when a problem is slightly novel (Results 2.6, p.12); the authors add that they cannot be sure of memorisation without access to training data.

Verus form (Inference): perturb a verified Rust task by changing bounds, data-structure sizes, ownership paths, or quantified predicates; ask the agent for a proof repair and then rerun Verus from a clean checkout. Include counterexample-driven requests and require the agent to state which invariant or postcondition changed. This detects memorized proof patterns and vacuous repairs.

what is trusted, measured, and left open

The paper measures ratings, traces, model preferences, taxonomy counts, and expert observations. It does not mechanically verify the informal mathematics. Inference: participant self-ratings, model identity blinding, selected ProofWiki tasks, and four-author annotation are the trusted parts of the experimental design. The authors call MathConverse preliminary and acknowledge that low-confidence participants may falsely judge correctness (Limitations, p.15). The taxonomy is non-exhaustive, and the sample includes only three OpenAI-family models.

Inference: for agent-written verified Rust, the main threat is automation bias and interactive error persistence. VL should not redo static pass/fail benchmarks alone; it should add trace replay, correction tests, specification perturbations, and independent contract review. The paper’s 261-interaction denominator and r = 0.83 correlation characterize this study’s cohort; they do not establish a universal relationship or a Verus success rate. The correlation is computed after dropping generations rated 0 for correctness (Methods 6.1, p.17).

techniques for the catalog

• interactive trace harness — record multi-turn proof assistance and rate every step plus the whole trace
• query-behaviour taxonomy — classify requests such as definitions, single lemmas, corrections, explanations, and examples
• correctness/helpfulness separation — measure mechanical or expert correctness separately from perceived utility
• expert perturbation — vary assumptions and ask for examples or counterexamples to probe generalization
• blind comparative evaluation — hide model identity and rank assistance over separate tasks Checked 2026-10-18 against the full paper by a Claude agent (mid-paper quote: “Problem 28 is a more difficult problem and the model is completely unable to deal with it.”): I read the whole paper text including the supplement and traces; checked every quotation, number (261, 25 entries, 54 problems, 9 per 6 topics, 20-exchange limit, r = 0.83, over 90%, four annotators, 10 categories) and page reference against it; changed the link (the old DOI belonged to the MathQA paper cited in the references; the new link is arXiv 2306.01694 from the paper’s first page), corrected pages for Results 2.6 quotes (p.12) and the 261 figure (p.5), fixed the rating, annotation and taxonomy-comparison descriptions, and labelled unsupported statements as Inference. I did not check the cited external papers, the released repository or dataset, or the Verus mappings, which are the study’s own inferences.

Last edited: 2026-10-18