Autoformalization for Ambiguous Inputs: Precision, Coverage, and Cost across SQL and Logical Forms

Henry Shen, Xinling Liao, Adarsh Vatsa, William Eiers

Agentic systems translate natural-language requests into executable artifacts while managing ambiguity and inference cost. We evaluate seven autoformalization workflows on SQL and first-order logic benchmarks for ambiguous inputs. Across five SQL workflows, the raw model leads with F1 of 53.35% on AMBROSIA and 60.85% on AmbiQT. On AmP, DRIFT gains 15.98 F1 points over the raw model at 2.03 times its token cost, whereas LoC uses 18.65 times the raw model's tokens with lower F1. Within AutoCedar, structured interpretation lowers F1 by 6.44-6.95 points and raises AMBROSIA token use 2.2-fold. Paired reviewer comparisons show modest Kimi K3 gains of 1.93 points on AMBROSIA and 2.04 on AmbiQT. Clear-ambiguous AMBROSIA analysis shows greater relative stability for AutoCedar, with a smaller F1 drop than the raw model (11.46 vs. 16.68 points), alongside lower aggregate F1 (50.16% vs. 53.35%). Autoformalization alone does not guarantee robustness to ambiguity: the tested additions offer no uniformly effective remedy, making accuracy, ambiguity handling, and inference cost joint design requirements.