Pith. sign in

REVIEW 3 major objections 5 minor 50 references

TempoBench: Evaluating Temporal Causal Reasoning in Large Language Models

T0 review · 3 major / 5 minor · reviewed 2026-08-04 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read The paper claims that large language models can simulate a system's behavior over time, yet systematically fail to identify which earlier inputs were necessary to cause a given output, and it introduces a formally verified benchmark — Tempo

desk verdict TempoBench has a genuinely useful idea—formally verified temporal causal labels from reactive synthesis and CORP—but the abstract promises claims the body doesn't deliver, and the prompt's 'any one missing' semantics likely doesn't match the formal definition of minimal cause. read the letter →

arxiv 2510.27544 v2 pith:2WSH66VR submitted 2025-10-31 cs.AI cs.FL

Nikolaus Holzer , William Fishell , Baishakhi Ray , Mark Santolucito This is my paper
classification cs.AIcs.FL
keywords temporalcausalreasoningLLMevaluationreactivesynthesisMealymachinestracesimulationminimalattributionformalverificationoverspecification
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

TempoBench is a synthetic, formally verified benchmark that separates two temporal reasoning abilities in large language models: simulating a system's behavior over time (trace evaluation), and identifying which past inputs were necessary to produce an observed output (minimal causal attribution). The paper claims that frontier models are strong at the first but systematically weak at the second: on the hard causal attribution task, aggregated F1 drops to 7.5%, and over 94% of causal errors are overspecification, where the model lists all inputs rather than the minimal cause set. The benchmark is built from reactive systems specified in temporal logic and synthesized into Mealy machines, so every trace and every causal label is formally grounded. If the paper is correct, it provides a parameterized diagnostic for causal credit assignment in LLMs, and evidence that fine-tuning on this benchmark transfers to standard reasoning tasks better than math, code, or instruction training.

What carries the argument

The framework is built from reactive synthesis: temporal-logic specifications are compiled into Mealy machines, presented in the HOA structured automaton format; random valid traces are sampled from those machines; and for each output effect a causality synthesis algorithm computes a minimal causal automaton over inputs. That automaton defines the ground truth: at each time step, which input conjunction is necessary for the effect. The framework also exposes five tunable difficulty features — effect depth, number of states, number of transitions, causal input count, and unique inputs in trace — and uses correlation plus feature-attribution analysis to show which structural features drive F1

What would settle it

Independently verify a random sample of hard causal items by counterfactual simulation: for each ground-truth cause, delete that input from the trace and re-run the machine; if the effect still occurs in a large share of cases, the labels are not minimal necessary conditions.

Watch

Extended reading notes

Core claim

The central claim is that LLMs can follow a trace through a finite-state machine but largely cannot perform temporal causal attribution: given a trace and an output effect at a time step, they fail to recover the minimal set of earlier inputs that were necessary for the effect. The paper supports this with a formally synthesized benchmark whose ground-truth causal labels are produced by a temporal-causality synthesis algorithm, reporting that models reach 65.6% F1 on the normal causal task but fall to 7.5% on the hard task, with 94% of errors being overspecification. The authors also report that fine-tuning on the benchmark's training corpus improves causal reasoning and generalizes better t

Load-bearing premise

The entire ground truth for the causal task rests on the assumption that the synthesis algorithm's causal sets are exactly the minimal input sets necessary for each output on the finite traces shown to the models; if that minimality notion does not carry over to finite traces, the scores measure fidelity to a tool's convention rather than causal reasoning.

Editorial extensions

If this is right

  • Trace simulation and causal attribution are separable capabilities; improving one does not imply improving the other.
  • Denser systems with more transitions can be easier, not harder, for models to track, so raw system size is not a reliable proxy for reasoning difficulty.
  • The dominant failure mode is overspecification, suggesting current models default to input retrieval instead of minimal-cause search.
  • The benchmark is a verified source of training data, and fine-tuning on it reportedly transfers to standard reasoning tasks better than math, code, or instruction data.
  • Near-7.5% scores on hard causal items quantify a systematic gap in causal credit assignment in frontier LLMs as system complexity grows.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The causal labels are defined over infinite omega-regular runs; a human study on the same finite traces would clarify whether the 7.5% score is model failure or a mismatch between the tool's minimality convention and the minimality a human would name — this is our inference, not the paper's.
  • If overspecification is really retrieval behavior, then a prompt that forces a per-input counterfactual test ('remove this input and re-simulate') might recover part of the gap; this is testable with the published harness but is not claimed by the paper.
  • The same synthesis pipeline could generate curricula that interleave trace simulation with causal attribution, a training strategy the paper leaves implicit.
  • The difficulty features could be used to predict where reinforcement-learning fine-tuning helps most, such as high-state-count, low-causal-density problems.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 5 minor

