Pith. sign in

REVIEW 4 major objections 6 minor 101 references

Re:Form -- Reducing Human Annotations in Scalable Formal Software Verification with RL in LLMs: A Preliminary Study on Dafny

T0 review · 4 major / 6 minor · reviewed 2026-08-06 · deepseek-v4-flash

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

Pith's one-line read A minimal-supervision pipeline trains small open LLMs to write Dafny formal specifications that pass the verifier and frequently strengthen the Claude-generated ground truth, using verifier feedback alone as the reinforcement-learning…

desk verdict Solid empirical pipeline, real benchmark, but unverified Python-to-Dafny semantics undercuts the behavioral claims. read the letter →

arxiv 2507.16331 v4 pith:IZGHA42X submitted 2025-07-22 cs.CL

Chuanhao Yan , Fengdi Che , Xuhan Huang , Xu Xu , Xin Li , Yizhi Li , Xingwei Qu , Jingzhe Shi
show 7 more authors
Chenghua Lin Yaodong Yang Binhang Yuan Hang Zhao Yu Qiao Bowen Zhou Jie Fu
This is my paper
classification cs.CL
keywords Dafnyformalverificationreinforcementlearningspecificationgenerationchain-of-thought-freereasoningsubsetrewardcompositionalgeneralizationLLMcode
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

This paper claims that formal-software-verification skills can be trained into language models with almost no human annotation: no per-example specifications, no natural-language chain-of-thought, and no human-designed outcomes. Using Dafny, a language whose built-in verifier checks whether code satisfies its formal contract, the authors build a pipeline that auto-generates 20,000 verified Dafny programs from Python code, fine-tunes small open models (0.5B to 14B) on 3,000 of them, and then runs reinforcement learning with the verifier itself as the reward oracle. The central result is that verifier-driven RL improves not just verification rates but specification quality: a 'subset reward' that certifies a generated specification is at least as strong as the ground truth pushes models to weaken preconditions and strengthen postconditions, and in doing so the models discover specifications strictly stronger than the Claude-generated ground truth that seeded the data. Small RL-trained models then generalize out of domain: on the new DafnyComp benchmark of compositionally assembled programs, the 14B model verifies 14.0% of programs at pass@1, versus 2.7% for the frontier model that generated the training data. If this holds, it points to a scalable route to verified software in which the machine-checkable verifier, not human labour, supplies the training signal.

What carries the argument

The central object is the Dafny verifier — the automated program verifier (powered by the Z3 SMT solver) that checks whether a method body satisfies its preconditions, postconditions, and loop invariants — used as a sound, fully automated reward oracle. Around it sits the paper's defining mechanism, the subset reward, which certifies specification superiority through two implication checks performed by the same verifier: the generated preconditions must be implied by (hence no stronger than) the ground-truth preconditions, and the generated postconditions must imply the ground-truth postconditions under those preconditions. This turns the space of specifications into a partial order in which an agent can be rewarded for moving toward the weakest admissible input assumptions and the strongest guaranteed output properties. The supporting machinery is the automatic Python-to-Dafny data curation pipeline (template extraction, iterative verification-and-repair loops up to ten rounds), the DafnyComp benchmark that assembles LeetCode functions into multi-function call chains for out-of-domain testing, and GRPO policy optimization with KL-divergence and entropy regularization to preserve exploration.

What would settle it

A direct test: sample roughly 200 programs from the curated dataset and DafnyComp, execute the original Python functions and the verified Dafny translations on identical randomized inputs, and compare outputs, exceptions, and mutated object state. If even a small fraction of pairs diverge, the auto-generated ground-truth specifications describe the translated Dafny code rather than the Python source, and the pipeline's claim of learning to infer program behavior would need to be restated.

Watch

Extended reading notes

Core claim

The paper's central claim is that reward signals taken directly from a formal verifier can replace human-annotated chains of thought and per-example specifications as the training signal for formal specification generation. The authors show that after a deliberately small supervised fine-tuning stage on automatically curated data, reinforcement learning with a three-part reward — syntax, verification, and the novel subset reward — makes small models produce Dafny contracts that pass the verifier, match or strengthen the seeded ground truth, and generalize to structurally novel compositional programs. The subset reward is the load-bearing idea: it uses the Dafny verifier to check two logical implications, $\mathrm{GT}_{\mathrm{pre}} \Rightarrow \mathrm{GEN}_{\mathrm{pre}}$ and $\mathrm{GT}_{\mathrm{pre}} \Rightarrow (\mathrm{GEN}_{\mathrm{post}} \Rightarrow \mathrm{GT}_{\mathrm{post}})$, which together certify that the generated specification is at least as strong as the ground truth; this stops the reward hacking observed with verification rewards alone, where models emit trivially true clauses. Under this scheme the 14B model reaches a 55.3% specification-superiority rate in-domain and a 63.8% relative gain over its SFT counterpart on out-of-domain compositional benchmarks, and RL rollouts reveal novel postconditions and invariants absent from all 128 SFT rollouts. The paper therefore asserts that a minimal-prior pipeline plus verifier-graded exploration is sufficient to learn formal specification reasoning that rivals and sometimes exceeds frontier-model annotations.

Load-bearing premise

The load-bearing premise is that the automatic Python-to-Dafny translation preserves the behavior of the original Python programs: the pipeline verifies only that the translated Dafny code satisfies its own generated specifications, with no cross-language equivalence check, so if a translation changes behavior any learned specification describes the translated code rather than the intended Python program.

Editorial extensions

If this is right

  • Even a 0.5B model, after SFT on 3,000 auto-curated examples, writes syntactically valid Dafny code over 80% of the time — above GPT-4o's 47.7% — so large proprietary models are not a prerequisite for formal-language generation.
  • The subset reward fixes the trivial-spec failure mode of pure verification rewards: verification-reward-only agents collapse toward semantically empty clauses, while subset-reward agents reach a 55.3% specification-superiority rate at 14B.
  • Verifier-graded RL discovers genuinely novel clauses — postconditions, modifies frames, and decreases measures unseen in 128 SFT rollouts, at rates up to roughly 17% for an exploration-focused variant — so the model can surpass the Claude-generated ground truth, not just match it.
  • Out-of-domain compositional generalization follows: on DafnyComp, the 14B RL model verifies 14.0% of pass@1 programs against 8.3% for SFT, 2.7% for the data-generating model, and near zero for other closed LLMs.
  • The pipeline reduces per-example human annotation to zero, amortizing expert effort into templates and spot-checks, which is the precondition for scaling formal verification beyond hand-crafted proofs.

Reading between the lines

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

  • A testable extension is whether the subset-reward recipe transfers to other verifier-backed domains — Lean proof search, VeriFast separation-logic contracts, or hardware assertion checking — wherever the checker can certify implication between candidate and reference artifacts.
  • Because the ground truth is generated from translated Dafny code and the pipeline verifies only that the Dafny code satisfies its own specifications, the honest reading is that the models learn to specify the translation; a natural next experiment is cross-checking learned contracts against Python behavior with property-based testing to close that gap.
  • The subset reward defines a partial order on specifications, which suggests a curriculum argument the paper only gestures at: the same ordering that grades a candidate against ground truth could let an agent bootstrap its own harder targets, progressively self-improving without fresh human annotation.
  • Given the reported entropy-bonus instability (training collapse after roughly 100 steps), the exploration mechanism that produces novel clauses is still fragile; whether novelty continues to grow with longer, stabilized training is an open quantitative question.
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

