Pith. sign in

REVIEW 4 major objections 5 minor 48 references

Solver-generated simplified queries let a language model verify optimization formulations against natural-language descriptions, improving accuracy and yielding a high-precision self-verification signal.

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

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

VeriSimpl improves natural-language-to-optimization translation by using the solver to generate simplified feasibility and variable-inference queries that an LLM checks against the problem text.

T0 review reviewed 2026-08-02 challenge →

load-bearing objection Genuinely new solver-guided verification trick with consistent gains, but 'verified' only means self-consistency and the paper lacks code, data, and error bars. the 4 major comments →

arxiv 2607.20474 v1 pith:PMZJXJ7J submitted 2026-05-24 cs.AI

VeriSimpl: Robust Optimization Modeling from Natural Language using Simplification-based Verification

Sumaya Abdul Rahman , Seckhen Ariel Andrade Cuellar , Ghani Raissov , Mohammad Raza This is my paper
classification cs.AI
keywords optimization modelingnatural language to solverLLM verificationsolver-guided verificationconstraint mutationvariable maskingmixed-integer linear programmingself-verification
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

VeriSimpl seeks to make natural-language-to-optimization translation trustworthy by turning the solver into a source of verification questions. Instead of asking the LLM to propose test cases, the solver mutates each constraint into strict, boundary, and violation variants and produces concrete witness valuations, and it masks subsets of decision variables, including the full set, to produce completion queries. The LLM reasons about each simplified query from the task description alone, and when its answer matches the solver's output, the query passes. The paper claims this consistently improves end-to-end formulation accuracy over prior systems across four benchmarks, and that when all queries pass, the chosen formulation is correct with 91.5% precision using one strong base model and 78.5% using another. The approach also yields a self-verification signal with high precision but modest coverage, which can reduce the manual inspection burden in practice.

Core claim

The central discovery is that an optimization solver can be used not just to solve a candidate model but to generate simplified diagnostic queries that make correctness tractable for an LLM. For constraints, the solver solves mutated versions of each constraint under strict, equality, and violation variants and supplies concrete valuations; the LLM judges feasibility against the natural-language description. For variables, the solver finds an optimal valuation, then reveals all but a small subset, or none, of the variables and asks the LLM to predict the hidden ones from the description. Consistency between solver output and LLM reasoning across these queries is aggregated into a verificatio

What carries the argument

Simplification-based verification: solver-generated diagnostic queries along two dimensions. Constraint-mutation feasibility checks normalize each constraint and solve three mutated variants (strict, equality, violation), using the solver's witness valuations as concrete test cases for the LLM. Variable-masking valuation checks hide one decision variable at a time, or the full variable set, under a solver-optimal fixed global context and ask the LLM to infer the hidden values. These queries reduce the LLM's reasoning to local, concrete tasks while preserving the global semantic structure of the original formulation, and consistency with solver results is the verification signal.

Load-bearing premise

Verification assumes the candidate program already defines the right decision variables and covers every part of the natural-language description; it only checks consistency between solver outputs and LLM reasoning within that assumed framing.

What would settle it

Run the full pipeline on a problem whose correct solution depends on a non-obvious variable meaning, such as shift-start count versus per-period staffing, or on a cost term mentioned only implicitly in the description. If all simplification queries pass and the returned solution is still wrong, the claim that full verification is a high-precision signal fails; the paper's own failure cases are concrete instances of this.

Watch this falsifier. Get emailed when new claim-graph text bears on it.