Summary. TempoBench is a synthetic benchmark for two temporal-reasoning tasks on Mealy machines generated from SYNTCOMP TLSF specifications via LTLsynt (HOA) and HOAX traces, with ground-truth causal labels from CORP. TTE asks whether a trace is accepted (simulation); TCE asks for the minimal set of inputs necessary for a queried output. Five LLMs are evaluated on 400 samples each under one-shot prompting, scored by AP-level and timestep-level F1, split into normal/hard by five structural features, and analyzed with random-forest SHAP. The central reported finding is that models perform reasonably on TTE (aggregate TS F1 approximately 52.8-61.0%) and on TCE-normal (65.6% TS F1) but collapse on TCE-hard (7.5% TS F1), suggesting a systematic difficulty with causal credit assignment as system complexity grows.

Significance. If the causal labels are correct under the stated semantics, TempoBench would be a valuable, formally grounded diagnostic: it uses external synthesis and causality tools rather than LLM-generated labels, it provides controlled structural difficulty features, and the sharp TTE/TCE gap is a falsifiable, non-obvious empirical finding that would help isolate causal attribution from simulation. The release of code and per-model SHAP analyses are additional strengths. However, the benchmark's validity currently rests on an unproven equivalence between CORP's minimal-cause convention and the prompt's individual-necessity semantics, and the abstract reports experiments that are absent from the body.

major comments (3)
  1. [Appendix A.2 / Listing 3 / Section 3.2] The prompt defines causality as individual necessity ('If any one of these inputs were missing, the effect would not have occurred'), but the formal definition in Appendix A.2 (conditions 1-3) only requires that altering/removing the whole set C can falsify E and that no proper subset of C is itself such a cause. Minimality of a sufficient set does not imply that each member is individually necessary. Algorithm 1 delegates to corp() without showing the reduction from CORP's output to the per-step JSON, and no oracle validation against the stated individual-necessity semantics is provided. The headline 7.5% TCE-hard / overspecification numbers may therefore measure fidelity to CORP's convention rather than the claimed causal reasoning. Add a proof or finite-trace brute-force check that each labeled input satisfies the prompt's counterfactual, or align the labels and prompt to one semantic
  2. [Abstract vs. Sections 3-7] The abstract claims 'up to 96% accuracy on SIM', 'below 25% on MIN', 'over 94% overspecification', and fine-tuning generalization improvements. None of these appear in the body or in Tables 1-3; the body reports only F1(AP)/F1(TS) values and contains no fine-tuning or overspecification experiments. The 96% figure is also hard to reconcile with the highest TTE F1(TS) value of 70.1% in Table 1. The unsupported claims should be removed or the corresponding experiments added; as written, the abstract and body appear to describe different results.
  3. [Section 3.3 / Algorithm 1] The hard/normal construction and label generation are underspecified. Section 3.3 says 'select the top n problems with the highest value for each feature' but does not give n, tie-breaking, or whether thresholds are applied per task or on the aggregate. Algorithm 1 is a three-line loop around corp() and does not state how the causal automaton becomes the target JSON, including 'no constraints' entries and repeated atomic propositions. This blocks reproducibility and auditing of the claimed 'provably correct' labels. Provide the full extraction procedure and thresholds.
minor comments (5)
  1. [Section 5.1] 'TTE and TCP tasks' should read 'TTE and TCE tasks'.
  2. [Section 5.2] The text says the SHAP features are 'listed from most important to least important,' but no such list appears; please provide the list or remove the sentence.
  3. [Figure 16 caption] The caption repeats 'Time Step Evaluation' even though the subsection concerns Atomic Proposition Evaluation; correct the caption.
  4. [Section 5.1] The MCP-optimization hypothesis is speculative, and the cited reference [41] (Toolformer) does not support it; either remove the speculation or provide an appropriate citation.
  5. [Listing 3] The one-shot prompt contains a complete ground-truth JSON answer. Consider adding a control or discussion showing that models do not simply imitate the 'no constraints' pattern from the demonstration.

Circularity Check

1 steps flagged · score 2.0 of 10

