The Proof is in the Pudding: Using Automated Theorem Proving to Generate Cooking Recipes
This paper presents FASTFOOD, a rule-based Natural Language Generation Program for cooking recipes. Recipes are generated by using an Automated Theorem Proving procedure to select the ingredients and instructions, with ingredients corresponding to axioms and instructions to implications. FASTFOOD also contains a temporal optimization module which can rearrange the recipe to make it more time-efficient for the user, e.g. the recipe specifies to chop the vegetables while the rice is boiling. The system is described in detail, using a framework which divides Natural Language Generation into 4 phases: content production, content selection, content organisation and content realisation. A comparison is then made with similar existing systems and techniques.
Code (1)
Tasks
Automated Theorem ProvingText GenerationSimilar Papers 제목 키워드 기반
Generating Millions Of Lean Theorems With Proofs By Exploring State Transition Graphs
Large Language Models (LLMs) have demonstrated significant potential in generating mathematical proofs. However, a persistent challenge is that LLMs occasionally make mistakes, while even a minor mistake can invalidate a…
Automated Theorem ProvingMathematical ProofsLearning to Prove Theorems by Learning to Generate Theorems
We consider the task of automated theorem proving, a key AI task. Deep learning has shown promise for training theorem provers, but there are limited human-written theorems and proofs available for supervised learning. T…
Automated Theorem ProvingAPOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning
Formal reasoning and automated theorem proving constitute a challenging subfield of machine learning, in which machines are tasked with proving mathematical theorems using formal languages like Lean. A formal verificatio…
Automated Theorem ProvingHybridProver: Augmenting Theorem Proving with LLM-Driven Proof Synthesis and Refinement
Formal methods is pivotal for verifying the reliability of critical systems through rigorous mathematical proofs. However, its adoption is hindered by labor-intensive manual proofs and the expertise required to use theor…
Automated Theorem ProvingMathematical ProofsA Combinatorial Identities Benchmark for Theorem Proving via Automated Theorem Generation
Large language models (LLMs) have significantly advanced formal theorem proving, yet the scarcity of high-quality training data constrains their capabilities in complex mathematical domains. Combinatorics, a cornerstone …
Automated Theorem ProvingLanguage ModelingLanguage ModellingLarge Language Model