Semi-Automation of Meta-Theoretic Proofs
Bibliographic record
Abstract
Beluga is a proof assistant designed for the mechanization of programming languages and other formal systems.An interactive tactic-based prover Harpoon was recently deployed, and though it was designed to ease usability for Beluga's users, much human interaction is still required for its proof developments.We develop a theoretical foundation for a semi-automated proof search procedure within Beluga in the form of a two-level focusing calculus and implement it through the tactic auto-invert-solve.The focusing calculus is sound and complete with respect to the sequent calculus for the fragment that we are automating.Once a case analysis has been conducted, auto-invert-solve searches for a focused uniform proof of a subgoal via a bounded depth-first search by using all available assumptions.Upon completion of a proof, auto-invert-solve produces a proof witness in the form of a program that is independently type-checked against the subgoal and subsequently spliced into the proof script.Our aim is to automate the tedious cases of proof development, leaving only the interesting cases to the user.We have utilized auto-invert-solve to simplify several common theorems including type preservation and value soundness for MiniML, weak-head normalization for the simply-typed lambda-calculus, and the Church-Rosser theorem for the untyped lambda-calculus.In these case studies, we demonstrate that auto-invert-solve reduces the amount of user interaction needed to complete large and complex proofs by automatically solving simple subgoals and helper lemmas.
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 distilled prediction
Teacher imitationNot calibrated prevalence, not ground truth. Human validation pending. Learned from the 10,348 direct Codex labels and 10,348 direct Gemma labels. Candidate is the union of thresholded teacher heads; consensus is their intersection. These outputs are machine_predicted_unvalidated and are not human labels or direct frontier model labels.
Codex and Gemma teacher scores by category
| Category | Codex | Gemma |
|---|---|---|
| Metaresearch | 0.002 | 0.001 |
| Meta-epidemiology (narrow) | 0.001 | 0.001 |
| Meta-epidemiology (broad) | 0.001 | 0.001 |
| Bibliometrics | 0.001 | 0.001 |
| Science and technology studies | 0.001 | 0.000 |
| Scholarly communication | 0.000 | 0.001 |
| Open science | 0.002 | 0.000 |
| Research integrity | 0.001 | 0.001 |
| Insufficient payload (model declined to judge) | 0.000 | 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 teacher head, 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".