TempoBench's headline TCE/TTE numbers are genuine measurements against externally generated, formally verified labels; only the difficulty-feature analysis is mildly self-referential.

  1. other [Section 3.3 (Data Generation / Difficulty Features) and Section 5.2 (Statistical Analysis, Fig. 11, Table 2)]
    "TempoBench exposes five features that let us scale problem difficulty... To make TempoBench Hard, we select the top n problems with the highest value for each of these features at generation time. These features allow us to condition evaluation on problem structure... The SHAP plots in figure 11 highlight both the relative importance of each feature and the direction of its influence on the F1 Score."

    The hard/normal split is defined by selecting top-n samples on the same five structural features (effect depth, system states, transition count, causal inputs count, unique inputs in trace) that the statistical analysis then identifies as the drivers of the TCE F1 gap. The random-forest/SHAP importance ranking re-discovers the very dimensions along which the hard set was constructed, so the claim 'these features cause difficulty' is partly by construction. However, the underlying F1 scores are measured model outputs, not fitted values, and the hard-vs-normal gap could in principle have gone either way; this circularity is therefore confined to the diagnostic feature-importance analysis and does not affect the headline 7.5% vs 65.6% comparison.

full rationale

The central empirical claim — LLMs simulate traces well but score only 7.5% F1(TS) on TCE-hard minimal causal attribution — is a genuine measurement against ground-truth labels produced by external formal tools (LTLsynt for controller synthesis, HOAX for trace generation, CORP for temporal causality) and external published definitions of temporal causality (Coenen et al. 2022; Finkbeiner et al. 2024). No parameter is fitted to produce the success or failure rates, and nothing in the generation pipeline forces models to score low; the dramatic hard/normal gap is an observed outcome. The only mild self-referentiality is in the difficulty-feature analysis: hard problems are selected as top-n on the structural features later reported as the drivers of difficulty, and the random-forest/SHAP analysis partly re-discovers the selection criteria. That affects the interpretability of the diagnostic-statistics section, not the integrity of the headline scores. The skeptic's concern that CORP's minimal counterfactual-sufficient sets may not satisfy the prompt's individual-necessity semantics ('If any one of these inputs were missing...') is a construct-validity or correctness risk, not a circularity: the labels are external and are not derived from the claims they support. Overall, the paper's derivation chain is self-contained as an evaluation study; no prediction reduces by construction to its inputs.

Assumptions & free parameters 2 free parameters · 4 assumptions · 1 invented entities

The benchmark's correctness rests on external formal tools and definitions rather than on fitted parameters. The only freely chosen numerical quantities are the unreported hard/normal cutoffs and unreported decoding settings, which directly affect the headline difficulty collapse.

free parameters (2)
  • TCE-hard selection threshold (top-n per feature) = not reported
    The normal/hard split is defined by taking top-n problems per difficulty feature (§3.3, §4.1); n and feature-specific thresholds are never given, so the headline normal-to-hard collapse (65.6% to 7.5%) is not reproducible.
  • LLM decoding parameters = not reported
    API evaluations of 800 samples per model are described without temperature, top-p, random seed, or number of runs, so sampling variance and prompt stochasticity are unquantified.
assumptions (4)
  • domain assumption LTL reactive synthesis (SYNTCOMP to LTLsynt to HOA) yields Mealy controllers whose finite traces faithfully realize the original temporal specifications.
    The entire dataset construction depends on this; invoked in §3.2 item (1). If synthesis or the HOA extraction distorts the specification, all downstream traces and causal labels are affected.
  • domain assumption CORP's temporal causality conditions (trace satisfies cause/effect, counterfactual dependence, minimality) correctly define the ground-truth 'minimal causal inputs' for each finite trace.
    TCE labels are taken directly from CORP via Algorithm 1 and Appendix A.2. The paper does not independently verify on finite traces that these labels match the intended 'minimal set of inputs necessary for the outcome' semantics.
  • ad hoc to paper The five hand-chosen structural features (effect depth, state count, transition count, causal input count, unique inputs in trace) capture the intended difficulty space.
    Introduced in §3.3 as 'five features that let us scale problem difficulty'. The selection of these five features rather than alternatives is not externally justified and becomes the basis for the hard/normal split and the SHAP analysis.
  • domain assumption A single one-shot CoT prompt is a valid measure of model capability rather than a measure of format/comprehension confounds.
    The paper uses high TTE scores to argue that HOA parsing is not the bottleneck, but the TCE instruction to output 'minimal set of inputs' could still be misunderstood independently of causal ability; no prompt ablations or multiple prompt variants are reported.
invented entities (1)
  • The five TempoBench difficulty features as a formal difficulty space
    purpose: Used to define normal/hard splits and to explain LLM performance via SHAP feature importance.
    These features are introduced by the paper as the relevant difficulty axes; they are not derived from an external theory and are explicitly chosen by the authors to parametrize complexity.

how reviews work

0 comments
Cite this review

Pith. "Pith review of TempoBench: Evaluating Temporal Causal Reasoning in Large Language Models." pith.science (2026). https://pith.science/paper/2WSH66VR