4 major / 6 minor

Summary. The paper proposes Re:Form, a pipeline for training small LLMs to generate Dafny specifications with minimal human annotation. It automatically translates 20,000 Python programs into Dafny using Claude 3.5 Sonnet with iterative verifier-based repair, then fine-tunes Qwen-2.5 models (0.5B–14B) on 3,000 examples without natural-language chain-of-thought, and applies GRPO with rewards based on Dafny syntax checking, verification, and a subset-based superiority criterion. The paper also introduces DafnyComp, a synthetic out-of-domain benchmark of composed Python-to-Dafny programs. The main claims are that SFT alone enables small models to surpass proprietary LLMs in syntactic validity and verification, and that RL with KL and entropy regularization further improves specification quality, discovers novel specifications absent from SFT rollouts, and achieves stronger out-of-domain generalization on DafnyComp.

Significance. If the claims hold, the work is a valuable step toward verifier-driven RL for formal code reasoning: the Dafny verifier provides an external, machine-checkable reward signal; the data curation and training pipeline is largely automated; and the authors release data, code, and checkpoints. The exploration analysis (novel specification rate, diversity) and the candid failure analysis in Appendix B.6 are useful contributions. The main reservations concern the unvalidated Python-to-Dafny semantic preservation, the unstable main RL configuration and unspecified checkpoint selection, and the small OOD evaluation without statistical support.

major comments (4)
  1. [Section 2.1, Algorithms 1–2, and Section 1] The pipeline verifies only that the translated Dafny code satisfies its own generated specifications; it never checks behavioral equivalence between the Python source and the Dafny translation. The introduction states the goal to 'verify their derived specifications’ equivalence, to guarantee behavioral alignment,' but no such cross-language check appears in Algorithms 1–3. Consequently, the auto-formalized ground truth and the DafnyComp benchmark may describe the translated Dafny artifact rather than the original Python behavior, which directly affects the claim in Section 2.4 that the agent 'infer[s] every program’s behavior' and the validity of DafnyComp as a behavioral out-of-domain benchmark. Please add differential testing or another cross-language equivalence validation, or explicitly restrict the claims to the Dafny translations.
  2. [Section 3.3 and Appendix B.2.3] The main RL configuration (subset + KL + entropy) is described as the configuration used for the headline results, but the same section and Figure 15 report that entropy regularization 'causes training to collapse after approximately 100 steps.' The paper does not state which checkpoint is used for the reported RL numbers or how that checkpoint is selected across the collapse. Without a checkpoint-selection rule and ideally multiple seeds, the conclusion that 'RL with regularization further improves performance' is not robust; please report the evaluation checkpoint, its training step, and variance across seeds.
  3. [Section 3.2, Figure 8] The out-of-domain evaluation is based on 300 DafnyComp programs, and the pass@1 differences between RL-14B (14.0%), SFT-14B (8.3%), and Claude (2.7%) are reported as point estimates without confidence intervals or significance tests. Given the small sample, statements such as 'dominates' and 'outperforming all strong baselines' may exceed the evidence. Please provide bootstrap confidence intervals or statistical tests, and report the number of evaluation samples per condition.
  4. [Section 3.1 and Section 4] The spec superiority rate (SSR) and the subset reward both compare against the Claude-generated ground truth. The paper acknowledges this dependence in Section 4, but the claim that the metric enables 'measuring specification quality beyond merely passing the verifier' is only meaningful if the ground-truth specifications themselves are semantically correct for the intended programs; that correctness is precisely what the missing cross-language equivalence check in Major Comment 1 would establish. Please either validate the ground truth against the Python semantics or present SSR explicitly as a relative-to-Claude metric rather than an absolute quality measure.
minor comments (6)
  1. [Figure 1 caption] The caption contains several typos ('exploration capab-itliy', 'specifcation', 'rudimentary') and should be cleaned up.
  2. [Figure 10 caption] The word 'stochasticy' appears in the caption; this should be 'stochasticity'.
  3. [Table 1] The column headers 'N#Spec' and 'N#Token' are unclear; please clarify the units and whether these are per-function averages or totals.
  4. [Section 2.4, Eq. (2)] The group-wise advantage in Eq. (2) divides by the standard deviation of the group rewards, but if all rewards in a group are equal the denominator is zero; please specify how this case is handled.
  5. [Section 5.2] The claim that this is 'the first to train a code LLM using reward signals directly from a formal verifier' may be challenged by closely related verifier-reward RL work in formal mathematics (e.g., DeepSeek-Prover-V2) and should be softened or backed by a more systematic related-work comparison.
  6. [Appendix A.8.2] The SFT prompt says the input contains 'function signature, preconditions, postconditions, and code, but with annotations missing,' then instructs the model to 'use exactly the same function signature, preconditions, and postconditions'; please clarify which parts of the specification the model is expected to generate, since this is ambiguous relative to the full-specification task described in Section 2.3.

Circularity Check

2 steps flagged · score 3.0 of 10

Partial circularity: the headline spec-superiority metric is identical to the training reward, and both the training ground truth and the DafnyComp benchmark labels are auto-generated by the same Claude pipeline that serves as the baseline; the Dafny verifier and DafnyBench provide independent checks, so the core result is not tautological.

  1. fitted input called prediction [Section 2.4 (Subset rewards) and Section 3.1 (Evaluation Metrics)]
    "Subset rewards: The subset reward is granted when the generated specification is superior to or at least as strong as the ground truth by simultaneously weakening its preconditions and strengthening its postcondition. ... spec superiority rate (SSR) for the percentage of generated specifications superior to or at least as strong as the corresponding ground truth."

    The paper's headline quality metric, Spec Superiority Rate (SSR), is exactly the subset reward used as the RL objective; the GRPO group advantage is computed from these rewards. Reporting SSR improvements after RL is therefore reporting the quantity that was directly optimized, so the 'superior to ground truth' result is the training target by construction rather than an independent measure of specification quality. The verification rate and external DafnyBench results provide independent evidence, which is why the circularity is only partial.

  2. self definitional [Section 2.1 Data Curation / Algorithm 1; Section 2.2 Benchmark]
    "Each function is automatically annotated using Claude 3.5 Sonnet... The specifications generated by the chosen annotator are then statically verified using the Dafny verifier. ... we develop a benchmark, DafnyComp, which consists of synthetic Dafny programs with enhanced quality and complexity ... accompanied by auto-formalized ground truth specifications."

    The ground-truth labels used for training and for DafnyComp are produced by Claude, the same model family that serves as the principal baseline, for Dafny code that the pipeline itself translated from Python. The Dafny verifier checks only that the generated Dafny code satisfies its own specifications; no step checks behavioral equivalence between the Dafny code and the original Python, despite the Section 1 goal to 'verify their derived specifications' equivalence, to guarantee behavioral alignment.' The model's 'infer every program's behavior' target is therefore defined relative to the pipeline's own Dafny artifacts, making the benchmark and superiority metric dependent on the data generator's outputs rather than an independent oracle, though the verifier's consistency check is sound.

full rationale