If this is right

  • Higher end-to-end accuracy than direct prompting and existing NL-to-solver systems on all four benchmarks, with gains consistent across different base models.
  • A high-precision self-verification signal: when full verification passes, the formulation is correct in roughly 91.5% of cases with one strong base model and 78.5% with another, so users can trust a substantial verified subset without manual review.
  • The method is solver- and LLM-agnostic, so improvements in either component should transfer directly to improved formulation accuracy and verification precision.
  • The complementary verification signals—constraint feasibility, singleton variable masking, full variable masking, and type checking—each contribute, and ablations show that no single signal is sufficient on its own.
  • Coverage is modest, around 23–34%, meaning many correct solutions fail full verification; the signal is best used as a confidence filter rather than a complete correctness proof.
  • The paper's own failure cases show that a shared misinterpretation of the natural-language description can let an incorrect formulation pass verification, which limits the claim to formulations whose variable definitions and coverage are already correct.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The simplification principle likely generalizes beyond optimization: any domain where a reliable backend can construct concrete witnesses from candidate formalizations—planning, satisfiability, theorem proving—could use the same 'solver asks, LLM answers' pattern; the paper hints at this but leaves it untested.
  • Precision could be raised by adding variable-definition and coverage-oriented queries that check whether every part of the natural-language description is represented, since the paper's failure cases are exactly shared misinterpretations of variable meaning and omitted costs or aspects.
  • A practical two-stage workflow suggests itself: automatically accept fully verified cases, route the rest to human review. The precision/coverage tradeoff, around 91.5% precision at 34% coverage, makes this viable even though full verification is incomplete.
  • Because the LLM and solver can share the same misinterpretation, using multiple independent reasoning paths or varying the framing of feasibility queries might reduce correlated false positives.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Referee Report

4 major / 5 minor

Summary. The paper introduces VeriSimpl, a solver–LLM framework for translating natural-language optimization problems into executable solver code. The method samples K candidate Gurobi programs, then uses the solver to generate simplification-based verification queries: constraint mutations (strict/equality/violation) with concrete witness valuations, and variable-masking valuation queries under a solver-optimal assignment. The LLM answers these queries against the natural-language description, and the resulting consistency scores are aggregated lexicographically to select the best candidate. The paper reports end-to-end accuracy on four benchmarks (NL4Opt, NLP4LP, CompOR, IndOR) with GPT-4o, R1, and Mistral, and reports a self-verification precision/coverage analysis showing precision above 90% (GPT-4o) on fully verified cases.

Significance. The core idea is novel and practically motivated: instead of asking the LLM to propose test cases, the solver constructs simplified diagnostic queries that expose local constraint semantics and global objective relationships. The empirical gains over strong baselines are consistent across three base models and four datasets, and the failure analysis in Appendix B is candid about structural blind spots. If the results hold under stricter statistical reporting, the approach would be a useful step toward reliable NL-to-optimization interfaces. The paper is also clearly written and the algorithms are presented in a model-agnostic way. However, the self-verification precision claim is conditional on the verifier's representational coverage, and the empirical evaluation lacks error bars and significance tests, which limits the strength of the central claims as currently stated.

major comments (4)
  1. [§4.2, Table 3; App. B] The reported self-verification precision is presented as an unconditional property of the system, but the verifier is structurally blind to two error classes: incorrect decision-variable semantics and entirely omitted aspects of the NL description. CONSTRAINTVERIFY (Alg. 2) only mutates constraints present in the candidate program; VARVERIFY (Alg. 3) only masks variables present in the candidate program. Appendix B documents exactly these failure modes (Problem 52: shift-start variables misinterpreted as per-period headcounts; Problem 86: objective omitting raw-material costs). Consequently the precision figures (91.5% GPT-4o, 78.5% R1) measure agreement only among errors representable by the candidate program's variables/constraints. The Abstract and §1 claims of a 'high-precision self-verification signal' need to be scoped accordingly—e.g., by defining precision conditional on verifier
  2. [§4.1, Tables 1–2] No variance or significance measures are reported. Some of the reported gains are modest relative to the sample sizes: CompOR contains only 17 problems, so a single problem accounts for ≈5.9 percentage points; on Mistral, CompOR accuracy ties SELFDEBUG at 70.6 (Table 10). No confidence intervals, per-seed breakdowns, or significance tests are given. Additionally, the COE baseline results are quoted from the original paper (Xiao et al., 2024) rather than re-run under the same harness and prompts, making the comparison inconsistent with the other baselines. Please provide error bars or significance tests, release per-problem results, and either re-run COE under the same conditions or clearly label it as a reported baseline.
  3. [§4, Datasets] The NL4Opt preprocessing is underspecified: the paper says the test split is used 'after removing some infeasible cases' without giving the exact number of removed problems, the criteria for 'infeasible', or whether the removed cases differ from prior work's exclusions. Similarly, the exact subset of CompOR used (17 problems) is not identified. This limits reproducibility and comparability with prior results on full splits. Please specify the filtering criteria, provide the problem IDs or release scripts that reproduce the exact splits, and clarify the licenses/availability of the datasets.
  4. [§4.4, App. B, §6] The paper's own limitation statement says decision variables are 'assumed as given' and simplification queries do not cover aspects 'completely missed or ignored' by the candidate program. This is not a peripheral caveat; it is the central weakness of the method as a verification signal. Since the contribution is framed as a verification mechanism, the paper should either (a) add a verification step for variable definitions and NL coverage, or (b) systematically restrict all claims to the conditional setting and explicitly state when the signal is safe to use. As written, the conclusion in §6 that the method 'provides a high-precision self-verification signal' is too strong relative to the evidence in the paper's own failure analysis.