@misc{pith2026251027544,
  author       = {Pith},
  title        = {Pith review of: TempoBench: Evaluating Temporal Causal Reasoning in Large Language Models},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/2WSH66VR}},
  note         = {Machine review of arXiv:2510.27544}
}
read the original abstract

Temporal reasoning involves understanding how systems evolve over time through input-driven state transitions. A key aspect is temporal causal reasoning, causally reasoning about what prior inputs were necessary in causing an observed outcome. While large language models (LLMs) perform well at forward simulation, predicting outputs from inputs, they struggle to identify the minimal causal inputs of outcomes. To study this distinction, we define two tasks: \textit{trace simulation} (SIM), which requires models to simulate system execution, and \textit{minimal causal attribution} (MIN), which identifies the minimal set of inputs necessary for a given outcome. We introduce \textsc{TempoBench}, the first formally verified benchmark for temporal causal reasoning, built from synthesized Mealy machines with controllable complexity and provably correct causal labels. Across frontier models, we observe that despite achieving up to 96\% accuracy on the SIM task, performance on the causal attribution MIN task drops below 25\%; models fail to reason about causal necessity. Over 94\% of causal errors involve overspecification, where models perform retrieval and list all possible inputs rather than reasoning about the minimal causal subset. Fine-tuning on \textsc{TempoBench} training corpus improves causal reasoning and generalizes better than math, code, or instruction training, with gains across standard reasoning benchmarks.

Figures

Figures reproduced from arXiv: 2510.27544 by the authors.

