Automatic and Verifiable Synthesis of Implementations from Mathematical Models
Bibliographic record
Abstract
Many applications in image processing, control systems and other areas, have very well understood mathematical models. Optimization problems, in particular, are a class of (implicit) models which is particularly useful. When faced with the task to develop such an application, a software engineer aware of best practices might use a computer algebra system to compute some problem-specific quantities which are then put into a simulation environment (such as Matlab), and ultimately translated to code. Such a process requires the development of multiple versions of the mathematical model, often by hand, in tools with widely varying levels of formalism, which are generally susceptible to soundness problems. Moreover, it may be very difficult to decide whether the various models are in fact equivalent. Through an extended example of a multidimensional Newton’s Method, we demonstrate how computer algebra and theorem proving systems can be used to largely automate this process. We compute problem-specific quantities, including higher-order ones, verify their correctness, and automatically generate code which is verifiably correct. The process combines untrusted components with trusted ones so that failure in an untrusted component is always detected.
Fetched live from OpenAlex and de-inverted. Abstracts are not stored in this database: the inverted indexes are 8.6 GB of the frame’s 9.3 GB of text, and the host has 13 GB free.
How this classification was reachedexpand
Full frame machine prediction
Teacher imitationNot calibrated prevalence, not ground truth. Human validation pending. The Gemma side is a direct model label for every work in the frame, read from the title-only record. The Codex side is a classifier learned from the 10,348 direct Codex labels and calibrated to design-weighted sample rates; fields without enough sample support carry no Codex call. Candidate is the union of the two sides; consensus is their intersection. These outputs are machine_predicted_unvalidated and are not human labels.
Distilled classifier scores by category (both heads)
| Category | Codex | Gemma |
|---|---|---|
| Metaresearch | 0.005 | 0.017 |
| Meta-epidemiology (narrow) | 0.001 | 0.001 |
| Meta-epidemiology (broad) | 0.001 | 0.002 |
| Bibliometrics | 0.001 | 0.001 |
| Science and technology studies | 0.001 | 0.003 |
| Scholarly communication | 0.002 | 0.003 |
| Open science | 0.002 | 0.003 |
| Research integrity | 0.001 | 0.002 |
| Insufficient payload (model declined to judge) | 0.005 | 0.001 |
Machine scores (provisional)
The two teacher heads of the student model, read on this work. A score orders the frame for review; it never asserts a category, and the validation status ships verbatim with every row.
Baseline scores from an immature model (maturity gate not passed, 7 training rounds). Scores rank; they never assert a category.
score_only:v0-immature-baseline · verbatim from the scoring run: score_only means the number may rank works, and no category label ships from itClassification
machine, unvalidatedMachine predicted; a candidate call from one source (direct Gemma or distilled Codex), not a consensus.
How this classification was reached, model by model and score by score, is at the end of the page under "How this classification was reached".