minor comments (5)
  1. [App. A.2, A.3] The displayed LLM reasoning in these success cases uses different numerical values from the stated problem descriptions. In A.2, the reasoning refers to '2 units of pollution' and 'total trips must not exceed 4', while the problem states 40 pollution units and a 20-trip limit. In A.3, the reasoning says 'must take at least one child' and 'up to two children' while the problem states at least three and at most four children, and the costs do not match. Please correct these examples or clarify that they are from different instances; as shown, they undermine the illustrative value of the success cases.
  2. [§4.4] Typo: 'Theses cases highlight limitations' should read 'These cases ...'.
  3. [Algorithm 1, line 5] The set-builder notation '{u} | u∈ V' is malformed; should be '{ {u} : u ∈ V }'.
  4. [§2] The phrase 'the solver computes a ground-truth result' is misleading, because the simplified query is derived from the candidate program rather than from the natural-language specification. Suggest 'reference result' or 'program-derived result' to avoid implying an independent oracle.
  5. [Abstract, throughout] The name is typeset inconsistently as 'VeriSimpl' in the title/abstract and 'VERISIMPL' in the body; please standardize.

Circularity Check

0 steps flagged

No significant circularity: the self-verification signal is an empirically evaluated consistency check with acknowledged blind spots, not a derivation that reduces to its inputs.

full rationale

VeriSimpl's verification pipeline is not circular in the mathematical sense. The solver generates queries from the candidate program, and the LLM is asked to reason from the natural-language description; agreement is an empirical outcome, not a tautology. The paper's own Appendix B documents false positives (e.g., Problem 52 and Problem 86) where variable-masking degenerates into a constrained-completion problem and verification passes despite an incorrect model. These are important correctness limitations and blind spots, but they do not make the central claim circular: the reported precision is measured against ground-truth benchmarks, and the method can and does fail. The only self-citation (Raza & Milic-Frayling, 2025) appears in related work and is not load-bearing. Score 2 reflects the acknowledged self-consistency blind spots and the minor self-citation, not a circular derivation.

Axiom & Free-Parameter Ledger

3 free parameters · 5 axioms · 0 invented entities

The method rests on solver correctness and LLM query-answering reliability, plus two paper-specific design choices: the constraint-mutation scheme with margin delta and lexicographic score aggregation. No constants are fitted to the benchmark data, but delta, K, and the singleton-masking cap are unspecified hyperparameters that could affect the reported numbers.

free parameters (3)
  • Constraint mutation margin delta
    Algorithm 2 replaces constraint e(V)<=0 with mutations e<=-delta, e=0, e>=+delta. The value of delta is not given and no sensitivity analysis is reported.
  • Number of candidate programs K = <=10
    Algorithm 1 samples K programs; accuracy and cost may depend on K, but no ablation over K is reported.
  • Singleton masking cap
    The implementation imposes a fixed upper bound on the number of singleton variables considered for masking; the bound is not specified.
axioms (5)
  • domain assumption SOLVE returns correct status and valuation for the instantiated model.
    Algorithms 1-3 treat solver output as ground truth for query generation and final selection; if the solver were unreliable, verification would inherit the error.
  • domain assumption The LLM can correctly answer feasibility and valuation queries from the natural-language description alone.
    Core mechanism; Appendix B documents cases where this fails because the LLM and solver share a misinterpretation.
  • ad hoc to paper Constraint normalization e(V)<=0 and the three mutations (strict, equal, violated) with margin delta expose semantic errors in each constraint.
    Algorithm 2 assumes local constraint mutation with fixed global context is sufficient to detect constraint-semantics errors; no formal justification or margin sensitivity is provided.
  • domain assumption Decision-variable definitions are correct and no part of the NL description is unmodeled.
    Stated as a limitation in Section 4.4: verification does not cover wrong variable definitions or entirely missed aspects of the description.
  • ad hoc to paper Lexicographic scoring of constraint, singleton-variable, full-variable, and type checks ranks the most correct program highest.
    Algorithm 1 lines 7-10; supported only empirically by ablations, with no theoretical guarantee.