Figure 1
Figure 1. Overview of the TempoBench framework. TempoBench includes 5 key features for modeling temporal problem difficulty and uses them to conduct rigorous statistical analysis of reasoning performance. Tem￾poBench consists of two tasks: Temporal Trace Evaluation (TTE) and Temporal Causality Evaluation (TCE) . permissions, such as access control lists [4]. Causality is also used for root cause analysis, for example, in micr… view at source ↗
Figure 2
Figure 2. Sample knowledge graph showcasing relationship inference. In this case, asked to determine who [PITH_FULL_IMAGE:figures/full_fig_p004_2.png] view at source ↗
Figure 3
Figure 3. Sample visualization of a tempo-bench problem. This example shows a trace through a system and a [PITH_FULL_IMAGE:figures/full_fig_p005_3.png] view at source ↗
Figures from the paper (14 more)
Figure 4
Figure 4. Figure 4: Pipeline flowchart for data generation in [PITH_FULL_IMAGE:figures/full_fig_p006_4.png]
Figure 5
Figure 5. Figure 5: Pipeline flowchart for the evaluation harness that we use to score reasoning model performance [PITH_FULL_IMAGE:figures/full_fig_p007_5.png]
Figure 6
Figure 6. Figure 6: Visualization of results across all benchmark tasks. TTE normal and hard, TCE normal and hard. [PITH_FULL_IMAGE:figures/full_fig_p009_6.png]
Figure 7
Figure 7. Figure 7: Correlation scores for log10 (transition_count) and log10 (hoa_states) versus 𝐹1(TS) scores at the temporal step, with corresponding 𝑝-values denoting statistical significance [PITH_FULL_IMAGE:figures/full_fig_p011_7.png]
Figure 8
Figure 8. Figure 8: Correlation scores for log10 (transition_count) and log10 (hoa_states) versus 𝐹1(AP) scores at the Atomic Proposition step, with corresponding 𝑝-values denoting statistical significance validating the effectiveness of our difficulty features. This trend is consistent a…
Figure 9
Figure 9. Figure 9: Correlation scores for log10 (unique_inputs_in_trace), log10 (hoa_states), and log10 (transition_count) versus 𝐹1 scores at the Atomic Proposition step, with corresponding 𝑝- values denoting statistical significance. This figure covers the TTE task. The TTE task reveal…
Figure 10
Figure 10. Figure 10: SHAP Beeswarm plot representing feature importance and correlation with Temporal Causality [PITH_FULL_IMAGE:figures/full_fig_p014_10.png]
Figure 11
Figure 11. Figure 11: SHAP Beeswarm plot representing feature importance and correlation with Temporal Causality [PITH_FULL_IMAGE:figures/full_fig_p014_11.png]
Figure 12
Figure 12. Figure 12: Temporal Causality HOA for Trace of Music Player [PITH_FULL_IMAGE:figures/full_fig_p020_12.png]
Figure 13
Figure 13. Figure 13: Complete pipeline flowchart for data generation in [PITH_FULL_IMAGE:figures/full_fig_p021_13.png]
Figure 14
Figure 14. Figure 14: Sample of a binary mod 3 DFA D.2 SHAPLEY Plots On Model Level and 𝑅 2 Scores Model Time Step 𝑅 2 AP Step 𝑅 2 Claude Sonnet 3.5 0.497 0.507 Claude Sonnet 4.5 0.772 0.613 Qwen 0.349 0.271 GPT-4o 0.429 0.440 GPT-4o Mini 0.781 0.776 [PITH_FULL_IMAGE:figures/full_fig_p024…
Figure 15
Figure 15. Figure 15: Shapley plots demonstrate that the behavior observed at the statistical results level is consistent at [PITH_FULL_IMAGE:figures/full_fig_p025_15.png]
Figure 16
Figure 16. Figure 16: Shapley plots demonstrate that the behavior observed at the statistical results level is consistent at [PITH_FULL_IMAGE:figures/full_fig_p026_16.png]
Figure 17
Figure 17. Figure 17: Distribution of 𝐹1 scores for Timestep Tem￾poral Causality [PITH_FULL_IMAGE:figures/full_fig_p026_17.png]

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

50 extracted references · 6 linked inside Pith

  1. [1]

    InPredictive analytics with KNIME: Analytics for citizen data scientists

    Acito, F.Ordinary least squares regression. InPredictive analytics with KNIME: Analytics for citizen data scientists. Springer, 2023, pp. 105–124. [2]Anthropic. Claude-3.5 sonnet. https://www.anthropic.com/news/claude-3-5-sonnet, 2024. Accessed: 2025-10-05. [3]Anthropic. Claude sonnet-4.5. https://www.anthropic.com/news/claude-sonnet-4-5, 2025. Accessed: ...

    2023

  2. [4]

    Semantic-based automated reasoning for aws access policies using smt

    Backes, J., Bolignano, P., Cook, B., Dodge, C., Gacek, A., Luckow, K., Rungta, N., Tkachuk, O., and V arming, C. Semantic-based automated reasoning for aws access policies using smt. In2018 Formal Methods in Computer Aided Design (FMCAD)(2018), pp. 1–9

    2018

  3. [5]

    Besta, M., Blach, N., Kubicek, A., Gerstenberger, R., Podstawski, M., Gianinazzi, L., Gajda, J., Lehmann, T., Niewiadomski, H., Nyczyk, P., and Hoefler, T.Graph of thoughts: solving elaborate problems with large language models. InProceedings of the Thirty-Eighth AAAI Conference on Artificial Intelligence and Thirty-Sixth Conference on Innovative Applicat...

    2024

  4. [6]

    A., and Janzing, D.Dowhy-gcm: An extension of dowhy for causal inference in graphical causal models.Journal of Machine Learning Research 25, 147 (2024), 1–7

    Blöbaum, P., Götz, P., Budhathoki, K., Mastakouri, A. A., and Janzing, D.Dowhy-gcm: An extension of dowhy for causal inference in graphical causal models.Journal of Machine Learning Research 25, 147 (2024), 1–7

    2024

  5. [7]

    Brown, T., Mann, B., Ryder, N., Subbiah, M., Kaplan, J. D., Dhariwal, P., Neelakantan, A., Shyam, P., Sastry, G., Askell, A., et al.Language models are few-shot learners.Advances in neural information processing systems 33(2020), 1877–1901

    2020

  6. [8]

    T., Li, Y., Lundberg, S., Nori, H., Palangi, H., Ribeiro, M

    Bubeck, S., Chandrasekaran, V., Eldan, R., Gehrke, J., Horvitz, E., Kamar, E., Lee, P., Lee, Y. T., Li, Y., Lundberg, S., Nori, H., Palangi, H., Ribeiro, M. T., and Zhang, Y.Sparks of artificial general intelligence: Early experiments with gpt-4, 2023. , Vol. 1, No. 1, Article . Publication date: November 2025. 16 Nikolaus Holzer, William Fishell, Baishak...

    2023

  7. [9]

    Chen, M., Tworek, J., Jun, H., Yuan, Q., de Oliveira Pinto, H. P., Kaplan, J., Edwards, H., Burda, Y., Joseph, N., Brockman, G., Ray, A., Puri, R., Krueger, G., Petrov, M., Khlaaf, H., Sastry, G., Mishkin, P., Chan, B., Gray, S., Ryder, N., Pavlov, M., Power, A., Kaiser, L., Bavarian, M., Winter, C., Tillet, P., Such, F. P., Cummings, D., Plappert, M., Ch...

    2021

  8. [10]

    W.Program of thoughts prompting: Disentangling computation from reasoning for numerical reasoning tasks, 2023

    Chen, W., Ma, X., W ang, X., and Cohen, W. W.Program of thoughts prompting: Disentangling computation from reasoning for numerical reasoning tasks, 2023. [11]Chollet, F., Knoop, M., Kamradt, G., and Landers, B.Arc prize 2024: Technical report, 2025

    2023

Show all 50 references
  1. [12]

    Chollet, F., Knoop, M., Kamradt, G., Landers, B., and Pinkard, H.Arc-agi-2: A new challenge for frontier ai reasoning systems, 2025

    2025

  2. [13]

    Church, A.Application of recursive arithmetic to the problem of circuit synthesis.Journal of Symbolic Logic 28, 4 (1963)

    1963

  3. [14]

    Cobbe, K., Kosaraju, V., Bavarian, M., Chen, M., Jun, H., Kaiser, L., Plappert, M., Tworek, J., Hilton, J., Nakano, R., Hesse, C., and Schulman, J.Training verifiers to solve math word problems, 2021

    2021

  4. [15]

    InInternational symposium on automated technology for verification and analysis(2022), Springer, pp

    Coenen, N., Finkbeiner, B., Frenkel, H., Hahn, C., Metzger, N., and Siber, J.Temporal causality in reactive systems. InInternational symposium on automated technology for verification and analysis(2022), Springer, pp. 208–224

    2022

  5. [16]

    Davila, N., Wiese, I., Steinmacher, I., Lucio da Silva, L., Kawamoto, A., Favaro, G. J. P., and Nunes, I.An industry case study on adoption of ai-based programming assistants. InProceedings of the 46th International Conference on Software Engineering: Software Engineering in P...

    2024

  6. [17]

    DeepSeek-AI, Guo, D., Yang, D., Zhang, H., Song, J., Zhang, R., Xu, R., Zhu, Q., Ma, S., Wang, P., Bi, X., Zhang, X., Yu, X., Wu, Y., Wu, Z. F., Gou, Z., Shao, Z., Li, Z., Gao, Z., Liu, A., Xue, B., Wang, B., Wu, B., Feng, B., Lu, C., Zhao, C., Deng, C., Zhang, C., Ruan, C., D...

    2025

  7. [18]

    InInternational Conference on Runtime Verification(2025), Springer, pp

    Di Stefano, L.Execution and monitoring of hoa automata with hoax. InInternational Conference on Runtime Verification(2025), Springer, pp. 44–53

    2025

  8. [19]

    Ding, J., Zhang, Y., Shang, Y., Zhang, Y., Zong, Z., Feng, J., Yuan, Y., Su, H., Li, N., Sukiennik, N., et al.Understanding world or predicting future? a comprehensive survey of world models.ACM Computing Surveys 58, 3 (2025), 1–38

    2025

  9. [20]

    J., Kaiser, G., and Ray, B.Cycle: Learning to self-refine the code generation.Proc

    Ding, Y., Min, M. J., Kaiser, G., and Ray, B.Cycle: Learning to self-refine the code generation.Proc. ACM Program. Lang. 8, OOPSLA1 (Apr. 2024)

    2024

  10. [21]

    J., Kaiser, G., Yang, J., and Ray, B.Semcoder: Training code language models with comprehensive semantics reasoning

    Ding, Y., Peng, J., Min, M. J., Kaiser, G., Yang, J., and Ray, B.Semcoder: Training code language models with comprehensive semantics reasoning. InAdvances in Neural Information Processing Systems(2024), A. Globerson, L. Mackey, D. Belgrave, A. Fan, U. Paquet, J. Tomczak, and ...

    2024

  11. [22]

    Fatemi, B., Kazemi, M., Tsitsulin, A., Malkan, K., Yim, J., Palowitch, J., Seo, S., Halcrow, J., and Perozzi, B.Test of time: A benchmark for evaluating llms on temporal reasoning, 2024

    2024

  12. [23]

    Fatemi, B., Kazemi, M., Tsitsulin, A., Malkan, K., Yim, J., Palowitch, J., Seo, S., Halcrow, J., and Perozzi, B.Test of time: A benchmark for evaluating llms on temporal reasoning.arXiv preprint arXiv:2406.09170(2024)

    2024 arXiv

  13. [24]

    InInternational Conference on Computer Aided Verification(2024), Springer, pp

    Finkbeiner, B., Frenkel, H., Metzger, N., and Siber, J.Synthesis of temporal causality. InInternational Conference on Computer Aided Verification(2024), Springer, pp. 87–111

    2024

  14. [25]

    In International Conference on Computer Aided Verification(2019), Springer, pp

    Finkbeiner, B., Klein, F., Piskac, R., and Santolucito, M.Temporal stream logic: Synthesis beyond the bools. In International Conference on Computer Aided Verification(2019), Springer, pp. 609–629. , Vol. 1, No. 1, Article . Publication date: November 2025. Mechanics of Learne...

    2019

  15. [26]

    Huan, M., Li, Y., Zheng, T., Xu, X., Kim, S., Du, M., Poovendran, R., Neubig, G., and Yue, X.Does math reasoning improve general llm capabilities? understanding transferability of llm reasoning.arXiv preprint arXiv:2507.00432(2025)

    2025 arXiv

  16. [27]

    Ikram, A., Chakraborty, S., Mitra, S., Saini, S., Bagchi, S., and Kocaoglu, M.Root cause analysis of failures in microservices through causal discovery.Advances in Neural Information Processing Systems 35(2022), 31158–31170

    2022

  17. [28]

    1 (extended version).arXiv preprint arXiv:1604.02284(2016)

    Jacobs, S., Klein, F., and Schirmer, S.A high-level ltl synthesis format: Tlsf v1. 1 (extended version).arXiv preprint arXiv:1604.02284(2016)

    2016 arXiv

  18. [29]

    Jacobs, S., Pérez, G. A., Abraham, R., Bruyère, V., Cadilhac, M., Colange, M., Delfosse, C., van Dijk, T., Duret- Lutz, A., Faymonville, P., Finkbeiner, B., Khalimov, A., Klein, F., Luttenberger, M., Meyer, K., Michaud, T., Pommellet, A., Renkin, F., Schlehuber-Caissier, P., S...

    2018

  19. [30]

    E., Y ang, J., Wettig, A., Y ao, S., Pei, K., Press, O., and Narasimhan, K.Swe-bench: Can language models resolve real-world github issues?, 2024

    Jimenez, C. E., Y ang, J., Wettig, A., Y ao, S., Pei, K., Press, O., and Narasimhan, K.Swe-bench: Can language models resolve real-world github issues?, 2024

    2024

  20. [31]

    H., Horstmann, S

    Klemmer, J. H., Horstmann, S. A., Patnaik, N., Ludden, C., Burton, Cordell, J., Powers, C., Massacci, F., Rahman, A., Votipka, D., Lipford, H. R., Rashid, A., Naiakshina, A., and Fahl, S.Using ai assistants in software development: A qualitative study on security practices and...

    2024

  21. [32]

    Leucker, M., and Schallhart, C.A brief account of runtime verification.The journal of logic and algebraic programming 78, 5 (2009), 293–303

    2009

  22. [33]

    Gpt-4o mini: Advancing cost-efficient intelligence

    OpenAI. Gpt-4o mini: Advancing cost-efficient intelligence. https://openai.com/index/gpt-4o-mini-advancing-cost- efficient-intelligence/, 2024. Accessed: 2025-10-05

    2024

  23. [34]

    Gpt-4o (“omni”): Openai’s flagship multimodal model

    OpenAI. Gpt-4o (“omni”): Openai’s flagship multimodal model. https://platform.openai.com/docs/models/gpt-4o, 2024. Accessed: 2025-10-05

    2024

  24. [35]

    Ouyang, L., Wu, J., Jiang, X., Almeida, D., W ainwright, C. L., Mishkin, P., Zhang, C., Agarwal, S., Slama, K., Ray, A., Schulman, J., Hilton, J., Kelton, F., Miller, L., Simens, M., Askell, A., Welinder, P., Christiano, P., Leike, J., and Lowe, R.Training language models to f...

    2022

  25. [36]

    Pham, L., Ha, H., and Zhang, H.Root cause analysis for microservice system based on causal inference: How far are we? ASE ’24, Association for Computing Machinery

  26. [37]

    In18th annual symposium on foundations of computer science (sfcs 1977) (1977), ieee, pp

    Pnueli, A.The temporal logic of programs. In18th annual symposium on foundations of computer science (sfcs 1977) (1977), ieee, pp. 46–57

    1977

  27. [38]

    InProceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages(1989), pp

    Pnueli, A., and Rosner, R.On the synthesis of a reactive module. InProceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages(1989), pp. 179–190

    1989

  28. [39]

    Renkin, F., Schlehuber-Caissier, P., Duret-Lutz, A., and Pommellet, A.Dissecting ltlsynt.Formal Methods in System Design 61, 2 (2022), 248–289

    2022

  29. [40]

    Roychoudhury, A., Pasareanu, C., Pradel, M., and Ray, B.Agentic ai software engineers: Programming with trust, 2025

    2025

  30. [41]

    Schick, T., Dwivedi-Yu, J., Dessì, R., Raileanu, R., Lomeli, M., Hambro, E., Zettlemoyer, L., Cancedda, N., and Scialom, T.Toolformer: Language models can teach themselves to use tools.Advances in Neural Information Processing Systems 36(2023), 68539–68551

    2023

  31. [42]

    Srivastava, A., Rastogi, A., Rao, A., Shoeb, A. A. M., Abid, A., Fisch, A., Brown, A. R., Santoro, A., Gupta, A., Garriga-Alonso, A., Kluska, A., Lewkowycz, A., Agarwal, A., Power, A., Ray, A., W arstadt, A., Kocurek, A. W., Safaya, A., Tazarv, A., Xiang, A., Parrish, A., Nie,...

    2025

  32. [43]

    SYNTCOMP/benchmarks: Repository of benchmarks for the Reactive Synthesis Competition (SYNT- COMP)

    SYNTCOMP. SYNTCOMP/benchmarks: Repository of benchmarks for the Reactive Synthesis Competition (SYNT- COMP). https://github.com/SYNTCOMP/benchmarks, 2025. Accessed: 2025-10-05

    2025

  33. [44]

    T., and Bing, L.Towards benchmarking and improving the temporal reasoning capability of large language models.arXiv preprint arXiv:2306.08952(2023)

    Tan, Q., Ng, H. T., and Bing, L.Towards benchmarking and improving the temporal reasoning capability of large language models.arXiv preprint arXiv:2306.08952(2023)

    2023 arXiv

  34. [45]

    T., and Bing, L.Towards benchmarking and improving the temporal reasoning capability of large lan- guage models

    Tan, Q., Ng, H. T., and Bing, L.Towards benchmarking and improving the temporal reasoning capability of large lan- guage models. InProceedings of the 61st Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers)(Toronto, Canada, July 2023), A. Ro...

    2023

  35. [46]

    Toles, M., Balwani, N., Singh, R., Rodriguez, V. G. S., and Yu, Z.Program synthesis dialog agents for interactive decision-making, 2025

    2025

  36. [47]

    Wang, X., Wei, J., Schuurmans, D., Le, Q., Chi, E., Narang, S., Chowdhery, A., and Zhou, D.Self-consistency improves chain of thought reasoning in language models, 2023

    2023

  37. [48]

    Wang, Y., and Zhao, Y.Tram: Benchmarking temporal reasoning for large language models.arXiv preprint arXiv:2310.00835(2023)

    2023 arXiv

  38. [49]

    V., Zhou, D., et al.Chain-of-thought prompting elicits reasoning in large language models.Advances in neural information processing systems 35(2022), 24824–24837

    Wei, J., W ang, X., Schuurmans, D., Bosma, M., Xia, F., Chi, E., Le, Q. V., Zhou, D., et al.Chain-of-thought prompting elicits reasoning in large language models.Advances in neural information processing systems 35(2022), 24824–24837

    2022

  39. [50]

    Xiong, S., Payani, A., Kompella, R., and Fekri, F.Large language models can learn temporal reasoning.arXiv preprint arXiv:2401.06853(2024)

    2024 arXiv

  40. [51]

    Y ang, A., Li, A., Y ang, B., Zhang, B., Hui, B., Zheng, B., Yu, B., Gao, C., Huang, C., Lv, C., Zheng, C., Liu, D., Zhou, F., Huang, F., Hu, F., Ge, H., Wei, H., Lin, H., Tang, J., Y ang, J., Tu, J., Zhang, J., Y ang, J., Y ang, J., Zhou, J., Zhou, J., Lin, J., Dang, K., Bao,...

    2025

  41. [52]

    XXX g": {

    Yao, S., Yu, D., Zhao, J., Shafran, I., Griffiths, T. L., Cao, Y., and Narasimhan, K.Tree of thoughts: deliberate problem solving with large language models. InProceedings of the 37th International Conference on Neural Information Processing Systems(Red Hook, NY, USA, 2023), N...

    2023

  42. [53]

    2 --END-- Fig. 14. Sample of a binary mod 3 DFA D.2 SHAPLEY Plots On Model Level and𝑅 2 Scores Model Time Step𝑅 2 AP Step𝑅 2 Claude Sonnet 3.5 0.497 0.507 Claude Sonnet 4.5 0.772 0.613 Qwen 0.349 0.271 GPT-4o 0.429 0.440 GPT-4o Mini 0.781 0.776 Table 4.𝑅 2 scores for each mode...

    2025

Pith tools

Reviewed August 4, 2026 · model on record in the stance chip above.