{"id":"da8019e9-4ed5-4c50-afaf-90d27ba918af","arxiv_id":"2505.00610","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":5.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":1,"one_line_summary":"A logic-guided LLM framework that answers free-form questions about MCTS plans reports large gains in FactCC and BERTScore over bare LLMs in a paratransit planning testbed.","lead":"This paper combines large language models with computation tree logic to explain Monte Carlo Tree Search decisions in a paratransit planning domain. The authors report that adding a logic and knowledge-retrieval layer makes LLM-generated explanations substantially more factually consistent than asking the LLM directly.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"FactCC and BERTScore are reference-based metrics; with no stated source document and no scoring of the logic layer, Table 1 does not establish factual consistency.","rationale":"The reader's conditional verdict is appropriate: the framework is plausible and the comparison to bare LLMs is a fair baseline, but the extended abstract provides no released code, no error bars, and no reliability analysis of the manually prepared benchmark. My concern sharpens the required condition rather than changing the verdict: even if the Query-Classification and Logic-Generator LLMs were perfect, the reported metrics would still fail to demonstrate factual consistency unless the FactCC source document is defined to be the MCTS-derived evidence rather than the reference narrative. The manually prepared 'correct evidence variables and logic' in Sec. 3 are a valuable resource; the paper should use them to report classification accuracy and logic-formula match rate, which would directly address the reader's weakest assumption. The paper's framework is testable, and the 620-query benchmark plus the 34-chunk knowledge base are concrete contributions, but the current evidence does not support the abstract's claim that the framework 'ensures' factual consistency. The conditionality should remain, with the explicit condition that the evaluation protocol be corrected and the intermediate logic layer be scored.","tokens_in":4668,"tokens_out":5535,"duration_ms":60046,"concrete_test":"Re-run the Table 1 evaluation with a defined FactCC source: for each of the 620 queries, construct the source document solely from the Logic Scorer's returned evidence values (variables, node values, and CTL comparison results) and the retrieved knowledge chunks, with no reference narrative included; compute FactCC and BERTScore against the same reference narratives. If the framework's FactCC scores drop materially below the reported 67.88% (Llama) and 72.12% (GPT-4o), the reported factual-consistency gains are an artifact of using the reference narrative as the source and do not establish consistency with the MCTS evidence.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The paper's central claim rests on Table 1, which reports FactCC and BERTScore gains of 2.40x/1.59x and 7.92x/1.70x for the Llama3.1 and GPT-4o backbones. These metrics cannot support the claim of improved factual consistency unless the source document used by FactCC is specified and appropriate. FactCC is a summarization entailment classifier: it predicts whether a generated summary is consistent with a given source article. The paper never states what source document is fed to FactCC. If the source is the manually prepared reference narrative paragraph (the only per-query text described in Sec. 3), then FactCC measures paraphrase/entailment closeness to the reference, not consistency with the MCTS tree or with the Logic Scorer's computed evidence. BERTScore is likewise a reference-based semantic similarity metric and cannot distinguish a confidently wrong explanation from a correct one. In addition, the components intended to guarantee logical fidelity—the Query-Classification LLM with 26 predefined types and the Logic Generator producing CTL statements, both described in Sec. 2 under 'Logic Generator and Parser'—are never evaluated. The paper reports no classification accuracy, no logic-formula match rate, and no ablation against the manually prepared 'correct evidence variables and logic' mentioned in Sec. 3. A query can therefore be misclassified or mistranslated, the Logic Scorer can compute evidence for a different question, and the final LLM can produce a fluent, high-scoring explanation of that different question without any reported metric revealing the failure. The framework's central mechanism is hence unverified by the quantitative results as presented.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proposes a framework that combines large language models (LLMs) with Computational Tree Logic (CTL) and retrieval-augmented generation (RAG) to generate natural-language explanations of Monte Carlo Tree Search (MCTS) decisions in a paratransit planning domain. User queries are classified into predefined types, translated into logic/variable statements, evaluated against the MCTS tree via a logic scorer, and then combined with retrieved domain knowledge for final answer generation. The authors evaluate the framework on 620 manually prepared queries, comparing FactCC and BERTScore against bare LLM baselines (GPT-4, GPT-4o, Llama3.1) and report large improvements with their framework.","tokens_in":4900,"tokens_out":2682,"duration_ms":28205,"significance":"If the empirical claims hold, the paper makes a useful contribution by showing that grounding LLM-generated explanations in symbolic evidence from the search tree can improve factual consistency over ungrounded LLM generation. The framework's decomposition into query classification, logic generation, tree-based scoring, and knowledge retrieval is a principled architecture for explainable sequential planning. The authors also put substantial effort into manually preparing 620 queries with correct evidence variables and reference narratives. However, the current evaluation does not yet substantiate the central factual-consistency claim because the reference documents used by the metrics are unspecified and the correctness of the logic-translation layer is not assessed.","major_comments":[{"comment":"The FactCC metric requires a source document against which generated text is checked for factual consistency, but the paper never states what source is used. If the source is the manually prepared reference narrative paragraph, then FactCC measures paraphrase/entailment closeness to the reference, not consistency with the MCTS search tree or with the logic scorer's computed evidence. The central claim of improved factual accuracy therefore rests on an unspecified and potentially inappropriate metric setup. Please specify the source document and, ideally, evaluate consistency against the tree-derived evidence directly.","section":"§3, Table 1"},{"comment":"The correctness of the entire pipeline depends on the Query-Classification LLM assigning one of 26 query types and the Logic Generator producing correct variable/CTL statements, yet no accuracy for these components is reported. A misclassified query or an incorrect logic formula causes the scorer to compute evidence for a different question while the final LLM still produces a fluent, confidently worded explanation. The paper should report classification accuracy, logic-formula match rates, or at least an ablation that replaces the generated logic with the manually prepared correct logic mentioned in §3.","section":"§2, 'Logic Generator and Parser'"},{"comment":"All quantitative claims are based on single point estimates with no error bars, confidence intervals, or significance tests, despite each query being repeated three times. The phrases 'significant improvements' and 'consistently outperformed' are not supported without variance information or paired statistical tests. Reporting standard errors or paired tests across the three repetitions is necessary to support the strength of the claims.","section":"§3, 'Factual Consistency Results and Discussions'"}],"minor_comments":[{"comment":"The meaning of the @1 and @3 columns is never defined in the text or table caption; please clarify what these rank cutoffs refer to.","section":"Table 1"},{"comment":"The sentence 'our framework consistently outperformed the basic LLMs across all categories' is not backed by category-level results in Table 1, which only reports aggregate scores; either add category-level numbers or temper the claim.","section":"§3"},{"comment":"Reference [18] is the original Llama paper, but the text cites it for Llama3.1; please update to the Llama 3.1 technical report.","section":"References"},{"comment":"The paper does not release the 620 queries, the reference narratives, or the evaluation code, which limits reproducibility; a supplementary release would strengthen the paper.","section":"§3"},{"comment":"There are minor typographical and stylistic issues, such as the section title '3 EVALUATIONS' and the lowercase 'our framework' at the beginning of a sentence in §3.","section":"General"}],"recommendation":"major_revision","confidential_remarks":"The paper is an extended abstract, and the evaluation gaps I identify (unspecified FactCC source, unassessed logic-translation accuracy, missing statistical significance) are substantial but fixable within the scope of a revision, especially if supplemented by a small ablation or additional metadata. The framework idea is promising and worth another round, but the current empirical evidence does not yet support the strong factual-consistency claims made in the abstract."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The short version: this is a genuine integration of CTL-based evidence with LLM explanation generation, and the measured gains over bare LLMs are large enough to take seriously. The evaluation, though, is thin in exactly the places that would confirm the framework's core claim.\n\nThe new material is real. The CTL scoring mechanism comes from the authors' prior work, but the LLM query classification into 26 types, few-shot logic generation, RAG retrieval, and the systematic comparison against GPT-4/GPT-4o/Llama3.1 are all new. The reported 2.4x/1.59x FactCC and 7.92x/1.70x BERTScore improvements are not the kind of numbers you get from noise, so something about the pipeline is working.\n\nNow the soft spots. The biggest one is that FactCC is a reference-based entailment metric, and the paper never states what source document is fed to it. If the source is the manually prepared reference narrative, then FactCC is measuring paraphrase closeness to a human-written ideal, not consistency of the explanation with the MCTS tree or the computed evidence. That matters because the framework's whole pitch is that logic grounds the explanation in the search tree. Relatedly, the query-classification and logic-generation layers are never evaluated for accuracy. A misclassified query can produce fluent, confident, wrong explanations, and no metric in Table 1 would reveal it because the final LLM can still produce a high-scoring narrative. The missing error bars, the non-release of the 620 queries and reference narratives, and the lack of ablations against a CTL-only or RAG-only variant make these concerns hard to resolve from the paper alone. The abstract's 'ensures' is also too strong given the evidence.\n\nFor a 3-page extended abstract, this is acceptable as an early report. The architecture is sensible, the authors are not hiding their manual benchmark prep, and the comparison against bare LLMs is a fair baseline choice. But the paper would need a released benchmark, a specified FactCC source, a logic-layer accuracy check, and some ablations before the factual-consistency claim is fully supported.\n\nThis is for people building LLM explainers for planners and for the formal-XAI crowd. It deserves a serious referee rather than a desk reject; the referee should push for the missing artifacts and diagnostics.","headline":"Real LLM+CTL integration with large reported gains, but the evaluation doesn't yet pin the improvement to the logic layer.","tokens_in":5520,"tokens_out":2209,"would_cite":true,"duration_ms":23842,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"Converting user questions about MCTS into computational-tree-logic statements, computing evidence from the search tree, then letting an LLM phrase the answer yields far more factually consistent explanations than asking the LLM directly.","keywords":["Explainable AI","Monte Carlo Tree Search","Sequential Planning","Large Language Models","Computational Tree Logic","Factual Consistency","Retrieval-Augmented Generation","Paratransit Planning"],"falsifier":"Run the pipeline with the logic-and-scorer stage replaced by a stub that returns random evidence while keeping the same LLM prompts; if FactCC and BERTScore do not drop substantially, the logic layer is not the cause of the reported gains.","tokens_in":4438,"feed_emoji":"🤖","tokens_out":13800,"duration_ms":119503,"temperature":0.7,"pith_summary":"This paper tries to establish that a large language model can explain Monte Carlo Tree Search (MCTS) planning decisions accurately if, before it writes the explanation, a logic layer converts the user's question into a formal statement, computes the corresponding evidence from the search tree, and retrieves relevant domain knowledge. On a paratransit routing testbed with 620 manually prepared queries, the framework lifts the factual-consistency score at rank 3 by a factor of 2.40 for Llama3.1 and 1.59 for GPT-4 compared with the same models answering directly. The larger point is that grounding LLM-generated text in verifiable search-tree evidence could make sequential-planning AI easier to trust and audit, which is precisely the barrier the paper addresses.","feed_headline":"Logic-guided LLMs give 2.4x more factual MCTS explanations","feed_subtitle":"Grounding LLM answers in search-tree logic lifts factual consistency from 25.8% to 67.9%.","key_machinery":"The load-bearing object is the three-level hierarchical evidence structure that sits between the user query and the final text. Level one extracts base variables directly from a single tree node; level two derives aggregated quantities across nodes at different depths or branches; level three uses Computation Tree Logic (CTL, a branching-time temporal logic for tree-like state spaces) to express and model-check comparisons between branches. A query translator fixes which variables and logic formula apply, a set of scorer functions computes the numeric or boolean evidence, and that evidence—together with retrieved knowledge—is what the final LLM is instructed to paraphrase. The framework's factual-consistency claim rests on this separation: the numbers the explanation cites are computed, not guessed.","core_discovery":"The central claim, stated as the authors would state it, is that a natural-language explanation of an MCTS decision should be assembled from evidence rather than generated from the model's prior. The framework routes each user question through a query classifier (into one of 26 predefined types), a logic generator that emits a computational-tree-logic statement and variable structure, a scorer that evaluates that logic directly on the MCTS tree, and a retrieval step that pulls domain knowledge from a small knowledge base. Only then does a question-answering LLM phrase the final answer. In the reported experiments, this ordering raises FactCC at rank 3 from 34.62% to 83.27% for Llama3.1 and from 51.15% to 81.35% for GPT-4, with BERTScore at rank 3 climbing from 12.31% to 97.50% for Llama3.1. The authors conclude that basic LLMs are not sufficiently factually consistent for MCTS explanation on their own, and that the logic-guided pipeline closes the gap.","pith_inferences":["A separate measurement of logic-generation accuracy would tell us how much of the remaining gap to a perfect factual-consistency score is translation error rather than narrative error; our reading suggests most of it is translation, because the final LLM is given the exact evidence.","A stricter deployment would attach each generated sentence to its source evidence variable or knowledge chunk, turning the reported scores from a test-set average into a per-explanation guarantee.","The same 'formalize the question, compute the answer, then phrase it' pattern could be applied to explain other black-box sequential decision-makers, such as value networks or policy networks, wherever reachability and avoidance properties can be checked with temporal logic."],"forward_implications":["Users can re-derive each number in an explanation directly from the MCTS tree, because the scored evidence is part of the pipeline input rather than a paraphrase of the model's memory.","The same architecture transfers to any tree-based planner whose underlying process is an MDP, since the 26 query types and three evidence levels are defined over the search tree, not over paratransit specifics.","Explanations become interactive: because follow-up queries are classified and scored in the same way, a user can drill into a plan without the LLM drifting from the record.","With the stronger Llama3.1 backbone, the framework's factual-consistency score at rank 3 reaches 83.27%, indicating the gap between generated and reference explanations narrows substantially once the evidence is computed."],"supporting_citations":[{"why":"Establishes the core idea of explaining MCTS decisions through Computation Tree Logic, which this framework builds on as its evidence layer.","marker":"[2]"},{"why":"Supplies the CTL formalism and model-checking semantics used to evaluate logic-comparison evidence on the search tree.","marker":"[7]"},{"why":"Defines MCTS, the algorithm whose decisions the framework is designed to explain.","marker":"[10]"},{"why":"Provides the FactCC metric used to score the factual consistency of the generated explanations.","marker":"[11]"},{"why":"Provides BERTScore, the semantic-relevance metric used alongside FactCC in evaluation.","marker":"[21]"},{"why":"Documents GPT-4/GPT-4o, the backbone models used both as baselines and inside the framework.","marker":"[1]"},{"why":"Documents Llama3.1, the other backbone model used as baseline and inside the framework.","marker":"[18]"},{"why":"Formulates the dynamic vehicle-routing MDP used to build the paratransit planning testbed.","marker":"[9]"},{"why":"Supplies the scorer-function approach for evaluating logic properties, adapted here to MCTS tree evidence.","marker":"[3]"}],"fun_headline_variants":["Logic-guided LLMs lift MCTS factuality from 26% to 68%","Logic-grounded LLMs outperform plain LLMs on MCTS explanations","Logic-routed LLMs explain MCTS with factual evidence"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The framework assumes the query-classification and logic-generation steps translate every free-form user question into the correct one of 26 types and a correct logic statement; if that translation is wrong, the scorer computes evidence for a different question while the final explanation still sounds confident.","fun_headline_variants_meta":{"raw":{"variants":["Logic-guided LLMs lift MCTS factuality from 26% to 68%","Logic-grounded LLMs outperform plain LLMs on MCTS explanations","Logic-routed LLMs explain MCTS with factual evidence"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.001313,"raw_usage":{"total_tokens":5331,"prompt_tokens":904,"completion_tokens":4427,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":520,"completion_tokens_details":{"reasoning_tokens":4366}},"tokens_in":520,"tokens_out":4427,"duration_ms":30001,"temperature":1.0,"reasoning_tokens":4366,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-16T04:37:52.286122+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Run the pipeline with the logic-and-scorer stage replaced by a stub that returns random evidence while keeping the same LLM prompts; if FactCC and BERTScore do not drop substantially, the logic layer is not the cause of the reported gains.","supporting_citations":[{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Establishes the core idea of explaining MCTS decisions through Computation Tree Logic, which this framework builds on as its evidence layer."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Supplies the CTL formalism and model-checking semantics used to evaluate logic-comparison evidence on the search tree."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Formulates the dynamic vehicle-routing MDP used to build the paratransit planning testbed."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Supplies the scorer-function approach for evaluating logic properties, adapted here to MCTS tree evidence."}],"review_version":1}