reviewed 2026-08-02 · how reviews work

0 comments
Cite this review

Pith. "Pith review of VeriSimpl: Robust Optimization Modeling from Natural Language using Simplification-based Verification." pith.science (2026). https://pith.science/paper/PMZJXJ7J

@misc{pith2026260720474,
  author       = {Pith},
  title        = {Pith review of: VeriSimpl: Robust Optimization Modeling from Natural Language using Simplification-based Verification},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/PMZJXJ7J}},
  note         = {Machine review of arXiv:2607.20474}
}
Share X Bluesky LinkedIn Reddit HN
read the original abstract

Natural language interfaces can greatly benefit the accessibility and usability of optimization modeling, and recent advances in large language models (LLMs) show promise in automatically translating textual problem descriptions into executable solver formulations. However, a key challenge for existing approaches is to ensure that the inferred formulation correctly implements the intended task, even if it may execute without errors. We introduce VeriSimpl, a solver LLM framework for robust natural-language-to-optimization formalization. Our approach is based on the idea of simplification-based verification, where the optimization solver is leveraged to generate simplified diagnostic queries about a candidate formulation to allow the LLM to tractably reason about the correctness of the formulation with respect to the task description. We present such simplification strategies along different dimensions with respect to problem constraints and decision variables, which allow the LLM to reason locally under fixed global contexts. Evaluations on a range of optimization benchmarks show how our approach provides consistent improvements in accuracy over existing methods, while also providing a novel high-precision self-verification signal.

Figures

Figures reproduced from arXiv: 2607.20474 by Ghani Raissov, Mohammad Raza, Seckhen Ariel Andrade Cuellar, Sumaya Abdul Rahman.