The derivation chain is mostly self-contained: the Dafny verifier is an external, sound tool that checks both basic consistency and the subset-relation checks used for superiority, and the paper additionally evaluates on the external DafnyBench benchmark. The RL models produce novel specifications absent from all SFT rollouts and verified by Dafny, so the central result is not equivalent to the training inputs by construction. However, two evaluation-dependence issues create partial circularity. First, the reported SSR metric is literally the subset reward optimized during RL, so SSR gains are the optimized objective, not an independent quality measure. Second, the training ground truth and the DafnyComp benchmark labels are auto-generated by the same Claude pipeline that is the main baseline, and the verifier certifies only consistency with the translated Dafny code, not equivalence to the original Python behavior; the paper's own stated cross-language equivalence check is not implemented in the pipeline. These issues constrain the independence of the benchmark and the 'superior to ground truth' claims, but they do not collapse the core result: the Dafny verifier and DafnyBench provide external, machine-checked evidence of the model's specification-generation ability. No load-bearing self-citation chain or imported uniqueness theorem is present. Overall score 3 reflects partial evaluation-dependence rather than fully forced circularity.

Assumptions & free parameters 5 free parameters · 4 assumptions · 0 invented entities

The central claim rests on a small number of hand-chosen hyperparameters and three domain assumptions: verifier soundness, cross-language semantic preservation, and the validity of LLM-generated ground truth as a reference. The verifier soundness is standard and externally grounded; the semantic-preservation assumption is the most fragile and is unverified. No new physical or mathematical entities are postulated.

free parameters (5)
  • KL divergence coefficient = 0.01
    Chosen by hand; anchors the RL policy to the SFT model and affects exploration and stability.
  • Entropy bonus coefficient = 0.02
    Chosen by hand; injects stochasticity to encourage exploration, but causes training instability.
  • SFT training subset size = 3000
    The paper states 3,000 examples are enough to instill Dafny syntax and basic semantics.
  • Maximum verifier repair iterations = 10
    Cap on data curation repair loops; affects data yield and benchmark quality.
  • DafnyComp filtering: complexity threshold = McCabe > 5, 1in1out
    Function selection criteria for the OOD benchmark shape its difficulty and representativeness.
assumptions (4)
  • domain assumption The Dafny verifier is sound: it never accepts an invalid specification.
    Stated in Section 2.4; the entire reward signal and SSR metric rely on this.
  • domain assumption Python-to-Dafny translation preserves the original Python behavior.
    Invoked throughout Section 2.1 and Algorithm 1; no cross-language equivalence check is performed.
  • domain assumption Claude-generated and verifier-repaired ground truth specifications are a valid reference for specification quality.
    Used in the subset reward (Section 2.4) and the SSR metric (Section 3.1); the paper acknowledges GT can be weak.
  • standard math Standard RL background: GRPO objective and advantage normalization.
    Equations 1 and 2 in Section 2.4.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Re:Form -- Reducing Human Annotations in Scalable Formal Software Verification with RL in LLMs: A Preliminary Study on Dafny." pith.science (2026). https://pith.science/paper/IZGHA42X

@misc{pith2026250716331,
  author       = {Pith},
  title        = {Pith review of: Re:Form -- Reducing Human Annotations in Scalable Formal Software Verification with RL in LLMs: A Preliminary Study on Dafny},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/IZGHA42X}},
  note         = {Machine review of arXiv:2507.16331}
}
read the original abstract

Existing informal language-based (e.g., human language) Large Language Models (LLMs) trained with Reinforcement Learning (RL) face a significant challenge: their verification processes, which provide crucial training signals, are neither reliable nor scalable. In fact, the prevalent large proprietary models could hardly generate verifiable programs. A promising yet largely uncharted alternative is formal language-based reasoning. Grounding LLMs in rigorous formal systems where generative models operate in formal language spaces (e.g., Dafny) enables the automatic and mathematically provable verification of their reasoning processes and outcomes. This capability is pivotal for achieving large-scale, reliable formal software verification. It is a common practice to employ human-annotated chain-of-thought and answers to induce the reasoning and coding capabilities of LLMs. Unfortunately, it becomes unacceptably all-consuming to provide such priors for supervising complex programming tasks. In this work, we systematically explore ways to reduce human annotations with the formal language, Dafny, as the main environment for our pilot study. Our pipeline mainly relies on introducing an automatic and scalable data curation pipeline, and careful RL designs integrated with feedback from the formal language verifier. We introduce DafnyComp, a benchmark of compositional formal programs with auto-formalized specifications for specification reasoning. Our supervised fine-tuning (SFT) stage enables even small models (e.g., 0.5B) to generate syntactically valid and verifiable Dafny code, surpassing proprietary models. RL with regularization further improves performance, achieving stronger generalization to out-of-domain tasks and outperforming all strong baselines on the challenging DafnyComp benchmark.

Figures

Figures reproduced from arXiv: 2507.16331 by the authors.

