{"id":"6ff26da7-3063-43ef-9b87-5362bfb9654d","arxiv_id":"2607.21307","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"An LLM-based pipeline translated 23 Alzheimer's clinical trial protocols into Temporal Ensemble Logic, with back-translation semantic similarity suggesting—but not proving—that much of the temporal meaning is preserved.","lead":"This paper tests whether large language models can convert plain-English clinical trial protocols into formal logical formulas that computers can reason over. It reports that the round-trip translation kept most of the meaning for 23 Alzheimer's trials, but the formulas themselves were never directly checked.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Round-trip semantic similarity cannot validate TEL formulas because reverse-translation can fill or hallucinate content; the paper's own §5.3 concession makes the central fidelity claim unsupported.","rationale":"The reader identified the same load-bearing weakness: the fidelity evaluation validates reconstructed text, not the TEL formula. My read agrees and sharpens it with the paper's own hallucination example (NCT04308512 maskingInfo) and with the explicit §5.3 concession that embedding-based metrics cannot detect logic errors. This is an internal gap between the central claim and the evidence, not a disagreement with external consensus. The paper is honest about the limitation, includes a useful cross-trial off-diagonal baseline, and frames itself as preliminary. However, because the formulas are the purported output, a conditional verdict requiring direct formula-level validation is appropriate. I do not see a more severe flaw that would justify rejection: the workflow is reproducible in principle, the structured JSON intermediate representation is sensible, and the ablation experiments are a good start. The lack of released code/data with commit hashes and the absent formula-level evaluation both support the conditional recommendation. No ad hominem concerns; the issue is evidentiary, and the authors themselves flag the missing logic-level validation in §5.1 and §5.3.","tokens_in":10636,"tokens_out":3848,"duration_ms":46191,"concrete_test":"Directly validate a sample of generated TEL formulas at the logic level. Select 6–10 trials spanning similarity scores, and have two independent TEL experts (or an automated TEL parser/model checker) assess each formula against the original protocol's temporal constraints, encoding checks analogous to Q1–Q4 but applied to the formula itself: Are the modal operators correctly chosen? Are durations and offsets exact? Are temporal anchors and Boolean scoping preserved? Additionally, run a perturbation probe: take one formula, introduce single logic errors (replace □3m with ♢3m, change x+3m to x+15m, delete a conjunct), reverse-translate each corrupted version, and recompute semantic similarity. If corrupted formulas yield scores still above 0.8, the metric is insensitive to exactly the errors the paper admits it cannot detect. Report score distributions and expert agreement.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central claim — that CT-TEL maps narrative protocols to faithful TEL formulas — is supported only by a text-to-text proxy: the LLM reverse-translates a formula into a reconstructed protocol, and semantic similarity is computed between that reconstruction and the source. This does not check whether the formula itself has the correct temporal operators, durations, anchors, or Boolean structure. High text similarity can arise even when the intermediate formula is wrong, because the reverse-translating LLM has strong clinical priors and may fill in omitted or altered details from general knowledge. §5.3 documents exactly such behavior: the NCT04308512 reconstruction added a maskingInfo field absent from the original, yet scored 0.966 semantic similarity. The paper explicitly concedes in §5.3 that 'Embedding-based metrics cannot detect logic errors such as collapsed duration states, hallucinated fields, or incorrect temporal anchors.' Since the reported semantic scores (0.622–0.860) are measured on reconstructed text, not on the formulas' satisfaction semantics, they constitute an upper bound on formula fidelity rather than evidence of it. The human review also evaluated reconstructed protocols, not formulas. Thus the workflow's load-bearing assertion of 'rigorously validating the semantic fidelity' is unverified; the formulas themselves have never been directly checked against the source protocols.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proposes CT-TEL, a workflow that uses large language models (LLMs) to translate narrative clinical trial protocols from ClinicalTrials.gov into Temporal Ensemble Logic (TEL) formulas. The pipeline includes ontology mapping, temporal event extraction, four-step TEL formalization, and a back-translation evaluation in which an LLM reconverts the TEL formulas into natural-language protocol text. Fidelity is assessed by human/LLM rating and by lexical/semantic similarity between the original and reconstructed text. The authors report results on 23 Alzheimer's-disease medication trials, including sensitivity ablations and a cross-trial similarity baseline, and claim that the workflow 'rigorously validates' semantic fidelity and scales formal protocol representation.","tokens_in":10967,"tokens_out":3804,"duration_ms":40858,"significance":"If the central claim were supported, CT-TEL would be a valuable contribution: it offers a concrete, reproducible pipeline for turning free-text protocols into executable temporal-logic formulas, with potential downstream use in cohort simulation and model checking. The paper has real strengths: it uses genuine ClinicalTrials.gov data, makes prompts and structured outputs publicly available, includes a cross-trial baseline to contextualize similarity scores, and candidly discusses known failure modes. However, the validation strategy measures text-to-text similarity between original and back-translated protocols, not the correctness of the intermediate TEL formulas. The authors themselves state that embedding-based metrics cannot detect logic errors. As a result, the paper's load-bearing assertion of faithful formalization is not yet established by the reported evidence.","major_comments":[{"comment":"The fidelity evaluation measures lexical and semantic similarity between the original protocol text and the LLM-back-translated protocol text, not between the source and the TEL formula. The paper's own sentence in Section 4.1 concedes: 'Embedding-based metrics cannot detect logic errors such as collapsed duration states, hallucinated fields, or incorrect temporal anchors.' This is precisely the gap that matters for the claim that CT-TEL maps protocols to 'computable logical structures.' High text-reconstruction similarity can be achieved even when the intermediate formula is wrong, because the reverse-translating LLM can draw on clinical priors to fill in or alter content. Table 1's scores (e.g., 0.622–0.860) are therefore an upper bound on formula fidelity, not evidence of it.","section":"Section 3 / Section 4.1 (after Table 1)"},{"comment":"The human expert review also evaluated the reconstructed protocols against the original source, not the TEL formulas themselves. The consensus mean scores (1.89 human, 1.85 LLM) thus speak to the quality of the natural-language reconstruction, not to whether the formalization correctly encodes the trial's temporal requirements. To support the central claim, the authors need at least a direct sample-based review of formulas (e.g., experts checking that each formula's operators, anchors, and durations match the source), or a logic-level comparison such as model checking the original and reconstructed formulas against the same temporal event structure.","section":"Section 4.1, 'Human and LLM-Based Review'"},{"comment":"The masking experiment illustrates the same problem. When ontological labels are replaced with opaque placeholders, back-translation similarity drops, as expected, because the reverse-translating LLM loses clinical context. But the authors correctly note that the underlying logical structure might still be accurate. This is exactly the point: the reported semantic scores respond to surface vocabulary, not to the correctness of temporal operators, Boolean structure, or quantifier scoping. The experiment therefore does not validate the formulas; it demonstrates the metric's sensitivity to surface form. The paper needs a separate, logic-level evaluation to substantiate the claim that the formulas are faithful.","section":"Section 5.1, 'Concept-term masking experiment'"},{"comment":"The worked example for NCT04179721 asserts that the back-translation 'confirms the semantic fidelity of the automated formalization.' This is circular: the back-translation is generated from the very formula it is supposed to validate, and the text is then compared to the source. Without an independent check that the TEL formula's temporal structure (e.g., the 3-month box operator, the 1-month diamond windows, the existential anchor x) matches the protocol's actual requirements, the example is illustrative but not evidential.","section":"Section 4, 'Example: From Canonical Formula to Protocol Narrative' (Eq. 1)"}],"minor_comments":[{"comment":"The abstract and introduction describe the validation as 'rigorous,' but Section 4.1 and Section 5.3 acknowledge that the current metrics cannot detect logic-level errors. Consider softening the wording to 'preliminary' or 'text-level' fidelity to align the claims with the evidence.","section":"Abstract / Section 1"},{"comment":"The phrase 'represented as anatomic proposition p' appears to be a typo for 'atomic proposition p.' Please correct.","section":"Section 2, 'Ensemble Logic'"},{"comment":"The description of the cross-trial similarity matrix is clear, but the text would benefit from stating explicitly that the off-diagonal baseline is computed on text reconstructions and therefore shares the same limitation of not reflecting formula correctness.","section":"Section 3, 'Evaluation of Translation Fidelity'"},{"comment":"The tables are informative, but the captions should note that the similarity scores are text-level measures, not formula-level validations, to prevent readers from interpreting them as direct evidence of logical fidelity.","section":"Table 1 / Table 2"},{"comment":"The discussion of collapsed duration states is a useful failure analysis, but it would be stronger with a concrete example showing the original text, the generated formula fragment, and the incorrect collapsed form. As written, the reader cannot assess the severity or frequency of this failure mode.","section":"Section 5.3, 'Temporal distortion of nested constraints'"}],"recommendation":"major_revision","confidential_remarks":"The paper is honest and well-structured, but the central claim—that CT-TEL produces faithful TEL formalizations—is currently supported only by a text-to-text proxy. The authors themselves identify the missing logic-level validation. I recommend requiring a direct evaluation of formula correctness (e.g., expert formula review on a subset, or model-checking-based comparison of original and reconstructed formulas) before the paper can claim rigorous validation. The claims in the abstract and introduction should be scaled back if such evaluation is not added."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The genuinely new thing here is the pipeline: LLMs taking ClinicalTrials.gov JSON through structured event arrays to TEL formulas, with provenance tracking and a six-tier library. That's a real engineering contribution for a real bottleneck. They ran it on 23 ADRD trials, and the masking ablation and cross-trial off-diagonal baseline are thoughtful touches.\n\nThe soft spot is the evaluation. The forward translation is tested only by reverse-translating the formula back to text and comparing embeddings to the source. That tells you the round trip preserved text similarity, not that the TEL formula has the right temporal operators, anchors, or Boolean structure. The paper's own example of NCT04308512 is telling: the reconstruction added a maskingInfo field absent from the original, yet scored 0.966 semantic similarity. And §5.3 concedes outright that 'Embedding-based metrics cannot detect logic errors such as collapsed duration states, hallucinated fields, or incorrect temporal anchors.' That is a direct admission that the central evidence does not support the load-bearing claim of 'rigorously validating the semantic fidelity.' The human review also examined reconstructed protocols, not the formulas.\n\nThere's a circularity issue too: the same LLM family does forward translation, back-translation, and embedding evaluation, so high scores partly reflect self-consistency. The masking experiment shows the metric is sensitive to surface cues. I also noticed no error bars or per-module variance, and the GitHub link lacks a commit hash or archival deposit.\n\nTo be fair, the authors are unusually honest. They explicitly call for logic-level validation via model-checking in §5.3 and future work. For a preliminary workflow paper, this is a decent start. The mismatch is between the abstract's confident language and what the evaluation can actually support.\n\nI'd send this to peer review, but with teeth: either add formula-level validation—model-checking against a TES, or at least manual formula review against the source for a sample—or scale the claims back to what the round-trip metric can support. The reader's conditional verdict is about right. People working on LLM-to-formal-language translation or clinical trial formalization would find value in this as a case study in evaluation pitfalls, but they shouldn't cite it as evidence that TEL formulas are correct.","headline":"CT-TEL is a useful preliminary pipeline for getting clinical trial text into TEL, but the round-trip similarity metric doesn't validate the formulas, and the paper's own §5.3 concession makes that clear.","tokens_in":11382,"tokens_out":1874,"would_cite":true,"duration_ms":21247,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["03B44","68Q60","68T50"],"pacs":[],"model":"deepseek-v4-flash","headline":"LLM-driven workflow translates narrative clinical trial protocols into Temporal Ensemble Logic formulas, using back-translation to show the formal versions retain meaning.","keywords":["clinical trial protocols","Temporal Ensemble Logic","large language models","back-translation","semantic similarity","formal representation","cohort simulation","model checking"],"falsifier":"Run a model-checking engine on the generated TEL formulas and compare satisfaction sets against the intended clinical events from the original protocol timelines; if a formula admits or excludes a patient cohort that the original narrative would not, the fidelity claim for that trial is falsified.","tokens_in":10585,"feed_emoji":"🩺","tokens_out":4108,"duration_ms":41303,"temperature":0.7,"pith_summary":"This paper tries to establish that large language models can convert narrative clinical trial protocols from a public trial registry into Temporal Ensemble Logic (TEL) formulas at scale, and that the conversion is faithful. The authors build CT-TEL, a pipeline that formalizes 23 Alzheimer's-disease medication trials into TEL and then uses a separate LLM pass to translate the formulas back into natural language. The back-translated protocols are compared to the source texts using human expert ratings, LLM ratings, and lexical/semantic similarity metrics. The scores suggest the formalized versions retain the temporal meaning of the original protocols. If this holds, it would remove the manual-encoding bottleneck that has prevented logic-based reasoning from being applied to large collections of trial records.","feed_headline":"LLM pipeline maps 23 clinical trials to temporal logic","feed_subtitle":"A back-translation step checks that the formalized protocols still match the original text semantically.","key_machinery":"The central mechanism is Temporal Ensemble Logic (TEL), a temporal logic whose formulas combine atomic propositions with shift operators (p at offset t), box operators (condition holds continuously for duration t), diamond operators (event occurs within window t), Boolean connectives, and quantifiers over time anchors. The workflow uses TEL as an intermediate representation: an LLM compiles narrative protocol text into TEL formulas, a second LLM reconstructs trial-protocol modules from the formulas, and fidelity is scored by comparing the reconstruction to the original. The bidirectionality of TEL is what makes the back-translation check possible.","core_discovery":"The paper's central discovery is that a round-trip LLM pipeline can produce TEL formulas from real clinical trial text with measurable semantic fidelity. Across 23 trials, semantic similarity between original and reverse-translated module text averaged 0.622 for conditions and 0.860 for eligibility, with diagonal entries in cross-trial similarity matrices clearly exceeding off-diagonal baselines. The authors interpret these results as evidence that the intermediate TEL formulas are faithful logical models, enabling downstream model-checking and cohort simulation.","pith_inferences":["The semantic-similarity proxy is text-to-text; it does not verify the TEL formula's logical structure. A model-checking comparison of satisfaction sets would be a stricter test, as the paper itself notes.","The masking experiment suggests that ontology labels contribute to surface similarity but may not be needed for logical correctness, implying the fidelity metric conflates terminology grounding with temporal accuracy.","If scaled, this approach could make trial protocols directly queryable, but the 'implicit assumption injection' failure mode means hallucinated fields may propagate into formal models even when semantic scores look high.","A natural extension would be to test the pipeline on trials with more complex nested temporal constraints, where the paper reports temporal distortion occurs."],"forward_implications":["Automated generation of TEL formulas removes the manual encoding bottleneck, making logic-based trial representation practical for large registries.","TEL formulas can be fed into model-checking engines to simulate eligibility cohorts and test recruitment strategies against real-world data.","Self-controlled case series could use these formulas to construct synthetic control arms from real-world patient timelines.","The workflow could extend beyond Alzheimer's disease trials to other therapeutic areas sharing the same protocol schema.","Cross-LLM results suggest the pipeline is not tied to a single model, though not all models can execute the formal-synthesis prompts."],"fun_headline_variants":["LLM round-trip turns trial text into verifiable logic","23 clinical trials formalized with LLM back-translation","AI pipeline converts trial protocols to temporal logic","Back-translation validates LLM-generated trial logic"],"cache_read_input_tokens":2304,"weakest_assumption_plain":"The paper's central assumption is that high semantic similarity between the original text and the LLM's back-translation of the TEL formula proves the formula itself is logically faithful; but embedding-based similarity cannot detect wrong temporal anchors, collapsed duration states, or hallucinated fields, as the paper itself concedes.","fun_headline_variants_meta":{"raw":{"variants":["LLM round-trip turns trial text into verifiable logic","23 clinical trials formalized with LLM back-translation","AI pipeline converts trial protocols to temporal logic","Back-translation validates LLM-generated trial logic"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000243,"raw_usage":{"total_tokens":1323,"prompt_tokens":661,"completion_tokens":662,"prompt_tokens_details":{"cached_tokens":256},"prompt_cache_hit_tokens":256,"prompt_cache_miss_tokens":405,"completion_tokens_details":{"reasoning_tokens":599}},"tokens_in":405,"tokens_out":662,"duration_ms":6909,"temperature":1.0,"reasoning_tokens":599,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-01T07:49:13.356106+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Run a model-checking engine on the generated TEL formulas and compare satisfaction sets against the intended clinical events from the original protocol timelines; if a formula admits or excludes a patient cohort that the original narrative would not, the fidelity claim for that trial is falsified.","supporting_citations":[],"review_version":1}