Figure 1
Figure 1. Figure 1: A sample optimization modelling problem. For a given natural language problem description, the LLM may generate the correct solver formulation or an incorrect one that looks very similar but contains subtle semantic errors that are difficult to detect. generation approaches often utilise unit tests or behavioral test cases generated from the task specification, such ap￾proaches are infeasible for optimizat… view at source ↗
Figure 2
Figure 2. Figure 2: The simplification-based verification pipeline: using solver-generated simplified queries for effective LLM reasoning a deeper way, using them jointly for formulation verification rather than relying on the solver solely for execution. Outline [PITH_FULL_IMAGE:figures/full_fig_p003_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: shows the accuracy gains for the ablation systems on each of the benchmark datasets. We observe that there are varying patterns for the different benchmark domains, show￾ing that no one verification feature performs consistently best across the different domains. However, A-FULLVAR mostly performs worse than the other features as can be expected from its lower coverage. 4.4. Qualitative analysis In Appendi… view at source ↗
Figure 5
Figure 5. Figure 5: Prompt for Gurobi code error correction Gurobi Code Error Correction Prompt System Prompt: You are a Gurobi Python code corrector. Your task is to correct the Gurobi Python code provided in the input. The input will contain the standard output and standard error messages from running a Gurobi Python file. You should analyze these messages and provide a corrected version of the Gurobi Python code. If there … view at source ↗

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

48 extracted references · 3 linked inside Pith

  1. [1]

    T. M. Mitchell. The Need for Biases in Learning Generalizations. 1980

    1980

  2. [2]

    M. J. Kearns , title =

  3. [3]

    Machine Learning: An Artificial Intelligence Approach, Vol. I. 1983

    1983

  4. [4]

    R. O. Duda and P. E. Hart and D. G. Stork. Pattern Classification. 2000

    2000

  5. [5]

    Suppressed for Anonymity , author=

  6. [6]

    Newell and P

    A. Newell and P. S. Rosenbloom. Mechanisms of Skill Acquisition and the Law of Practice. Cognitive Skills and Their Acquisition. 1981

    1981

  7. [7]

    A. L. Samuel. Some Studies in Machine Learning Using the Game of Checkers. IBM Journal of Research and Development. 1959

    1959

  8. [8]

    2022 , eprint=

    STaR: Bootstrapping Reasoning With Reasoning , author=. 2022 , eprint=

    2022

  9. [9]

    Aho and Jeffrey D

    Alfred V. Aho and Jeffrey D. Ullman , title =. 1972

    1972

  10. [10]

    Publications Manual , year = "1983", publisher =

    1983

  11. [11]

    Chandra and Dexter C

    Ashok K. Chandra and Dexter C. Kozen and Larry J. Stockmeyer , year = "1981", title =. doi:10.1145/322234.322243

    arXiv 1981

  12. [12]

    Scalable training of

    Andrew, Galen and Gao, Jianfeng , booktitle=. Scalable training of

  13. [13]

    Dan Gusfield , title =. 1997

    1997

  14. [14]

    Tetreault , title =

    Mohammad Sadegh Rasooli and Joel R. Tetreault , title =. Computing Research Repository , volume =. 2015 , url =

    2015

  15. [15]

    A Framework for Learning Predictive Structures from Multiple Tasks and Unlabeled Data , Volume =

    Ando, Rie Kubota and Zhang, Tong , Issn =. A Framework for Learning Predictive Structures from Multiple Tasks and Unlabeled Data , Volume =. Journal of Machine Learning Research , Month = dec, Numpages =

  16. [16]

    Chain-of-Experts: When

    Ziyang Xiao and Dongxiang Zhang and Yangjun Wu and Lilin Xu and Yuan Jessica Wang and Xiongwei Han and Xiaojin Fu and Tao Zhong and Jia Zeng and Mingli Song and Gang Chen , booktitle=. Chain-of-Experts: When. 2024 , url=

    2024

  17. [17]

    Mistral Large: Flagship Model Launch , year =

  18. [18]

    2024 , howpublished =

    Hello GPT-4o , author =. 2024 , howpublished =

    2024

  19. [19]

    arXiv preprint arXiv:2501.12948 , year=

    Deepseek-r1: Incentivizing reasoning capability in llms via reinforcement learning , author=. arXiv preprint arXiv:2501.12948 , year=

    Pith/arXiv arXiv

  20. [20]

    European Journal of Operational Research , volume=

    A survey of contextual optimization methods for decision-making under uncertainty , author=. European Journal of Operational Research , volume=. 2025 , publisher=

    2025

  21. [21]

    2009 , publisher=

    Logic and integer programming , author=. 2009 , publisher=

    2009

  22. [22]

    Gurobi Optimizer , year =

  23. [23]

    IBM ILOG CPLEX Optimization Studio , year =

  24. [24]

    Mathematical Programming Computation , volume=

    SCIP: solving constraint integer programs , author=. Mathematical Programming Computation , volume=. 2009 , publisher=

    2009

  25. [25]

    ACM Computing Surveys , year=

    A systematic survey on large language models for algorithm design , author=. ACM Computing Surveys , year=

  26. [26]

    2024 , series =

    Ahmaditeshnizi, Ali and Gao, Wenzhi and Udell, Madeleine , booktitle =. 2024 , series =

    2024

  27. [27]

    arXiv preprint arXiv:2405.17743 , year=

    ORLM: Training Large Language Models for Optimization Modeling , author=. arXiv preprint arXiv:2405.17743 , year=

    Pith/arXiv arXiv

  28. [28]

    ICLR , ee =

    Chen, Xinyun and Lin, Maxwell and Schärli, Nathanael and Zhou, Denny , biburl =. ICLR , ee =

  29. [29]

    The Twelfth International Conference on Learning Representations , year=

    Large Language Models as Optimizers , author=. The Twelfth International Conference on Learning Representations , year=

  30. [30]

    arXiv , url =

    Li, Beibin and Mellou, Konstantina and Zhang, Bo and Pathuri, Jeevan and Menache, Ishai , title =. arXiv , url =. 2023 , month =

    2023

  31. [31]

    NeurIPS 2022 competition track , pages=

    Nl4opt competition: Formulating optimization problems based on their natural language descriptions , author=. NeurIPS 2022 competition track , pages=. 2023 , organization=

    2022

  32. [32]

    ICLR , year=

    LLMOPT: Learning to Define and Solve General Optimization Problems from Scratch , author=. ICLR , year=

  33. [33]

    Advances in Neural Information Processing Systems (NeurIPS) , year =

    Reflexion: Language Agents with Verbal Reinforcement Learning , author =. Advances in Neural Information Processing Systems (NeurIPS) , year =

  34. [34]

    International Conference on Software Maintenance and Evolution (ICSME), Tool Demonstrations , year =

    LLMLOOP: Improving LLM-Generated Code and Tests through Automated Iterative Feedback Loops , author =. International Conference on Software Maintenance and Evolution (ICSME), Tool Demonstrations , year =

  35. [35]

    arXiv preprint arXiv:2406.06864 , year =

    Validating LLM-Generated Programs with Metamorphic Prompt Testing , author =. arXiv preprint arXiv:2406.06864 , year =

    Pith/arXiv arXiv

  36. [36]

    SIGSOFT FSE Companion , editor =

    Bose, Dibyendu Brinto , biburl =. SIGSOFT FSE Companion , editor =

  37. [37]

    IEEE Transactions on Software Engineering , volume =

    Testing Programs with the Aid of a Compiler , author =. IEEE Transactions on Software Engineering , volume =

  38. [38]

    IEEE Computer , volume =

    Hints on Test Data Selection: Help for the Practicing Programmer , author =. IEEE Computer , volume =

  39. [39]

    IEEE Transactions on Software Engineering , volume =

    An Analysis and Survey of the Development of Mutation Testing , author =. IEEE Transactions on Software Engineering , volume =. 2011 , doi =

    2011

  40. [40]

    Advances in Computers , volume =

    Mutation Testing Advances: An Analysis and Survey , author =. Advances in Computers , volume =

  41. [41]

    Instantiation-based Formalization of Logical Reasoning Tasks Using Language Models and Logical Solvers

    Raza, Mohammad and Milic-Frayling, Natasa , biburl =. Instantiation-based Formalization of Logical Reasoning Tasks Using Language Models and Logical Solvers. , url =. IJCAI , ee =

  42. [42]

    Xi Ye and Qiaochu Chen and Isil Dillig and Greg Durrett , booktitle=. Sat. 2023 , url=

    2023

  43. [43]

    Logic-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning

    Pan, Liangming and Albalak, Alon and Wang, Xinyi and Wang, William Yang , biburl =. Logic-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning. , url =. EMNLP (Findings) , editor =

  44. [44]

    , biburl =

    Kalyanpur, Aditya and Saravanakumar, Kailash and Barres, Victor and Chu-Carroll, Jennifer and Melville, David and Ferrucci, David A. , biburl =. LLM-ARC: Enhancing LLMs with an Automated Reasoning Critic. , url =. CoRR , keywords =

  45. [45]

    Position:

    Subbarao Kambhampati and Karthik Valmeekam and Lin Guan and Mudit Verma and Kaya Stechly and Siddhant Bhambri and Lucas Paul Saldyt and Anil B Murthy , booktitle=. Position:. 2024 , url=

    2024

  46. [46]

    Proceedings of the 37th International Conference on Neural Information Processing Systems , articleno =

    Guan, Lin and Valmeekam, Karthik and Sreedharan, Sarath and Kambhampati, Subbarao , title =. Proceedings of the 37th International Conference on Neural Information Processing Systems , articleno =. 2024 , publisher =

    2024

  47. [47]

    and Staats, Charles and Jamnik, Mateja and Szegedy, Christian , biburl =

    Wu, Yuhuai and Jiang, Albert Qiaochu and Li, Wenda and Rabe, Markus N. and Staats, Charles and Jamnik, Mateja and Szegedy, Christian , biburl =. Autoformalization with Large Language Models. , url =. NeurIPS , editor =

  48. [48]

    ICLR , ee =

    Jiang, Albert Qiaochu and Welleck, Sean and Zhou, Jin Peng and Lacroix, Timothée and Liu, Jiacheng and Li, Wenda and Jamnik, Mateja and Lample, Guillaume and Wu, Yuhuai , biburl =. ICLR , ee =

This paper was first reviewed by deepseek-v4-flash on August 2, 2026.