Figure 1
Figure 1. Model Performance on DafnyComp benchmark. We roughly categorize the cases into four groups in [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. The Illustration of Re:Form Pipeline. Human prior is extensively removed across different [PITH_FULL_IMAGE:figures/full_fig_p004_2.png] view at source ↗
Figure 3
Figure 3. Specification Type Distribution. The first pipeline is designed to extensively leverage existing publicly available Dafny resources (Poesia et al., 2024; Lozhkov et al., 2024). We start with a public dataset data5 , and implement a lightweight crawler that scans and processes specific .dfy files in Dafny repositories. After merging the public dataset and automatically downloaded code modules, we apply a series of de… view at source ↗
Figures from the paper (29 more)
Figure 4
Figure 4. Figure 4: The figure presents an example of comments generated during RL learning, which is not extended [PITH_FULL_IMAGE:figures/full_fig_p011_4.png]
Figure 5
Figure 5. Figure 5: The figure shows the comparison between GPT-4o, our Qwen base models, SFT models and [PITH_FULL_IMAGE:figures/full_fig_p012_5.png]
Figure 6
Figure 6. Figure 6: The figure reports SFT and RL performance with [PITH_FULL_IMAGE:figures/full_fig_p012_6.png]
Figure 7
Figure 7. Figure 7: First example of novel specifications that never show up in the SFT model’s [PITH_FULL_IMAGE:figures/full_fig_p013_7.png]
Figure 8
Figure 8. Figure 8: Our 14B RL model dominates the pass@1 performance over SFT and GPT-4o, the best performing proprietary LLM other than our data-generator, Claude. Notably, GPT-4o attains the best score on DafnyBench, highlighting an asymmetry toward that benchmark. verification success…
Figure 9
Figure 9. Figure 9: These figures present the training curves for different reward schemes and regularization choices. [PITH_FULL_IMAGE:figures/full_fig_p014_9.png]
Figure 10
Figure 10. Figure 10: This figure compares the spec superiority rate (SSR) among three RL configurations: the subset [PITH_FULL_IMAGE:figures/full_fig_p015_10.png]
Figure 11
Figure 11. Figure 11: A toy example of a Dafny implementation with full specification, including precondition, postcon [PITH_FULL_IMAGE:figures/full_fig_p027_11.png]
Figure 12
Figure 12. Figure 12: The same implementation as in Figure 11, shown without any specification annotations. [PITH_FULL_IMAGE:figures/full_fig_p027_12.png]
Figure 13
Figure 13. Figure 13: Example of Python-to-Dafny conversion from our data curation pipeline. The left side shows the [PITH_FULL_IMAGE:figures/full_fig_p028_13.png]
Figure 14
Figure 14. Figure 14: On the top right block, we present the input code and show the extracted method preconditions [PITH_FULL_IMAGE:figures/full_fig_p029_14.png]
Figure 15
Figure 15. Figure 15: Training curves with [PITH_FULL_IMAGE:figures/full_fig_p038_15.png]
Figure 16
Figure 16. Figure 16: Training curves with 7B and 14B models for verification reward model, subset reward model without regularization, and subset reward model with KL and entropy. B.2.4 Qualitative Analysis [PITH_FULL_IMAGE:figures/full_fig_p039_16.png]
Figure 17
Figure 17. Figure 17: The top block shows the input code, followed by the extracted preconditions and postconditions [PITH_FULL_IMAGE:figures/full_fig_p040_17.png]
Figure 18
Figure 18. Figure 18: Left: Novel specification generation rate versus rollout count across different models. The SFT model yields zero novel specifications and serves as a baseline. Right: Diversity score (measured as embedding variance) versus rollout count for the same models. These plo…
Figure 19
Figure 19. Figure 19: Left: Novel specification generation rate versus rollout count across different models. The SFT model yields zero novel specifications and serves as a baseline. Right: Diversity score (measured as embedding variance) versus rollout count for the same models. These plo…
Figure 20
Figure 20. Figure 20: Left: Scatter plot of spec superiority rate versus novel specification rate. Right: Scatter plot of diversity score versus spec superiority rate. Each data point corresponds to a rollout group. Different colors indicate different models. Pearson correlation coefficien…
Figure 21
Figure 21. Figure 21: An example of trivial specification. These postconditions are trivially true [PITH_FULL_IMAGE:figures/full_fig_p044_21.png]
Figure 22
Figure 22. Figure 22: An example of trivial specification. These postconditions are trivially true. [PITH_FULL_IMAGE:figures/full_fig_p045_22.png]
Figure 23
Figure 23. Figure 23: Second example of novel specifications that did not show up in the SFT model’s 128 rollouts. [PITH_FULL_IMAGE:figures/full_fig_p046_23.png]
Figure 24
Figure 24. Figure 24: An example of novel specification "modifies" that did not show up in the SFT model’s 128 rollouts. 47 [PITH_FULL_IMAGE:figures/full_fig_p047_24.png]
Figure 25
Figure 25. Figure 25: An example of novel specification "decreases" that did not show up in the SFT model’s 128 rollouts. 48 [PITH_FULL_IMAGE:figures/full_fig_p048_25.png]
Figure 26
Figure 26. Figure 26: A sequence-head example where the generated specification surfaces the hidden requirement that [PITH_FULL_IMAGE:figures/full_fig_p049_26.png]
Figure 27
Figure 27. Figure 27: A division example where the generated contract surfaces a hidden arithmetic precondition instead [PITH_FULL_IMAGE:figures/full_fig_p049_27.png]
Figure 28
Figure 28. Figure 28: A buggy absolute-value implementation. The generated semantic postcondition exposes the bug [PITH_FULL_IMAGE:figures/full_fig_p050_28.png]
Figure 29
Figure 29. Figure 29: A buggy max-style implementation. The generated postconditions expose the semantic error [PITH_FULL_IMAGE:figures/full_fig_p050_29.png]
Figure 30
Figure 30. Figure 30: An example of generated code leading to unverifiable side conditions due to unproved assumptions [PITH_FULL_IMAGE:figures/full_fig_p051_30.png]
Figure 31
Figure 31. Figure 31: A comparison demonstrating a weak generated specification versus a stronger ground truth [PITH_FULL_IMAGE:figures/full_fig_p052_31.png]
Figure 32
Figure 32. Figure 32: A representative example of a trivial specification. The method verifies locally due to the trivial [PITH_FULL_IMAGE:figures/full_fig_p052_32.png]

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

101 extracted references · 29 canonical work pages

  1. [1]

    write newline

    " write newline "" before.all 'output.state := FUNCTION n.dashify 't := "" t empty not t #1 #1 substring "-" = t #1 #2 substring "--" = not "--" * t #2 global.max substring 't := t #1 #1 substring "-" = "-" * t #2 global.max substring 't := while if t #1 #1 substring * t #2 global.max substring 't := if while FUNCTION format.date year duplicate empty "emp...

  2. [2]

    L., Almeida, D., Altenschmidt, J., Altman, S., Anadkat, S., et al

    Achiam, J., Adler, S., Agarwal, S., Ahmad, L., Akkaya, I., Aleman, F. L., Almeida, D., Altenschmidt, J., Altman, S., Anadkat, S., et al. Gpt-4 technical report. arXiv preprint arXiv:2303.08774, 2023

    arXiv 2023

  3. [3]

    Alphacode 2 technical report

    AlphaCode Team . Alphacode 2 technical report. Blog post, December 2023. URL https://storage.googleapis.com/deepmind-media/AlphaCode2/AlphaCode2_Tech_Report.pdf

    2023

  4. [4]

    System card: Claude opus 4 & claude sonnet 4

    Anthropic . System card: Claude opus 4 & claude sonnet 4. Technical report, Anthropic, May 2025. URL https://www.anthropic.com/claude-4-system-card

    2025

  5. [5]

    Program synthesis with large language models

    Austin, J., Odena, A., Nye, M., Bosma, M., Michalewski, H., Dohan, D., Jiang, E., Cai, C., Terry, M., Le, Q., et al. Program synthesis with large language models. arXiv preprint arXiv:2108.07732, 2021

    arXiv 2021

  6. [6]

    Y., Collignon, N., Neo, C., Lee, I., Paren, A., Bibi, A., Trager, R., Fornasiere, D., Yan, J., Elazar, Y., and Bengio, Y

    Barez, F., Wu, T.-Y., Arcuschin, I., Lan, M., Wang-Maścianica, V., Siegel, N. Y., Collignon, N., Neo, C., Lee, I., Paren, A., Bibi, A., Trager, R., Fornasiere, D., Yan, J., Elazar, Y., and Bengio, Y. Chain-of-thought is not explainability. alphaXiv preprint, 2025. URL https://www.alphaxiv.org/abs/2025.02

    2025

  7. [7]

    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...

    arXiv 2021

  8. [8]

    Towards reasoning era: A survey of long chain-of-thought for reasoning large language models

    Chen, Q., Qin, L., Liu, J., Peng, D., Guan, J., Wang, P., Hu, M., Zhou, Y., Gao, T., and Che, W. Towards reasoning era: A survey of long chain-of-thought for reasoning large language models. arXiv preprint arXiv:2503.09567, 2025 a . URL https://arxiv.org/abs/2503.09567

    arXiv 2025

Show all 101 references
  1. [9]

    Reasoning models don't always say what they think

    Chen, Y., Benton, J., Radhakrishnan, A., Uesato, J., Denison, C., Schulman, J., Somani, A., Hase, P., Wagner, M., Roger, F., et al. Reasoning models don't always say what they think. arXiv preprint arXiv:2505.05410, 2025 b

    2025 arXiv

  2. [10]

    A., Nielsen-Garcia, C., Mir, S., Li, S., Orender, J., et al

    Cheng, Z., Wohnig, S., Gupta, R., Alam, S., Abdullahi, T., Ribeiro, J. A., Nielsen-Garcia, C., Mir, S., Li, S., Orender, J., et al. Position: Benchmarking is broken-don't let ai be its own judge, 2025

    2025

  3. [11]

    On the measure of intelligence

    Chollet, F. On the measure of intelligence. arXiv preprint arXiv:1911.01547, 2019

    1911 arXiv

  4. [12]

    V., Levine, S., and Ma, Y

    Chu, T., Zhai, Y., Yang, J., Tong, S., Xie, S., Schuurmans, D., Le, Q. V., Levine, S., and Ma, Y. Sft memorizes, rl generalizes: A comparative study of foundation model post-training. In Forty-second International Conference on Machine Learning, 2025

    2025

  5. [13]

    Chung, H. W. Don't teach. incentivize. YouTube video, September 2024. URL https://www.youtube.com/watch?v=kYWUEV_e2ss. MIT EI Seminar, OpenAI researcher

    2024

  6. [14]

    Towards formal verification of llm-generated code from natural language prompts, 2025

    Councilman, A., Fu, D., Gupta, A., Wang, C., Grove, D., Wang, Y.-X., and Adve, V. Towards formal verification of llm-generated code from natural language prompts, 2025. URL https://arxiv.org/abs/2507.13290

    2025

  7. [15]

    Towards guaranteed safe ai: A framework for ensuring robust and reliable ai systems

    Dalrymple, D., Skalse, J., Bengio, Y., Russell, S., Tegmark, M., Seshia, S., Omohundro, S., Szegedy, C., Goldhaber, B., Ammann, N., et al. Towards guaranteed safe ai: A framework for ensuring robust and reliable ai systems. arXiv preprint arXiv:2405.06624, 2024

    2024 arXiv

  8. [16]

    and Bj rner, N

    De Moura, L. and Bj rner, N. Z3: An efficient smt solver. In International conference on Tools and Algorithms for the Construction and Analysis of Systems, pp.\ 337--340. Springer, 2008

    2008

  9. [17]

    The lean theorem prover (system description)

    De Moura, L., Kong, S., Avigad, J., Van Doorn, F., and Von Raumer, J. The lean theorem prover (system description). In International Conference on Automated Deduction, pp.\ 378--388. Springer, 2015

    2015

  10. [18]

    Deepseek-prover-v2: Advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition

    DeepSeek-AI. Deepseek-prover-v2: Advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition. arXiv preprint arXiv:2504.21801, 2025

    2025 arXiv

  11. [19]

    Dijkstra, E. W. On the foolishness of ``natural language programming''. In Program Construction, International Summer School, pp.\ 51--53, London, UK, 1979. Springer. doi:10.5555/2891460.2891552. Originally written 1978

    1979

  12. [20]

    Generalization or memorization: Data contamination and trustworthy evaluation for large language models

    Dong, Y., Jiang, X., Liu, H., Jin, Z., Gu, B., Yang, M., and Li, G. Generalization or memorization: Data contamination and trustworthy evaluation for large language models. In Findings of the Association for Computational Linguistics: ACL 2024, pp.\ 12039--12050, 2024

    2024

  13. [21]

    and Mehta, R

    Dougherty, Q. and Mehta, R. Proving the coding interview: A benchmark for formally verified code generation. In 2025 IEEE/ACM International Workshop on Large Language Models for Code (LLM4Code), pp.\ 72--79. IEEE, 2025

    2025

  14. [22]

    Gemini 2.5: Pushing the frontier with advanced reasoning, multimodality, long context, and next generation agentic capabilities

    Gemini Team, Google . Gemini 2.5: Pushing the frontier with advanced reasoning, multimodality, long context, and next generation agentic capabilities. Technical report, Google DeepMind, June 2025. URL https://storage.googleapis.com/deepmind-media/gemini/gemini_v2_5_report.pdf....

    2025

  15. [23]

    Deepseek-r1: Incentivizing reasoning capability in llms via reinforcement learning

    Guo, D., Yang, D., Zhang, H., Song, J., Zhang, R., Xu, R., Zhu, Q., Ma, S., Wang, P., Bi, X., et al. Deepseek-r1: Incentivizing reasoning capability in llms via reinforcement learning. arXiv preprint arXiv:2501.12948, 2025

    2025 arXiv

  16. [24]

    Measuring and improving semantic diversity of dialogue generation

    Han, S., Kim, B., and Chang, B. Measuring and improving semantic diversity of dialogue generation. In Goldberg, Y., Kozareva, Z., and Zhang, Y. (eds.), Findings of the Association for Computational Linguistics: EMNLP 2022, pp.\ 934--950, Abu Dhabi, United Arab Emirates, Decemb...

    2022 doi

  17. [25]

    Dynacode: A dynamic complexity-aware code benchmark for evaluating large language models in code generation

    Hu, W., Duan, J., Wei, C., Zhang, L., Zhang, Y., and Xu, K. Dynacode: A dynamic complexity-aware code benchmark for evaluating large language models in code generation. arXiv preprint arXiv:2503.10452, 2025

    2025 arXiv

  18. [26]

    Does math reasoning improve general llm capabilities? understanding transferability of llm reasoning, 2025

    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, 2025

    2025

  19. [27]

    Hui, B., Yang, J., Cui, Z., Yang, J., Liu, D., Zhang, L., Liu, T., Zhang, J., Yu, B., Lu, K., et al. Qwen2. 5-coder technical report. arXiv preprint arXiv:2409.12186, 2024

    2024 arXiv

  20. [28]

    and Cheng, M

    Ibrahim, L. and Cheng, M. Thinking beyond the anthropomorphic paradigm benefits llm research. arXiv preprint arXiv:2502.09192, 2025

    2025 arXiv

  21. [29]

    AI safety via debate, May 2018

    Irving, G., Christiano, P., and Amodei, D. AI safety via debate, May 2018

    2018

  22. [30]

    Verifast: A powerful, sound, predictable, fast verifier for c and java

    Jacobs, B., Smans, J., Philippaerts, P., Vogels, F., Penninckx, W., and Piessens, F. Verifast: A powerful, sound, predictable, fast verifier for c and java. In NASA formal methods symposium, pp.\ 41--55. Springer, 2011

    2011

  23. [31]

    Do we need to verify step by step? rethinking process supervision from a theoretical perspective, February 2025

    Jia, Z., Rakhlin, A., and Xie, T. Do we need to verify step by step? rethinking process supervision from a theoretical perspective, February 2025

    2025

  24. [32]

    Can large language models understand intermediate representations in compilers?, February 2025

    Jiang, H., Zhu, J., Wan, Y., Fang, B., Zhang, H., Jin, R., and Guan, Q. Can large language models understand intermediate representations in compilers?, February 2025

    2025

  25. [33]

    sel4: Formal verification of an os kernel

    Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., et al. sel4: Formal verification of an os kernel. In Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles, pp.\ 207--220, 2009

    2009

  26. [34]

    Chain of thought monitorability: A new and fragile opportunity for AI safety, July 2025

    Korbak, T., Balesni, M., Barnes, E., Bengio, Y., Benton, J., Bloom, J., Chen, M., Cooney, A., Dafoe, A., Dragan, A., Emmons, S., Evans, O., Farhi, D., Greenblatt, R., Hendrycks, D., Hobbhahn, M., Hubinger, E., Irving, G., Jenner, E., Kokotajlo, D., Krakovna, V., Legg, S., Lind...

    2025

  27. [35]

    Gradual disempowerment: Systemic existential risks from incremental AI development, January 2025

    Kulveit, J., Douglas, R., Ammann, N., Turan, D., Krueger, D., and Duvenaud, D. Gradual disempowerment: Systemic existential risks from incremental AI development, January 2025

    2025

  28. [36]

    M., Cholakkal, H., Shah, M., Yang, M.-H., Torr, P

    Kumar, K., Ashraf, T., Thawakar, O., Anwer, R. M., Cholakkal, H., Shah, M., Yang, M.-H., Torr, P. H., Khan, F. S., and Khan, S. Llm post-training: A deep dive into reasoning large language models. arXiv preprint arXiv:2502.21321, 2025

    2025 arXiv

  29. [37]

    Measuring faithfulness in chain-of-thought reasoning

    Lanham, T., Chen, A., Radhakrishnan, A., Steiner, B., Denison, C., Hernandez, D., Li, D., Durmus, E., Hubinger, E., Kernion, J., et al. Measuring faithfulness in chain-of-thought reasoning. arXiv preprint arXiv:2307.13702, 2023

    2023 arXiv

  30. [38]

    D., Savarese, S., and Hoi, S

    Le, H., Wang, Y., Gotmare, A. D., Savarese, S., and Hoi, S. C. H. Coderl: Mastering code generation through pretrained models and deep reinforcement learning, 2022. URL https://arxiv.org/abs/2207.01780

    2022 arXiv

  31. [39]

    How well do llms compress their own chain-of-thought? a token complexity approach

    Lee, A., Che, E., and Peng, T. How well do llms compress their own chain-of-thought? a token complexity approach. arXiv preprint arXiv:2503.01141, 2025

    2025 arXiv

  32. [40]

    Leino, K. R. M. Dafny: An automatic program verifier for functional correctness. In International conference on logic for programming artificial intelligence and reasoning, pp.\ 348--370. Springer, 2010

    2010

  33. [41]

    Codei/o: Condensing reasoning patterns via code input-output prediction

    Li, J., Guo, D., Yang, D., Xu, R., Wu, Y., and He, J. Codei/o: Condensing reasoning patterns via code input-output prediction. arXiv preprint arXiv:2502.07316, 2025 a

    2025 arXiv

  34. [42]

    Autotriton: Automatic triton programming with reinforcement learning in llms

    Li, S., Wang, Z., He, Y., Li, Y., Shi, Q., Li, J., Hu, Y., Che, W., Han, X., Liu, Z., et al. Autotriton: Automatic triton programming with reinforcement learning in llms. arXiv preprint arXiv:2507.05687, 2025 b

    2025 arXiv

  35. [43]

    M., Tang, H., Naim, M., Nguyen, D., et al

    Li, W.-D., Hu, K., Larsen, C., Wu, Y., Alford, S., Woo, C., Dunn, S. M., Tang, H., Naim, M., Nguyen, D., et al. Combining induction and transduction for abstract reasoning. arXiv preprint arXiv:2411.02272, 2024

    2024 arXiv

  36. [44]

    Competition-level code generation with alphacode

    Li, Y., Choi, D., Chung, J., Kushman, N., Schrittwieser, J., Leblond, R., Eccles, T., Keeling, J., Gimeno, F., Dal Lago, A., et al. Competition-level code generation with alphacode. Science, 378 0 (6624): 0 1092--1097, 2022

    2022

  37. [45]

    C., Zetzsche, S., and Somayyajula, S

    Li, Y. C., Zetzsche, S., and Somayyajula, S. Dafny as verification-aware intermediate language for code generation. arXiv preprint arXiv:2501.06283, 2025 c

    2025 arXiv

  38. [46]

    Towards solving more challenging imo problems via decoupled reasoning and proving

    Liang, Z., Song, L., Li, Y., Yang, T., Zhang, F., Mi, H., and Yu, D. Towards solving more challenging imo problems via decoupled reasoning and proving. arXiv preprint arXiv:2507.06804, 2025. URL https://arxiv.org/abs/2507.06804

    2025 arXiv

  39. [47]

    Goedel-prover-v2: The strongest open-source theorem prover to date, 2025

    Lin, Y., Tang, S., Lyu, B., Yang, Z., Chung, J.-H., Zhao, H., Jiang, L., Geng, Y., Ge, J., Sun, J., Wu, J., Gesi, J., Acuna, D., Yang, K., Lin, H., Choi, Y., Chen, D., Arora, S., and Jin, C. Goedel-prover-v2: The strongest open-source theorem prover to date, 2025

    2025

  40. [48]

    Safe: Enhancing mathematical reasoning in large language models via retrospective step-aware formal verification, 2025 a

    Liu, C., Yuan, Y., Yin, Y., Xu, Y., Xu, X., Chen, Z., Wang, Y., Shang, L., Liu, Q., and Zhang, M. Safe: Enhancing mathematical reasoning in large language models via retrospective step-aware formal verification, 2025 a . URL https://arxiv.org/abs/2506.04592

    2025 arXiv

  41. [49]

    Prorl: Prolonged reinforcement learning expands reasoning boundaries in large language models

    Liu, M., Diao, S., Lu, X., Hu, J., Dong, X., Choi, Y., Kautz, J., and Dong, Y. Prorl: Prolonged reinforcement learning expands reasoning boundaries in large language models. arXiv preprint arXiv:2505.24864, 2025 b

    2025 arXiv

  42. [50]

    Loughridge, C., Sun, Q., Ahrenbach, S., Cassano, F., Sun, C., Sheng, Y., Mudide, A., Misu, M. R. H., Amin, N., and Tegmark, M. Dafnybench: A benchmark for formal software verification. arXiv preprint arXiv:2406.08467, 2024

    2024 arXiv

  43. [51]

    B., Cassano, F., Lamy-Poirier, J., Tazi, N., Tang, A., Pykhtar, D., Liu, J., Wei, Y., et al

    Lozhkov, A., Li, R., Allal, L. B., Cassano, F., Lamy-Poirier, J., Tazi, N., Tang, A., Pykhtar, D., Liu, J., Wei, Y., et al. Starcoder 2 and the stack v2: The next generation. arXiv preprint arXiv:2402.19173, 2024

    2024 arXiv

  44. [52]

    Reasoning models can be effective without thinking, April 2025

    Ma, W., He, J., Snell, C., Griggs, T., Min, S., and Zaharia, M. Reasoning models can be effective without thinking, April 2025

    2025

  45. [53]

    Potemkin understanding in large language models

    Mancoridis, M., Weeks, B., Vafa, K., and Mullainathan, S. Potemkin understanding in large language models. arXiv preprint arXiv:2506.21521, 2025

    2025 arXiv

  46. [54]

    Misu, M. R. H., Lopes, C. V., Ma, I., and Noble, J. Towards ai-assisted synthesis of verified dafny methods. Proceedings of the ACM on Software Engineering, 1 0 (FSE): 0 812--835, 2024

    2024

  47. [55]

    Mitchell, T. M. The need for biases in learning generalizations, 1980

    1980

  48. [56]

    Z., Shirobokov, S., Kozlovskii, B., Ruiz, F

    Novikov, A., V \ u , N., Eisenberger, M., Dupont, E., Huang, P.-S., Wagner, A. Z., Shirobokov, S., Kozlovskii, B., Ruiz, F. J., Mehrabian, A., et al. Alphaevolve: A coding agent for scientific and algorithmic discovery. arXiv preprint arXiv:2506.13131, 2025

    2025 arXiv

  49. [57]

    Training language models to follow instructions with human feedback

    Ouyang, L., Wu, J., Jiang, X., Almeida, D., Wainwright, C., Mishkin, P., Zhang, C., Agarwal, S., Slama, K., Ray, A., et al. Training language models to follow instructions with human feedback. Advances in neural information processing systems, 35: 0 27730--27744, 2022

    2022

  50. [58]

    How to get your llm to generate challenging problems for evaluation

    Patel, A., Reddy, S., and Bahdanau, D. How to get your llm to generate challenging problems for evaluation. arXiv preprint arXiv:2502.14678, 2025

    2025 arXiv

  51. [59]

    How does code pretraining affect language model task performance? Transactions on Machine Learning Research, 2025, 2025

    Petty, J., van Steenkiste, S., and Linzen, T. How does code pretraining affect language model task performance? Transactions on Machine Learning Research, 2025, 2025

    2025

  52. [60]

    dafny-annotator: Ai-assisted verification of dafny programs

    Poesia, G., Loughridge, C., and Amin, N. dafny-annotator: Ai-assisted verification of dafny programs. arXiv preprint arXiv:2411.15143, 2024

    2024 arXiv

  53. [61]

    Qodo-Embed-1: State-of-the-Art Code Embedding Models

    Qodo AI . Qodo-Embed-1: State-of-the-Art Code Embedding Models . https://www.qodo.ai/products/code-embedding/, February 2025. URL https://www.qodo.ai/products/code-embedding/. Qodo-Embed-1-1.5B available on Hugging Face: https://huggingface.co/Qodo/Qodo-Embed-1-1.5B

    2025

  54. [62]

    What is ansible?, 2025

    Red Hat . What is ansible?, 2025. URL https://www.ansible.com. Accessed: July 19, 2025

    2025

  55. [63]

    Evaluating the ability of gpt-4o to generate verifiable specifications in verifast

    Rego, M., Fan, W., Hu, X., Dod, S., Ni, Z., Xie, D., DiVincenzo, J., and Tan, L. Evaluating the ability of gpt-4o to generate verifiable specifications in verifast. In 2025 IEEE/ACM Second International Conference on AI Foundation Models and Software Engineering (Forge), pp.\ ...

    2025

  56. [64]

    Quantifying contamination in evaluating code generation capabilities of language models

    Riddell, M., Ni, A., and Cohan, A. Quantifying contamination in evaluating code generation capabilities of language models. In Proceedings of the 62nd Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), pp.\ 14116--14137, 2024

    2024

  57. [65]

    R., Gnaneshwar, D., Locatelli, A., Kirk, R., Rockt \"a schel, T., Grefenstette, E., and Bartolo, M

    Ruis, L., Mozes, M., Bae, J., Kamalakara, S. R., Gnaneshwar, D., Locatelli, A., Kirk, R., Rockt \"a schel, T., Grefenstette, E., and Bartolo, M. Procedural knowledge in pretraining drives reasoning in large language models. In The Thirteenth International Conference on Learnin...

    2025

  58. [66]

    Boundless socratic learning with language games

    Schaul, T. Boundless socratic learning with language games. arXiv preprint arXiv:2411.16905, 2024

    2024 arXiv

  59. [67]

    Autoregressive large language models are computationally universal

    Schuurmans, D., Dai, H., and Zanini, F. Autoregressive large language models are computationally universal. arXiv preprint arXiv:2410.03170, 2024

    2024 arXiv

  60. [68]

    Deepseekmath: Pushing the limits of mathematical reasoning in open language models

    Shao, Z., Wang, P., Zhu, Q., Xu, R., Song, J., Bi, X., Zhang, H., Zhang, M., Li, Y., Wu, Y., et al. Deepseekmath: Pushing the limits of mathematical reasoning in open language models. arXiv preprint arXiv:2402.03300, 2024

    2024 arXiv

  61. [69]

    The illusion of thinking: Understanding the strengths and limitations of reasoning models via the lens of problem complexity

    Shojaee, P., Mirzadeh, I., Alizadeh, K., Horton, M., Bengio, S., and Farajtabar, M. The illusion of thinking: Understanding the strengths and limitations of reasoning models via the lens of problem complexity. arXiv preprint arXiv:2506.06941, 2025

    2025 arXiv

  62. [70]

    and Sutton, R

    Silver, D. and Sutton, R. S. Welcome to the era of experience. Google AI, 1, 2025

    2025

  63. [71]

    Silver, D., Singh, S., Precup, D., and Sutton, R. S. Reward is enough. Artificial Intelligence, 299: 0 103535, 2021

    2021

  64. [72]

    Beyond semantics: The unreasonable effectiveness of reasonless intermediate tokens, May 2025

    Stechly, K., Valmeekam, K., Gundawar, A., Palod, V., and Kambhampati, S. Beyond semantics: The unreasonable effectiveness of reasonless intermediate tokens, May 2025

    2025

  65. [73]

    Clover: Closed-loop verifiable code generation

    Sun, C., Sheng, Y., Padon, O., and Barrett, C. Clover: Closed-loop verifiable code generation. In International Symposium on AI Verification, pp.\ 134--155. Springer, 2024

    2024

  66. [74]

    Omega: Can llms reason outside the box in math? evaluating exploratory, compositional, and transformative generalization

    Sun, Y., Hu, S., Zhou, G., Zheng, K., Hajishirzi, H., Dziri, N., and Song, D. Omega: Can llms reason outside the box in math? evaluating exploratory, compositional, and transformative generalization. arXiv preprint arXiv:2506.18880, 2025

    2025 arXiv

  67. [75]

    The bitter lesson

    Sutton, R. The bitter lesson. http://www.incompleteideas.net/IncIdeas/BitterLesson.html, 2019. Accessed: 2025-07-19

    2019

  68. [76]

    S., Barto, A

    Sutton, R. S., Barto, A. G., et al. Introduction to reinforcement learning, volume 135. MIT press Cambridge, 1998

    1998

  69. [77]

    S., McAllester, D., Singh, S., and Mansour, Y

    Sutton, R. S., McAllester, D., Singh, S., and Mansour, Y. Policy gradient methods for reinforcement learning with function approximation. Advances in neural information processing systems, 12, 1999

    1999

  70. [78]

    K., Fu, S., and Sundaresan, N

    Svyatkovskiy, A., Deng, S. K., Fu, S., and Sundaresan, N. Intellicode compose: Code generation using transformer. In Proceedings of the 28th ACM joint meeting on European software engineering conference and symposium on the foundations of software engineering, pp.\ 1433--1443, 2020

    2020

  71. [79]

    A promising path towards autoformalization and general artificial intelligence

    Szegedy, C. A promising path towards autoformalization and general artificial intelligence. In International Conference on Intelligent Computer Mathematics, pp.\ 3--20. Springer, 2020

    2020

  72. [80]

    Worldcoder, a model-based llm agent: Building world models by writing code and interacting with the environment

    Tang, H., Key, D., and Ellis, K. Worldcoder, a model-based llm agent: Building world models by writing code and interacting with the environment. Advances in Neural Information Processing Systems, 37: 0 70148--70212, 2024

    2024

  73. [81]

    Clever: A curated benchmark for formally verified code generation

    Thakur, A., Lee, J., Tsoukalas, G., Sistla, M., Zhao, M., Zetzche, S., Durrett, G., Yue, Y., and Chaudhuri, S. Clever: A curated benchmark for formally verified code generation. arXiv preprint arXiv:2505.13938, 2025

    2025

  74. [82]

    Trivedi, D., Zhang, J., Sun, S.-H., and Lim, J. J. Learning to synthesize programs as interpretable and generalizable policies. In Ranzato, M., Beygelzimer, A., Dauphin, Y., Liang, P., and Vaughan, J. W. (eds.), Advances in Neural Information Processing Systems, volume 34, pp....

    2021

  75. [83]

    Dice: Detecting in-distribution contamination in llm's fine-tuning phase for math reasoning

    Tu, S., Zhu, K., Bai, Y., Yao, Z., Hou, L., and Li, J. Dice: Detecting in-distribution contamination in llm's fine-tuning phase for math reasoning. arXiv preprint arXiv:2406.04197, 2024

    2024 arXiv

  76. [84]

    D., Romero-Sorozabal, P., Rocon, E., and Cebrian, M

    Varela, I. D., Romero-Sorozabal, P., Rocon, E., and Cebrian, M. Rethinking the illusion of thinking. arXiv preprint arXiv:2507.01231, 2025

    2025 arXiv

  77. [85]

    Wang, H., Unsal, M., Lin, X., Baksys, M., Liu, J., Santos, M. D., Sung, F., Vinyes, M., Ying, Z., Zhu, Z., Lu, J., de Saxcé, H., Bailey, B., Song, C., Xiao, C., Zhang, D., Zhang, E., Pu, F., Zhu, H., Liu, J., Bayer, J., Michel, J., Yu, L., Dreyfus-Schmidt, L., Tunstall, L., Pa...

    2025 arXiv

  78. [86]

    Reasoning or memorization? unreliable results of reinforcement learning due to data contamination

    Wu, M., Zhang, Z., Dong, Q., Xi, Z., Zhao, J., Jin, S., Fan, X., Zhou, Y., Fu, Y., Liu, Q., et al. Reasoning or memorization? unreliable results of reinforcement learning due to data contamination. arXiv preprint arXiv:2507.10532, 2025 a

    2025

  79. [87]

    When more is less: Understanding chain-of-thought length in llms

    Wu, Y., Wang, Y., Ye, Z., Du, T., Jegelka, S., and Wang, Y. When more is less: Understanding chain-of-thought length in llms. arXiv preprint arXiv:2502.07266, 2025 b

    2025 arXiv

  80. [88]

    K., Sun, H., Wu, S., Hu, J., and Xu, X

    Xia, Y., Shen, W., Wang, Y., Liu, J. K., Sun, H., Wu, S., Hu, J., and Xu, X. Leetcodedataset: A temporal dataset for robust evaluation and efficient training of code llms, 2025. URL https://arxiv.org/abs/2504.14655

    2025 arXiv

  81. [89]

    Formal mathematical reasoning: A new frontier in ai

    Yang, K., Poesia, G., He, J., Li, W., Lauter, K., Chaudhuri, S., and Song, D. Formal mathematical reasoning: A new frontier in ai. arXiv preprint arXiv:2412.16075, 2024

    2024 arXiv

  82. [90]

    Verina: Benchmarking verifiable code generation

    Ye, Z., Yan, Z., He, J., Kasriel, T., Yang, K., and Song, D. Verina: Benchmarking verifiable code generation. arXiv preprint arXiv:2505.23135, 2025

    2025

  83. [91]

    FormalMATH : Benchmarking formal mathematical reasoning of large language models, May 2025

    Yu, Z., Peng, R., Ding, K., Li, Y., Peng, Z., Liu, M., Zhang, Y., Yuan, Z., Xin, H., Huang, W., Wen, Y., Zhang, G., and Liu, W. FormalMATH : Benchmarking formal mathematical reasoning of large language models, May 2025

    2025

  84. [92]

    Does reinforcement learning really incentivize reasoning capacity in LLMs beyond the base model?, April 2025

    Yue, Y., Chen, Z., Lu, R., Zhao, A., Wang, Z., Yue, Y., Song, S., and Huang, G. Does reinforcement learning really incentivize reasoning capacity in LLMs beyond the base model?, April 2025

    2025

  85. [93]

    Absolute zero: Reinforced self-play reasoning with zero data, 2025

    Zhao, A., Wu, Y., Yue, Y., Wu, T., Xu, Q., Yue, Y., Lin, M., Wang, S., Wu, Q., Zheng, Z., and Huang, G. Absolute zero: Reinforced self-play reasoning with zero data, 2025. URL https://arxiv.org/abs/2505.03335

    2025 arXiv

  86. [94]

    M., and Polu, S

    Zheng, K., Han, J. M., and Polu, S. Minif2f: a cross-system benchmark for formal olympiad-level mathematics, 2022. URL https://arxiv.org/abs/2109.00110

    2022 arXiv

  87. [95]

    What makes large language models reason in (multi-turn) code generation?, 2025

    Zheng, K., Decugis, J., Gehring, J., Cohen, T., Negrevergne, B., and Synnaeve, G. What makes large language models reason in (multi-turn) code generation?, 2025. URL https://arxiv.org/abs/2410.08105

    2025 arXiv

  88. [96]

    Reasoning by superposition: A theoretical perspective on chain of continuous thought

    Zhu, H., Hao, S., Hu, Z., Jiao, J., Russell, S., and Tian, Y. Reasoning by superposition: A theoretical perspective on chain of continuous thought. July 2025

    2025

  89. [97]

    @esa (Ref

    \@ifxundefined[1] #1\@undefined \@firstoftwo \@secondoftwo \@ifnum[1] #1 \@firstoftwo \@secondoftwo \@ifx[1] #1 \@firstoftwo \@secondoftwo [2] @ #1 \@temptokena #2 #1 @ \@temptokena \@ifclassloaded agu2001 natbib The agu2001 class already includes natbib coding, so you should ...

  90. [98]

    \@lbibitem[] @bibitem@first@sw\@secondoftwo \@lbibitem[#1]#2 \@extra@b@citeb \@ifundefined br@#2\@extra@b@citeb \@namedef br@#2 \@nameuse br@#2\@extra@b@citeb \@ifundefined b@#2\@extra@b@citeb @num @parse #2 @tmp #1 NAT@b@open@#2 NAT@b@shut@#2 \@ifnum @merge>\@ne @bibitem@firs...

  91. [99]

    best exploration

    @open @close @open @close and [1] URL: #1 \@ifundefined chapter * \@mkboth \@ifxundefined @sectionbib * \@mkboth * \@mkboth\@gobbletwo \@ifclassloaded amsart * \@ifclassloaded amsbook * \@ifxundefined @heading @heading NAT@ctr thebibliography [1] @ \@biblabel @NAT@ctr \@bibset...

    2010

  92. [100]

    write newline

    " write newline "" before.all 'output.state := FUNCTION n.dashify 't := "" t empty not t #1 #1 substring "-" = t #1 #2 substring "--" = not "--" * t #2 global.max substring 't := t #1 #1 substring "-" = "-" * t #2 global.max substring 't := while if t #1 #1 substring * t #2 gl...

  93. [101]

    License" shall mean the terms and conditions for use, reproduction, and distribution as defined by Sections 1 through 9 of this document

    @open @close @open @close and [1] URL: #1 \@ifundefined chapter * \@mkboth \@ifxundefined @sectionbib * \@mkboth * \@mkboth\@gobbletwo \@ifclassloaded amsart * \@ifclassloaded amsbook * \@ifxundefined @heading @heading NAT@ctr thebibliography [1] @ \@biblabel @NAT@ctr \@bibset...

    2004

Pith tools

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