ai-research-survey

scan.json (25674B)

---

 {
   "paper": {
     "title": "Logically Constrained Decoding",
     "authors": ["Franklin Ma", "Alan J. Hu"],
     "year": 2025,
     "venue": "MathNLP 2025 (Workshop at ACL)",
     "doi": "10.18653/v1/2025.mathnlp-main.11"
   },
   "scan_version": 2,
   "active_modules": ["experimental_rigor", "data_leakage"],
   "methodology_tags": ["benchmark-eval"],
   "key_findings": "Logically constrained decoding extends constrained decoding from syntactic to logical constraints, demonstrated on chess and propositional resolution proofs. In chess, unconstrained LLMs made illegal moves in 897/900 games while constrained LLMs made zero illegal moves. For resolution proofs, constrained decoding achieved 100% correct proof generation on pigeonhole problems of size 1-2, where unconstrained models scored 0% on size 2. The technique works across 9 different open-source LLM families with minimal latency overhead.",
   "checklist": {
     "artifacts": {
       "code_released": {
         "applies": true,
         "answer": true,
         "justification": "GitHub repository URL provided: https://github.com/terwo/logically-constrained-decoding (§4, footnote 8)."
       },
       "data_released": {
         "applies": true,
         "answer": true,
         "justification": "Pigeonhole problem encodings are fully specified in Appendix B, and chess uses the standard Stockfish engine. The SAT encodings are loaded via PySAT. The data is reproducible from the specification."
       },
       "environment_specified": {
         "applies": true,
         "answer": false,
         "justification": "Hardware is described (Dell EMC C4140, NVIDIA Tesla V100 16/32GB) and HuggingFace Transformers is mentioned, but no requirements.txt, Dockerfile, or specific library versions are provided in the paper."
       },
       "reproduction_instructions": {
         "applies": true,
         "answer": false,
         "justification": "No step-by-step reproduction instructions are provided in the paper. The GitHub link is given but no README or reproduction guide is described."
       }
     },
     "statistical_methodology": {
       "confidence_intervals_or_error_bars": {
         "applies": true,
         "answer": true,
         "justification": "Figure 2 shows whiskers representing 1 standard deviation for chess game results across 20 games per condition."
       },
       "significance_tests": {
         "applies": true,
         "answer": false,
         "justification": "No statistical significance tests are reported. Claims of improvement are based on raw comparisons (e.g., 897/900 vs 0/900 illegal moves, 0% vs 100% proof accuracy) without formal tests."
       },
       "effect_sizes_reported": {
         "applies": true,
         "answer": true,
         "justification": "Effect sizes are implicitly clear from absolute numbers: 897/900 games ended by illegal move without constraints vs 0/900 with constraints. For proofs, 0% vs 100% success rates. These provide full context for the magnitude of improvement."
       },
       "sample_size_justified": {
         "applies": true,
         "answer": false,
         "justification": "No justification is given for why 20 games per condition (chess) or 50 trials (proofs) were chosen. No power analysis is discussed."
       },
       "variance_reported": {
         "applies": true,
         "answer": true,
         "justification": "Standard deviation whiskers are shown in Figure 2 for chess results across 20 games. Figure 5 reports average tokens per second."
       }
     },
     "evaluation_design": {
       "baselines_included": {
         "applies": true,
         "answer": true,
         "justification": "Each model is compared in unconstrained vs constrained conditions, serving as its own baseline. This is the natural comparison for the proposed technique."
       },
       "baselines_contemporary": {
         "applies": true,
         "answer": true,
         "justification": "Models tested include recent releases: Qwen2.5 (2025), Gemma3 (2025), Phi-4-mini (2025), Llama 3.1 (2024), Ministral-8B (2024). Stockfish 17.1 is the latest version."
       },
       "ablation_study": {
         "applies": false,
         "answer": false,
         "justification": "The system has one core component (the symbolic constraint engine). The comparison is constrained vs unconstrained, which is the natural evaluation, not an ablation."
       },
       "multiple_metrics": {
         "applies": true,
         "answer": true,
         "justification": "For chess: number of legal moves before illegal move and game outcomes. For proofs: proof correctness rate. For performance: tokens per second. Multiple metrics across the two domains."
       },
       "human_evaluation": {
         "applies": false,
         "answer": false,
         "justification": "Human evaluation is irrelevant here — correctness of chess moves and resolution proofs is formally verifiable by machine."
       },
       "held_out_test_set": {
         "applies": false,
         "answer": false,
         "justification": "Not applicable — the evaluation uses online game play and proof generation, not a static dataset with train/test splits."
       },
       "per_category_breakdown": {
         "applies": true,
         "answer": true,
         "justification": "Results are broken down per model (9 models), per difficulty level (5 Stockfish settings), and per pigeonhole size (1, 2, 3) in Figures 2-4 and Table 1."
       },
       "failure_cases_discussed": {
         "applies": true,
         "answer": true,
         "justification": "The paper discusses failures: unconstrained models making illegal chess moves (Figure 1 example), ChatGPT-5 making an unsound deduction in resolution proofs, scalability issues with size-3 pigeonhole proofs, and the constraint engine's inability to complete experiments for large proofs."
       },
       "negative_results_reported": {
         "applies": true,
         "answer": true,
         "justification": "The paper reports that the constraint engine for resolution proofs does not scale to larger proofs — throughput drops from 24.7 to 5.5 tokens/sec as proof length grows (§4.3). They also could not complete size-3 experiments without an optimization that relaxes minimal invasiveness."
       }
     },
     "claims_and_evidence": {
       "abstract_claims_supported": {
         "applies": true,
         "answer": true,
         "justification": "The abstract claims proof-of-concept implementations for chess and resolution proofs with constrained decoding. These are supported by the experimental results in §4.1-4.3."
       },
       "causal_claims_justified": {
         "applies": true,
         "answer": true,
         "justification": "The causal claim is that logically constrained decoding prevents illegal outputs. This is justified by the controlled comparison (same models, same prompts, with/without constraint) and the formal guarantee that the constraint engine blocks illegal tokens."
       },
       "generalization_bounded": {
         "applies": true,
         "answer": true,
         "justification": "The paper explicitly frames results as 'proof-of-concept' and limits claims to chess and propositional resolution. The Limitations section acknowledges they only tested open-source models and smaller sizes, and that results may not directly apply to proprietary frontier models."
       },
       "alternative_explanations_discussed": {
         "applies": true,
         "answer": true,
         "justification": "The Limitations section discusses that prompt variations could affect results, that constraining output may limit reasoning ability (citing Banerjee et al. 2025), and that the chess experiments did not allow unconstrained thinking which may have affected play quality."
       },
       "proxy_outcome_distinction": {
         "applies": true,
         "answer": true,
         "justification": "The paper's claims match the granularity of its measurements: it measures illegal moves and proof correctness and claims exactly that — no broader proxy gap exists. It explicitly does not claim to produce a superior chess engine."
       }
     },
     "setup_transparency": {
       "model_versions_specified": {
         "applies": true,
         "answer": true,
         "justification": "Specific model names with sizes are given: Qwen2.5-7B-Instruct, Qwen2.5-14B-Instruct, Qwen2.5-32B-Instruct, Llama-3.1-8B-Instruct, Gemma-3-4b-it, Gemma-3-12b-it, Gemma-3-27b-it, Phi-4-mini-instruct, Ministral-8B-Instruct-2410. These are specific enough to identify exact model checkpoints."
       },
       "prompts_provided": {
         "applies": true,
         "answer": true,
         "justification": "Full prompts for both chess (Figure 6) and resolution proofs (Figures 7-8) are provided in Appendix A."
       },
       "hyperparameters_reported": {
         "applies": true,
         "answer": true,
         "justification": "Appendix D states temperature=1.0 and defaults from HuggingFace Transformers. Max token limits per pigeonhole size are given in Table 2. Precision settings (FP32 for Gemma3, FP16 for others) and quantization (8-bit for Gemma3 and Qwen2.5-32B) are specified."
       },
       "scaffolding_described": {
         "applies": false,
         "answer": false,
         "justification": "No agentic scaffolding is used. The system is a constrained decoding engine operating at the token level during generation."
       },
       "data_preprocessing_documented": {
         "applies": true,
         "answer": true,
         "justification": "The pigeonhole SAT encoding is fully specified in Appendix B with the DIMACS format. Chess setup details are given (Stockfish 17.1, depth-15, 5 difficulty levels, 20 games per condition). Tokenization handling is documented in Appendix C."
       }
     },
     "limitations_and_scope": {
       "limitations_section_present": {
         "applies": true,
         "answer": true,
         "justification": "A dedicated 'Limitations' section is present after §5, with substantive discussion spanning multiple paragraphs."
       },
       "threats_to_validity_specific": {
         "applies": true,
         "answer": true,
         "justification": "Specific threats discussed: prompt notation variations (e.g., using + vs ∨ for OR), limitation to open-source models, limitation to smaller models due to compute constraints, chess experiments not allowing unconstrained thinking tokens, resolution implementation not scaling to larger proofs."
       },
       "scope_boundaries_stated": {
         "applies": true,
         "answer": true,
         "justification": "The paper explicitly states scope boundaries: 'We can modify and perform experiments only on open-source language models, so it is unclear to what degree our results can be applied to proprietary, frontier models.' Also: 'we were limited by our available computing resources to using smaller models.' The paper frames results as proof-of-concept, not general claims."
       }
     },
     "data_integrity": {
       "raw_data_available": {
         "applies": true,
         "answer": false,
         "justification": "No raw experimental data (game logs, proof transcripts, per-trial results) is made available. Only aggregate results in figures and tables."
       },
       "data_collection_described": {
         "applies": true,
         "answer": true,
         "justification": "The data collection procedure is well-described: chess games against Stockfish 17.1 at 5 difficulty levels, 20 games per condition (10 as White, 10 as Black), maximum 10 tokens per move. Resolution proofs: 50 trials per condition for sizes 1-2, 20 for size 3."
       },
       "recruitment_methods_described": {
         "applies": false,
         "answer": false,
         "justification": "No human participants. Data source is standard benchmark problems (pigeonhole) and chess engine play."
       },
       "data_pipeline_documented": {
         "applies": true,
         "answer": true,
         "justification": "The pipeline is straightforward and documented: generate move/proof step with LLM → check legality → update world model state → continue. The constraint engine's operation is described in §3 with pseudocode in §2.3."
       }
     },
     "conflicts_of_interest": {
       "funding_disclosed": {
         "applies": true,
         "answer": true,
         "justification": "Acknowledgements section states: 'This research was funded through an Undergraduate Summer Research Award and a Discovery Grant, both from the Natural Sciences and Engineering Research Council of Canada (NSERC).' Also mentions UBC Advanced Research Computing."
       },
       "affiliations_disclosed": {
         "applies": true,
         "answer": true,
         "justification": "Authors are from Department of Computer Science, University of British Columbia. No commercial product is being evaluated, so there is no affiliation conflict."
       },
       "funder_independent_of_outcome": {
         "applies": true,
         "answer": true,
         "justification": "NSERC is a government funding agency with no financial interest in the outcome of this research."
       },
       "financial_interests_declared": {
         "applies": true,
         "answer": false,
         "justification": "No competing interests or financial interests statement is present in the paper."
       }
     },
     "contamination": {
       "training_cutoff_stated": {
         "applies": true,
         "answer": false,
         "justification": "No training data cutoff dates are stated for any of the 9 models used."
       },
       "train_test_overlap_discussed": {
         "applies": true,
         "answer": false,
         "justification": "No discussion of whether chess game patterns or pigeonhole proofs appeared in training data. Chess games and SAT problems are widely available online."
       },
       "benchmark_contamination_addressed": {
         "applies": true,
         "answer": false,
         "justification": "The pigeonhole problem is a classic well-known problem. No discussion of whether models may have seen pigeonhole resolution proofs during training. However, the constrained condition guarantees correctness regardless of contamination, partially mitigating this concern."
       }
     },
     "human_studies": {
       "pre_registered": {
         "applies": false,
         "answer": false,
         "justification": "No human participants in this study."
       },
       "irb_or_ethics_approval": {
         "applies": false,
         "answer": false,
         "justification": "No human participants in this study."
       },
       "demographics_reported": {
         "applies": false,
         "answer": false,
         "justification": "No human participants in this study."
       },
       "inclusion_exclusion_criteria": {
         "applies": false,
         "answer": false,
         "justification": "No human participants in this study."
       },
       "randomization_described": {
         "applies": false,
         "answer": false,
         "justification": "No human participants in this study."
       },
       "blinding_described": {
         "applies": false,
         "answer": false,
         "justification": "No human participants in this study."
       },
       "attrition_reported": {
         "applies": false,
         "answer": false,
         "justification": "No human participants in this study."
       }
     },
     "cost_and_practicality": {
       "inference_cost_reported": {
         "applies": true,
         "answer": true,
         "justification": "Tokens per second throughput is reported in Figure 5 for both constrained and unconstrained conditions, showing latency overhead. Specific numbers given: 24.7 tokens/sec for shorter proofs down to 5.5 for longer ones."
       },
       "compute_budget_stated": {
         "applies": true,
         "answer": false,
         "justification": "Hardware is described (Dell EMC C4140, NVIDIA Tesla V100) but total compute budget (GPU hours, total experiment time) is not quantified."
       }
     },
     "experimental_rigor": {
       "seed_sensitivity_reported": {
         "applies": true,
         "answer": true,
         "justification": "Results are reported across multiple trials with variance: 20 games per chess condition with standard deviation whiskers (Figure 2), and 50 trials per proof condition (Figures 3-4) showing success rates."
       },
       "number_of_runs_stated": {
         "applies": true,
         "answer": true,
         "justification": "Explicitly stated: 20 games per condition for chess (10 as White, 10 as Black), 50 iterations for pigeonhole sizes 1-2, 20 for size 3."
       },
       "hyperparameter_search_budget": {
         "applies": true,
         "answer": false,
         "justification": "No hyperparameter search is described. Temperature is set to 1.0 with defaults, but no justification for why these settings were chosen or whether alternatives were explored."
       },
       "best_config_selection_justified": {
         "applies": false,
         "answer": false,
         "justification": "No configuration selection is needed — the paper uses default settings for all models and reports results for all of them."
       },
       "multiple_comparison_correction": {
         "applies": false,
         "answer": false,
         "justification": "No statistical tests are performed, so multiple comparison correction is not applicable."
       },
       "self_comparison_bias_addressed": {
         "applies": true,
         "answer": false,
         "justification": "The authors implement both the constraint engine and the evaluation. No discussion of potential bias from evaluating their own system, though the formal nature of the domains (legal chess moves, valid resolvents) largely eliminates subjective evaluation bias."
       },
       "compute_budget_vs_performance": {
         "applies": true,
         "answer": true,
         "justification": "Figure 5 directly shows the performance cost of constrained vs unconstrained decoding in tokens/sec. The paper also discusses how throughput degrades with proof length (24.7 to 5.5 tokens/sec)."
       },
       "benchmark_construct_validity": {
         "applies": true,
         "answer": true,
         "justification": "The paper explicitly discusses what the benchmarks test and what they don't: chess is used as a 'Drosophila' model organism, not to build a chess engine. The pigeonhole problem is chosen as a well-known hard proof problem. The paper frames these as proof-of-concept, not claims about general reasoning."
       },
       "scaffold_confound_addressed": {
         "applies": false,
         "answer": false,
         "justification": "No scaffolding is involved — the technique operates at the token decoding level."
       }
     },
     "data_leakage": {
       "temporal_leakage_addressed": {
         "applies": true,
         "answer": false,
         "justification": "No discussion of whether pigeonhole proofs or chess strategies appeared in training data before model training cutoffs."
       },
       "feature_leakage_addressed": {
         "applies": true,
         "answer": false,
         "justification": "No discussion of whether the prompt format or problem encoding leaks information to the models."
       },
       "non_independence_addressed": {
         "applies": false,
         "answer": false,
         "justification": "Not applicable — the evaluation uses generated games and proof attempts, not a static dataset where train/test independence is a concern."
       },
       "leakage_detection_method": {
         "applies": true,
         "answer": false,
         "justification": "No leakage detection or prevention method is applied. The paper does not check whether models have memorized pigeonhole proofs."
       }
     }
   },
   "claims": [
     {
       "claim": "Logically constrained decoding eliminates illegal moves in LLM chess play across all 9 models tested.",
       "evidence": "Table 1: 897/900 unconstrained games ended by illegal move vs 0/900 constrained games. Tested across 9 LLMs × 5 difficulty levels × 20 games = 900 per condition.",
       "supported": "strong"
     },
     {
       "claim": "With logically constrained decoding, all 9 LLMs achieve 100% correct resolution proofs for pigeonhole problems of size 1 and 2.",
       "evidence": "Figures 3 and 4: constrained models achieve 100% accuracy across 50 trials for size 1 and 2, while unconstrained models score 0% on size 2.",
       "supported": "strong"
     },
     {
       "claim": "Small constrained LLMs can solve problems that frontier models (ChatGPT-5, Claude Sonnet 4) solve incorrectly.",
       "evidence": "§4.2: Qwen2.5-7B with constrained decoding completes size-3 pigeonhole proof correctly, while ChatGPT-5 makes an unsound deduction and Claude Sonnet 4 fails.",
       "supported": "moderate"
     },
     {
       "claim": "The latency overhead of logically constrained decoding is generally minimal.",
       "evidence": "Figure 5: tokens/sec comparison for Qwen2.5-7B shows modest overhead for sizes 1-2, though significant slowdown for size-3 proofs (24.7→5.5 tokens/sec for long proofs).",
       "supported": "moderate"
     }
   ],
   "red_flags": [
     {
       "flag": "No contamination analysis for well-known problems",
       "detail": "Pigeonhole problems and their resolution proofs are classic textbook material widely available online. LLMs may have memorized these proofs during training. The unconstrained baseline performance may understate what models could do with better prompting, and the constrained performance may benefit from memorized proof strategies. This doesn't undermine the correctness guarantee, but does affect the generalizability claim."
     },
     {
       "flag": "Frontier model comparisons are informal",
       "detail": "The comparisons to ChatGPT-5 and Claude Sonnet 4 are described as informal ('We do not have the resources to do extensive experiments on these models'). The chess game in Figure 1 is a single casual game. These anecdotal comparisons are presented prominently but lack the rigor of the main experiments."
     },
     {
       "flag": "Incomplete experiments for size-3 pigeonhole",
       "detail": "The constrained experiments for 3-pigeonhole could not be completed without an optimization that relaxes the 'minimal invasiveness' property. The paper acknowledges this but still presents the result as evidence of the technique's success."
     }
   ],
   "cited_papers": [
     {
       "title": "CRANE: Reasoning with constrained LLM generation",
       "authors": ["Debangshu Banerjee", "Tarun Suresh", "Shubham Ugare", "Sasa Misailovic", "Gagandeep Singh"],
       "year": 2025,
       "relevance": "Directly relevant: shows that strictly constraining LLM outputs can reduce reasoning ability, motivating the design of logically constrained decoding."
     },
     {
       "title": "Prompting is programming: A query language for large language models",
       "authors": ["Luca Beurer-Kellner", "Marc Fischer", "Martin Vechev"],
       "year": 2023,
       "relevance": "Foundational work on constrained decoding for regular expressions and context-free grammars."
     },
     {
       "title": "Guiding LLMs the right way: Fast, non-invasive constrained generation",
       "authors": ["Luca Beurer-Kellner", "Marc Fischer", "Martin Vechev"],
       "year": 2024,
       "relevance": "Key prior work on efficient, minimally-invasive constrained decoding techniques."
     },
     {
       "title": "Type-constrained code generation with language models",
       "authors": ["Niels Mündler", "Jingxuan He", "Hao Wang", "Koushik Sen", "Dawn Song", "Martin Vechev"],
       "year": 2025,
       "relevance": "Extends constrained decoding beyond syntax to type safety for code generation — philosophically aligned work."
     },
     {
       "title": "Can transformers reason logically? A study in SAT solving",
       "authors": ["Leyan Pan", "Vijay Ganesh", "Jacob Abernethy", "Chris Esposo", "Wenke Lee"],
       "year": 2025,
       "relevance": "Shows that empirically trained transformers for SAT generalize and scale poorly, motivating neuro-symbolic approaches."
     },
     {
       "title": "Syncode: LLM generation with grammar augmentation",
       "authors": ["Shubham Ugare", "Tarun Suresh", "Hangoo Kang", "Sasa Misailovic", "Gagandeep Singh"],
       "year": 2024,
       "arxiv_id": "2403.01632",
       "relevance": "Constrained decoding system using grammar augmentation for LLM output — key baseline approach."
     },
     {
       "title": "Efficient guided generation for large language models",
       "authors": ["Brandon T. Willard", "Rémi Louf"],
       "year": 2023,
       "arxiv_id": "2307.09702",
       "relevance": "Foundational work on efficient constrained generation supporting both regex and CFG constraints."
     },
     {
       "title": "Chain-of-thought prompting elicits reasoning in large language models",
       "authors": ["Jason Wei", "Xuezhi Wang", "Dale Schuurmans"],
       "year": 2023,
       "arxiv_id": "2201.11903",
       "relevance": "Chain-of-thought prompting as an alternative approach to improving LLM reasoning on complex tasks."
     },
     {
       "title": "Reinforcement learning for reasoning in large language models with one training example",
       "authors": ["Yiping Wang"],
       "year": 2025,
       "arxiv_id": "2504.20571",
       "relevance": "RL with verified rewards as an alternative technique for boosting LLM reasoning performance."
     },
     {
       "title": "Lost in space: Finding the right tokens for structured output",
       "authors": ["Sil Hamilton", "David Mimno"],
       "year": 2025,
       "arxiv_id": "2502.14969",
       "relevance": "Addresses token misalignment in constrained decoding — a key implementation challenge."
     }
   ]
 }