{"id":"b70f3f77-94e3-40df-852b-076225e7a997","arxiv_id":"2501.05252","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":5.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"A prototype that uses an LLM iteratively with Dafny verification can turn natural-language graph proofs into verifiable code for three simple lemmas, suggesting a two-stage path toward automated verification.","lead":"This position paper proposes using large language models to turn proofs found in research papers into formally verifiable code, with a prototype called PROMETHEUS. It reports success in proving three simple graph lemmas in Dafny by splitting work into a high-level proof skeleton and low-level proof details.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Experiment conflates iterative verifier feedback with the two-stage skeleton decomposition, so the central claim that the split is what enables success is not supported.","rationale":"The reader's weakest assumption—that omitted proof steps are mostly low-level and mechanical—is an important generality concern for the vision, and I agree it deserves scrutiny. However, the single most load-bearing problem with the paper's central claim is more immediate: the one controlled experiment does not isolate the proposed mechanism. The zero-shot baseline differs from PROMETHEUS in two ways at once: it lacks the skeleton-first decomposition and it lacks iterative verifier feedback. Because iterative self-correction is a well-known and comparatively simple technique, the observed success rates could be fully explained by that component alone. That would not falsify the two-stage vision, but it would mean the paper's main empirical support does not actually support its stated contribution. The proposed ablation is cheap, concrete, and would settle the question. This does not change the overall verdict: the paper is honestly framed as a position paper with a prototype, its limitations are stated, and a conditional verdict remains appropriate pending stronger evidence. I credit the authors for openly listing manual specification verification and the small evaluation, and for sharing a demonstration video, but the missing artifact and the uncontrolled baseline are precisely why the evidence is not yet convincing.","tokens_in":7011,"tokens_out":6310,"duration_ms":68041,"concrete_test":"Re-run the feasibility study on the same three lemmas with at least 20 runs per arm and two additional conditions: (A) PROMETHEUS's exact iterative loop (verifier errors plus the same hints) but with the model prompted to output the complete Dafny proof directly, without first producing a high-level proof skeleton; (B) the skeleton-first prompt but with no iterative feedback. If arm A achieves verified-proof success rates statistically indistinguishable from the reported 4/5, 3/5, 3/5, then the claimed advantage of the two-stage decomposition is not established; if arm B also succeeds, then iterative feedback is the active ingredient. Report all prompts and generated Dafny code to make the comparison reproducible.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The feasibility study in Section III compares PROMETHEUS—which iteratively sends verifier errors and high-level hints back to the LLM—against a zero-shot baseline that gets a single attempt with no feedback. The reported jump from 0/5 to 3–4/5 could therefore be caused entirely by the iterative refinement loop and by the injected hints, rather than by the proposed separation into a high-level proof skeleton and low-level generated proofs. The paper's central assertion is specifically that this separation makes transformers viable; without an ablation that holds the feedback mechanism constant, the experiment cannot discriminate between the two-stage decomposition and a much simpler iterative self-correction strategy. The conclusion 'PROMETHEUS outperforms existing LLM-based verifiers' is also drawn without comparing against an iterative baseline. If iterative feedback alone accounts for the success, then the 'key observation' in Section I—that low-level omitted proof steps do not require deep intellectual effort—is not tested at all. The three selected lemmas are all elementary graph-theory facts, so even the success rate itself does not probe the generality of that assumption.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"This position paper argues that large language models can translate proofs from scientific papers into Dafny-verifiable code if the task is split into two stages: first, a high-level translation of the textual proof into a proof skeleton, and second, the iterative generation of low-level proof details that human text typically omits. The authors present a prototype, PROMETHEUS, built on Claude Sonnet 3.5, which interacts with Dafny by sending verifier errors and hand-authored hints back to the LLM. They evaluate it on three elementary graph-theory lemmas (handshake lemma, degree bounds, even cycle in bipartite graphs) and report success rates of 4/5, 3/5, and 3/5, respectively, against a zero-shot baseline that achieves 0/5 on all three. The paper also discusses challenges such as verifying formal specifications and the limits of LLM reasoning, and it frames the work as a feasibility study for a broader research agenda.","tokens_in":7231,"tokens_out":4837,"duration_ms":49685,"significance":"If the proposed two-stage decomposition works as claimed, it would meaningfully lower the barrier to formal verification and could enable the semi-automatic conversion of research-paper proofs into machine-checked code. The manuscript deserves credit for using Dafny as an external verifier, so the reported successes are not merely agreement with the prompt, and for explicitly acknowledging that the formal specifications were manually checked rather than automatically generated. The vision is plausible and timely. However, the current evidence is considerably weaker than the conclusions drawn from it: the experimental design does not isolate the two-stage decomposition from iterative feedback and hand-provided hints, no artifacts are provided, and the 'outperforms existing LLM-based verifiers' statement is made without any comparison. If the central mechanism is confirmed in future work, the significance would be high; as it stands, the paper is a useful position statement but does not yet substantiate its stronger empirical claims.","major_comments":[{"comment":"The comparison presented in Section III does not isolate the two-stage decomposition that the paper claims is responsible for the success. PROMETHEUS differs from the zero-shot baseline in at least three ways: it receives iterative verifier feedback, it is allowed multiple attempts, and it is supplied with manually chosen hints. The reported jumps from 0/5 to 3/5 or 4/5 are therefore equally consistent with a simpler explanation, namely that iterative self-correction plus hints suffices, with the proof-skeleton stage playing no special role. An ablation that holds the feedback and hint mechanism constant while toggling only the proof-skeleton stage is needed before the central claim in Section I ('we can break down the verification task into two main stages') is supported. Without such an ablation, the experiment cannot discriminate between the proposed method and a generic iterative refinement loop.","section":"Section III (Feasibility study)"},{"comment":"The manuscript provides no code, Dafny files, prompts, list of hints, or verification logs, and Section IV states that all formal specifications were manually verified before being given to PROMETHEUS. For a claim about automating text-to-verifiable-code generation, these details are load-bearing: the hand-chosen hints could encode much of the missing proof structure, and the manually verified specifications establish the correctness of the 'foundational truth' that the LLM relies on. I ask the authors to release an artifact containing the exact prompts, the full hint set, the input specifications, and the successful and failed Dafny outputs, and to quantify how much of the generated proof is attributable to the hints. This is a standard expectation for empirical claims in this area and is obtainable within the manuscript's scope.","section":"Sections III and IV (Reproducibility and manual specification)"},{"comment":"The conclusion that 'PROMETHEUS outperforms existing LLM-based verifiers' is not supported by the evidence: no existing tool is run on the same lemmas, and the cited systems (Clover, Dafny-induct, Laurel) appear only in related work. Since the baseline receives a strictly weaker protocol, the comparison cannot establish superiority of this method, let alone of the two-stage idea. I recommend either adding comparative runs on identical inputs and with comparable feedback protocols, or explicitly restricting the claim to a feasibility demonstration rather than an outperformance result.","section":"Section III (Comparative claim)"},{"comment":"The central assumption of the two-stage strategy is stated in Section I: 'such low-level proofs do not require deep intellectual effort.' This assumption is load-bearing because if omitted proof steps sometimes encode conceptually important reasoning, the low-level generation stage will fail exactly where the textual proof is most informative. The evaluation does not test this assumption: all three lemmas are standard, short, and in a single domain, and their omitted details are indeed mechanical. A test on a proof where the paper omits a nontrivial case distinction or relies on an unstated invariant would be needed to show that the assumed division of labor holds outside the simplest examples. Until such evidence exists, the vision is plausible but the feasibility result remains narrow.","section":"Sections I and IV (Key assumption)"}],"minor_comments":[{"comment":"In the discussion after the book proof, the assertion is written as '|X| = sum_{v in V} d(x)'; the argument of d should be v, not x, since the summation is over vertices. This typo obscures the otherwise clear explanation.","section":"Section II"},{"comment":"Five runs per lemma is a small sample, and the paper does not report whether the runs are independent, what the failed runs looked like, or how close they came to success. Please add per-run details and state the configuration of the LLM (temperature, sampling, etc.) used for the runs.","section":"Section III (Table 1)"},{"comment":"References [3] and [18] contain bare 'Link to article' placeholders instead of full bibliographic information; these need to be completed before publication.","section":"References"},{"comment":"The sentence 'PROMETHEUS always starts with a proof skeleton, delves into the low-level details, and refines them iteratively' describes an implementation invariant, but no trace or log is shown to support the word 'always.' Please clarify whether this is a guaranteed property of the system or an observed pattern in the successful runs.","section":"Section III"}],"recommendation":"major_revision","confidential_remarks":"This is a reasonable position paper, and I see no signs of misconduct: the use of Dafny as an external verifier prevents circularity, and the authors are candid about several limitations. My main reservation is that the empirical claims are materially ahead of the evidence: the experimental design confounds iterative feedback with the proposed two-stage decomposition, no artifact is provided, and the outperformance claim is untested against any existing tool. The stress-test concern about the zero-shot baseline is valid and has been incorporated into the major comments. I would ask the editor to require an artifact and an ablation in the revision, or, if the journal is willing to treat this strictly as a vision paper, to have the authors remove or sharply qualify the comparative claims."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Read it. The paper is a position piece with a small prototype, and on those terms it mostly works. The two-stage idea—first translate a textual proof into a high-level Dafny skeleton, then let an LLM fill low-level proof obligations with verifier feedback—is sensible and clearly explained. The three small experiments (handshake lemma, degree bounds, even cycle bipartite) are honest feasibility demos, and the authors openly say the formal specifications were manually verified and full automation is future work. That candor is genuine, and the writing is unusually direct.\n\nWhat's new is the specific combination and the reported success rates: zero-shot baseline gets 0/5, PROMETHEUS gets 3–4/5 on these lemmas. That's a real data point, small as it is.\n\nThe soft spots are in the evidence, not the idea. The biggest one is exactly what the stress-test note says: the experiment compares a zero-shot, single-attempt baseline against PROMETHEUS, which gets iterative verifier feedback and hand-chosen hints. So the 0/5→3–4/5 jump could come entirely from the refinement loop, not from the two-stage decomposition. The paper needs an ablation that holds feedback constant—e.g., a single-stage LLM with the same iterative loop—before it can claim the skeleton split is what matters. Relatedly, the sentence 'PROMETHEUS outperforms existing LLM-based verifiers' is not supported by the data: there's no comparison against Clover, Laurel, or any iterative baseline. The three lemmas are also all elementary graph-theory facts, so the load-bearing assumption that omitted proof steps are 'low-level' and don't require deep thought is plausible but essentially untested. And with no code or Dafny files shipped, independent reproduction is harder than it should be.\n\nNone of this kills the paper, but it does mean the central claim is conditional, not demonstrated. For a position paper that's acceptable; the authors mostly frame it as a feasibility prototype. I'd suggest revisions that add an ablation and an honest comparison, and soften the 'outperforms' claim.\n\nWho gets value: anyone working on LLM-assisted formal verification, and people thinking about how to evaluate such systems. Worth a serious referee, not a desk reject. I'd bring it to reading group as an example of a position paper that is clear about its limitations but whose conclusions outrun its experiments.","headline":"A candid, readable position paper with a small prototype that works on three toy lemmas, but the experiment can't pin the success on the two-stage split rather than iterative feedback.","tokens_in":7711,"tokens_out":2850,"would_cite":true,"duration_ms":24989,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"A transformer-based system can turn human proofs from research papers into verifiable Dafny code, provided the work is split into a high-level proof skeleton and iteratively generated low-level lemmas.","keywords":["formal verification","transformers","large language models","Dafny","proof skeleton","iterative proof generation","graph theory lemmas","LLM code generation"],"falsifier":"Run PROMETHEUS on a set of published proofs in which, by construction, the omitted step is a non-obvious invariant or case split that a human expert had to supply; if the success rate drops to near zero on those examples while staying high for proofs whose gaps are purely mechanical, the central premise is falsified.","tokens_in":6825,"feed_emoji":"✅","tokens_out":10907,"duration_ms":97652,"temperature":0.7,"pith_summary":"This position paper argues that large language models can bridge the gap between human-written research proofs and formal verification, if the task is split in the right way. The authors' key claim is that transformers should only translate the textual proof into a high-level code skeleton, while a second stage uses the same model to fill in the low-level proof obligations that human authors routinely omit. To support the vision, they build a prototype called PROMETHEUS that iterates between the LLM and the Dafny verifier, sending back error messages and high-level hints until proofs go through. The prototype succeeds on three graph-theory lemmas—handshake, degree bounds, even-cycle bipartite—whereas zero-shot LLM generation produces no verifiable proofs at all. If this separation generalizes, formal verification would no longer demand deep proof-engineering expertise, and decades of published algorithms could be retro-verified automatically.","feed_headline":"Two-stage pipeline turns textbook proofs into verified code","feed_subtitle":"In the paper's tests, the two-stage prototype verifies three graph lemmas where one-shot LLM generation fails every time.","key_machinery":"The mechanism is the two-stage separation of responsibilities. In stage one, the transformer translates the natural-language proof into a high-level Dafny skeleton, exploiting the near one-to-one correspondence between the prose proof steps and verifier statements; the verifier is allowed to assume the unproved low-level details. In stage two, the system repeatedly sends the verifier's output and high-level hints—induction, extension equalities, missing preconditions—back to the LLM, which generates the low-level lemmas needed to discharge the assumptions. PROMETHEUS is the prototype that instantiates this loop, and the Dafny verifier is the referee that decides when the generated code is complete.","core_discovery":"Naively asking an LLM to turn a mathematical statement and its human proof into Dafny code fails because verifiers operate at a far lower level than human exposition, requiring every recursive definition and set-cardinality identity to be proved explicitly. The paper's discovery is that this failure is a task-decomposition problem, not a model-capability problem: first let the transformer map the natural-language proof onto a high-level Dafny proof skeleton, exactly the kind of near one-to-one translation transformers are good at; then let the same model generate the omitted low-level lemmas one at a time, guided by verifier feedback and hints about recurring Dafny proof patterns. Prototype PROMETHEUS follows this two-stage loop and verifies the handshake lemma in four of five runs and the degree-bounds and even-cycle-bipartite lemmas in three of five runs, while the zero-shot baseline verifies none of the fifteen attempts.","pith_inferences":["Because the prototype's success is judged by whether Dafny accepts the proof, a stronger claim would require independently checking that the formal specification faithfully reflects the theorem as stated in natural language; the paper already flags specification checking as a human task.","A direct scale-up would be to run the pipeline over a corpus of published graph-theory and networking lemmas with mixed gap sizes, measuring success rate as a function of the number and depth of omitted steps.","If the two-stage premise holds, the limiting skill for formal verification shifts from proof engineering to writing precise formal specifications, so automating specification synthesis from natural language becomes the next bottleneck.","The same skeleton-then-fill loop could in principle be adapted to other verifiers besides Dafny, since the feedback cycle only needs a tool that reports unresolved proof obligations; the paper does not test this extension."],"forward_implications":["Formal verification of published research would shift from proof engineering to specification checking: the LLM produces both the proof skeleton and the mechanical lemmas, while a human verifies that the formal specification captures the intended theorem.","Transformer-based verifiable-code tools should abandon one-shot proof generation; the paper's experiments show zero-shot prompting verifies none of the attempts, whereas iterative skeleton-then-lemmas succeeds in most runs.","The same two-stage separation is expected to transfer beyond graph-theory examples to other domains, since the prototype's principles are not tied to a particular subject matter.","A later stage of the vision would use the accumulated verified formal proofs as a basis for systems that not only verify known algorithms but also create novel algorithms together with proofs.","Specialized smaller transformers could be trained on the recurrent low-level proof patterns, streamlining the second stage instead of relying on a general-purpose model."],"supporting_citations":[{"why":"Provides the textbook statement and proof of the handshake lemma that serve as the natural-language input to the prototype.","marker":"[16]"},{"why":"Supplies the Dafny verifier that defines the target formalism and returns the error feedback used to drive iterative refinement.","marker":"[17]"},{"why":"Documents an existing closed-loop verifiable-code generator that barely scales beyond single-loop programs, giving the prior-art baseline this comparison must beat.","marker":"[11]"},{"why":"Describes earlier AI-assisted synthesis of verified Dafny methods, cited as evidence that transformer-based systems for verifiable code do not yet scale.","marker":"[12]"},{"why":"Presents an LLM-based tool for generating Dafny assertions, another comparison point showing that current systems lack low-level proof details.","marker":"[13]"},{"why":"Introduces the transformer architecture, the sequence-to-sequence translation ability that the high-level skeleton stage exploits.","marker":"[7]"},{"why":"Reports limits of LLMs in relational reasoning, supporting the paper's claim that low-level but pattern-like proofs are the right task for them.","marker":"[14]"},{"why":"Describes verification brittleness in Dafny, motivating the intermediate assertions and hints that the prototype uses.","marker":"[5]"}],"fun_headline_variants":["LLM proof-to-code pipeline beats zero-shot on graph lemmas","Transformers turn paper proofs into verified code in two stages","Two-stage prompting verifies graph lemmas that one-shot LLMs miss","From math paper to Dafny: prototype splits proof into verifiable steps"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The load-bearing premise is that proof steps omitted from published papers are mostly low-level and mechanical, so an LLM can invent them without deep insight; if omitted steps sometimes contain the conceptual core of the argument, the two-stage approach will not generalize.","fun_headline_variants_meta":{"raw":{"variants":["LLM proof-to-code pipeline beats zero-shot on graph lemmas","Transformers turn paper proofs into verified code in two stages","Two-stage prompting verifies graph lemmas that one-shot LLMs miss","From math paper to Dafny: prototype splits proof into verifiable steps"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000793,"raw_usage":{"total_tokens":3475,"prompt_tokens":912,"completion_tokens":2563,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":528,"completion_tokens_details":{"reasoning_tokens":2487}},"tokens_in":528,"tokens_out":2563,"duration_ms":20378,"temperature":1.0,"reasoning_tokens":2487,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-10T21:13:28.614610+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Run PROMETHEUS on a set of published proofs in which, by construction, the omitted step is a non-obvious invariant or case split that a human expert had to supply; if the success rate drops to near zero on those examples while staying high for proofs whose gaps are purely mechanical, the central premise is falsified.","supporting_citations":[{"cited_title":"Graph Theory,","cited_arxiv_id":null,"evidence_quote":"Provides the textbook statement and proof of the handshake lemma that serve as the natural-language input to the prototype."},{"cited_title":"Accessible Software V erification with D afny ,","cited_arxiv_id":null,"evidence_quote":"Supplies the Dafny verifier that defines the target formalism and returns the error feedback used to drive iterative refinement."},{"cited_title":"Clover: Closed-loop verifiable code generation,","cited_arxiv_id":null,"evidence_quote":"Documents an existing closed-loop verifiable-code generator that barely scales beyond single-loop programs, giving the prior-art baseline this comparison must beat."},{"cited_title":"Towards AI-assisted synthesis of verified Dafny methods,","cited_arxiv_id":null,"evidence_quote":"Describes earlier AI-assisted synthesis of verified Dafny methods, cited as evidence that transformer-based systems for verifiable code do not yet scale."},{"cited_title":"Attention is all you need,","cited_arxiv_id":null,"evidence_quote":"Introduces the transformer architecture, the sequence-to-sequence translation ability that the high-level skeleton stage exploits."},{"cited_title":"Llms for relational reasoning: How far are we?","cited_arxiv_id":null,"evidence_quote":"Reports limits of LLMs in relational reasoning, supporting the paper's claim that low-level but pattern-like proofs are the right task for them."},{"cited_title":"Avoiding verification brittlene ss in Dafny,","cited_arxiv_id":null,"evidence_quote":"Describes verification brittleness in Dafny, motivating the intermediate assertions and hints that the prototype uses."}],"review_version":1}